equal
deleted
inserted
replaced
1140 "wf {(v1, v2). v1 :\<sqsubset>val v2 \<and> v1 \<in> LV r s \<and> v2 \<in> LV r s}" |
1140 "wf {(v1, v2). v1 :\<sqsubset>val v2 \<and> v1 \<in> LV r s \<and> v2 \<in> LV r s}" |
1141 apply(rule finite_acyclic_wf) |
1141 apply(rule finite_acyclic_wf) |
1142 prefer 2 |
1142 prefer 2 |
1143 apply(simp add: acyclic_def) |
1143 apply(simp add: acyclic_def) |
1144 apply(induct_tac rule: trancl.induct) |
1144 apply(induct_tac rule: trancl.induct) |
1145 apply(auto)[1] |
1145 apply(auto)[1] |
|
1146 prefer 3 |
|
1147 |
1146 oops |
1148 oops |
1147 |
1149 |
1148 |
1150 |
1149 unused_thms |
1151 unused_thms |
1150 |
1152 |