equal
deleted
inserted
replaced
130 apply simp |
130 apply simp |
131 apply (frule listall_conj1) |
131 apply (frule listall_conj1) |
132 apply (drule listall_conj2) |
132 apply (drule listall_conj2) |
133 apply (drule_tac i=i and j=j in subst_terms_NF) |
133 apply (drule_tac i=i and j=j in subst_terms_NF) |
134 apply assumption |
134 apply assumption |
135 apply (rule_tac m=x and n=j in nat_eq_dec [THEN disjE, standard]) |
135 apply (rule_tac m1=x and n1=j in nat_eq_dec [THEN disjE]) |
136 apply simp |
136 apply simp |
137 apply (erule NF.App) |
137 apply (erule NF.App) |
138 apply (rule_tac m=j and n=x in nat_le_dec [THEN disjE, standard]) |
138 apply (rule_tac m1=j and n1=x in nat_le_dec [THEN disjE]) |
139 apply simp |
139 apply simp |
140 apply (iprover intro: NF.App) |
140 apply (iprover intro: NF.App) |
141 apply simp |
141 apply simp |
142 apply (iprover intro: NF.App) |
142 apply (iprover intro: NF.App) |
143 apply simp |
143 apply simp |
171 apply (induct arbitrary: i set: NF) |
171 apply (induct arbitrary: i set: NF) |
172 apply (frule listall_conj1) |
172 apply (frule listall_conj1) |
173 apply (drule listall_conj2) |
173 apply (drule listall_conj2) |
174 apply (drule_tac i=i in lift_terms_NF) |
174 apply (drule_tac i=i in lift_terms_NF) |
175 apply assumption |
175 apply assumption |
176 apply (rule_tac m=x and n=i in nat_le_dec [THEN disjE, standard]) |
176 apply (rule_tac m1=x and n1=i in nat_le_dec [THEN disjE]) |
177 apply simp |
177 apply simp |
178 apply (rule NF.App) |
178 apply (rule NF.App) |
179 apply assumption |
179 apply assumption |
180 apply simp |
180 apply simp |
181 apply (rule NF.App) |
181 apply (rule NF.App) |