equal
deleted
inserted
replaced
148 "\<forall>i j u v. i < j + 1 --> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]" |
148 "\<forall>i j u v. i < j + 1 --> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]" |
149 apply (induct_tac t) |
149 apply (induct_tac t) |
150 apply (simp_all |
150 apply (simp_all |
151 add: diff_Suc subst_Var lift_lift [symmetric] lift_subst_lt |
151 add: diff_Suc subst_Var lift_lift [symmetric] lift_subst_lt |
152 split: nat.split) |
152 split: nat.split) |
153 apply (auto simp add: linorder_neq_iff) |
|
154 done |
153 done |
155 |
154 |
156 |
155 |
157 subsection {* Equivalence proof for optimized substitution *} |
156 subsection {* Equivalence proof for optimized substitution *} |
158 |
157 |