Paper/Paper.thy
changeset 1713 a3f923d88215
parent 1712 40f13b52b107
child 1714 8c59c8a0721c
equal deleted inserted replaced
1712:40f13b52b107 1713:a3f923d88215
  1236      provided @{term "x\<^isub>j"} is a deep recursive binder with the auxiliary binding
  1236      provided @{term "x\<^isub>j"} is a deep recursive binder with the auxiliary binding
  1237      function @{text "bn\<^isub>m"} and permutation @{text "\<pi>"}, @{term "fvs"} is a compound
  1237      function @{text "bn\<^isub>m"} and permutation @{text "\<pi>"}, @{term "fvs"} is a compound
  1238      free variable function returning the union of appropriate @{term "fv_ty\<^isub>x"} and
  1238      free variable function returning the union of appropriate @{term "fv_ty\<^isub>x"} and
  1239      @{term "R"} is the composition of equivalence relations @{text "\<approx>"} and @{text "\<approx>\<^isub>n"}\\
  1239      @{term "R"} is the composition of equivalence relations @{text "\<approx>"} and @{text "\<approx>\<^isub>n"}\\
  1240   $\bullet$ & @{text "x\<^isub>j"} has a deep recursive binding\\
  1240   $\bullet$ & @{text "x\<^isub>j"} has a deep recursive binding\\
  1241   $\bullet$ & @{term "({x\<^isub>n, x\<^isub>j) \<approx>gen R fv_ty \<pi> (y\<^isub>n, y\<^isub>j)"} provided @{text "x\<^isub>j"} has
  1241   $\bullet$ & @{term "({x\<^isub>n}, x\<^isub>j) \<approx>gen R fv_ty \<pi> ({y\<^isub>n}, y\<^isub>j)"} provided @{text "x\<^isub>j"} has
  1242      a shallow binder @{text "x\<^isub>n"} with permutation @{text "\<pi>"}, @{term "R"} is the
  1242      a shallow binder @{text "x\<^isub>n"} with permutation @{text "\<pi>"}, @{term "R"} is the
  1243      alpha-equivalence for @{term "x\<^isub>j"}
  1243      alpha-equivalence for @{term "x\<^isub>j"}
  1244      and @{term "fv_ty"} is the free variable function for @{term "x\<^isub>j"}\\
  1244      and @{term "fv_ty"} is the free variable function for @{term "x\<^isub>j"}\\
  1245   $\bullet$ & @{term "(bn\<^isub>m x\<^isub>n, x\<^isub>j) \<approx>gen R fv_ty \<pi> (bn\<^isub>m y\<^isub>n, y\<^isub>j)"} provided @{text "x\<^isub>j"}
  1245   $\bullet$ & @{term "(bn\<^isub>m x\<^isub>n, x\<^isub>j) \<approx>gen R fv_ty \<pi> (bn\<^isub>m y\<^isub>n, y\<^isub>j)"} provided @{text "x\<^isub>j"}
  1246      has a deep non-recursive binder @{text "bn\<^isub>m x\<^isub>n"} with permutation @{text "\<pi>"}, @{term "R"} is the
  1246      has a deep non-recursive binder @{text "bn\<^isub>m x\<^isub>n"} with permutation @{text "\<pi>"}, @{term "R"} is the