src/ZF/Constructible/Rec_Separation.thy
 changeset 13651 ac80e101306a parent 13647 7f6f0ffc45c3 child 13655 95b95cdb4704
```     1.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Thu Oct 17 10:52:59 2002 +0200
1.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Thu Oct 17 10:54:11 2002 +0200
1.3 @@ -53,11 +53,6 @@
1.4   "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> rtran_closure_mem_fm(x,y,z) \<in> formula"
1.6
1.7 -lemma arity_rtran_closure_mem_fm [simp]:
1.8 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.9 -      ==> arity(rtran_closure_mem_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
1.10 -by (simp add: rtran_closure_mem_fm_def succ_Un_distrib [symmetric] Un_ac)
1.11 -
1.12  lemma sats_rtran_closure_mem_fm [simp]:
1.13     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.14      ==> sats(A, rtran_closure_mem_fm(x,y,z), env) <->
1.15 @@ -103,11 +98,6 @@
1.16       "[| x \<in> nat; y \<in> nat |] ==> rtran_closure_fm(x,y) \<in> formula"
1.18
1.19 -lemma arity_rtran_closure_fm [simp]:
1.20 -     "[| x \<in> nat; y \<in> nat |]
1.21 -      ==> arity(rtran_closure_fm(x,y)) = succ(x) \<union> succ(y)"
1.22 -by (simp add: rtran_closure_fm_def succ_Un_distrib [symmetric] Un_ac)
1.23 -
1.24  lemma sats_rtran_closure_fm [simp]:
1.25     "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
1.26      ==> sats(A, rtran_closure_fm(x,y), env) <->
1.27 @@ -140,11 +130,6 @@
1.28       "[| x \<in> nat; y \<in> nat |] ==> tran_closure_fm(x,y) \<in> formula"