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.5  by (simp add: rtran_closure_mem_fm_def)
     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.17  by (simp add: rtran_closure_fm_def)
    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"
    1.29  by (simp add: tran_closure_fm_def)
    1.30  
    1.31 -lemma arity_tran_closure_fm [simp]:
    1.32 -     "[| x \<in> nat; y \<in> nat |]
    1.33 -      ==> arity(tran_closure_fm(x,y)) = succ(x) \<union> succ(y)"
    1.34 -by (simp add: tran_closure_fm_def succ_Un_distrib [symmetric] Un_ac)
    1.35 -
    1.36  lemma sats_tran_closure_fm [simp]:
    1.37     "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
    1.38      ==> sats(A, tran_closure_fm(x,y), env) <->