:: REWRITE2 semantic presentation begin theorem :: REWRITE2:1 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Bool "not" (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) & (Bool (Set (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: REWRITE2:2 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")) ")" )))) "holds" (Bool "ex" (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "l")))) & (Bool (Set (Var "l")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "l")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")))) ")" )))) ; theorem :: REWRITE2:3 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "p")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set (Set (Var "p")) ($#k16_finseq_1 :::"|"::: ) (Set (Var "k"))) "is" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set (Var "R")))))) ; theorem :: REWRITE2:4 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "p")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")))) ")" ))))) ; begin definitionlet "f" be ($#m1_hidden :::"Function":::); attr "f" is :::"XFinSequence-yielding"::: means :: REWRITE2:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#m1_hidden :::"XFinSequence":::))); end; :: deftheorem defines :::"XFinSequence-yielding"::: REWRITE2:def 1 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_rewrite2 :::"XFinSequence-yielding"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#m1_hidden :::"XFinSequence":::))) ")" )); registration cluster ($#v1_xboole_0 :::"empty"::: ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) -> ($#v1_rewrite2 :::"XFinSequence-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "f" be ($#m1_hidden :::"XFinSequence":::); cluster (Set ($#k5_finseq_1 :::"<*"::: ) "f" ($#k5_finseq_1 :::"*>"::: ) ) -> ($#v1_rewrite2 :::"XFinSequence-yielding"::: ) ; end; registrationlet "p" be ($#v1_rewrite2 :::"XFinSequence-yielding"::: ) ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "p" ($#k1_funct_1 :::"."::: ) "x") -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "p" be ($#v1_rewrite2 :::"XFinSequence-yielding"::: ) ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "p" ($#k1_funct_1 :::"."::: ) "x") -> ($#v5_ordinal1 :::"T-Sequence-like"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v1_rewrite2 :::"XFinSequence-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "E" be ($#m1_hidden :::"set"::: ) ; cluster -> ($#v1_rewrite2 :::"XFinSequence-yielding"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set "E" ($#k8_afinsq_1 :::"^omega"::: ) ); end; registrationlet "p", "q" be ($#v1_rewrite2 :::"XFinSequence-yielding"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "p" ($#k7_finseq_1 :::"^"::: ) "q") -> ($#v1_rewrite2 :::"XFinSequence-yielding"::: ) ; end; begin definitionlet "s" be ($#m1_hidden :::"XFinSequence":::); let "p" be ($#v1_rewrite2 :::"XFinSequence-yielding"::: ) ($#m1_hidden :::"Function":::); func "s" :::"^+"::: "p" -> ($#v1_rewrite2 :::"XFinSequence-yielding"::: ) ($#m1_hidden :::"Function":::) means :: REWRITE2:def 2 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "p")) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "p"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set "s" ($#k1_ordinal4 :::"^"::: ) (Set "(" "p" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ); func "p" :::"+^"::: "s" -> ($#v1_rewrite2 :::"XFinSequence-yielding"::: ) ($#m1_hidden :::"Function":::) means :: REWRITE2:def 3 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "p")) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "p"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "p" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k1_ordinal4 :::"^"::: ) "s")) ")" ) ")" ); end; :: deftheorem defines :::"^+"::: REWRITE2:def 2 : (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"XFinSequence":::) (Bool "for" (Set (Var "p")) "," (Set (Var "b3")) "being" ($#v1_rewrite2 :::"XFinSequence-yielding"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_rewrite2 :::"^+"::: ) (Set (Var "p")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_ordinal4 :::"^"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" ))); :: deftheorem defines :::"+^"::: REWRITE2:def 3 : (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"XFinSequence":::) (Bool "for" (Set (Var "p")) "," (Set (Var "b3")) "being" ($#v1_rewrite2 :::"XFinSequence-yielding"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k2_rewrite2 :::"+^"::: ) (Set (Var "s")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set (Var "s")))) ")" ) ")" ) ")" ))); registrationlet "s" be ($#m1_hidden :::"XFinSequence":::); let "p" be ($#v1_rewrite2 :::"XFinSequence-yielding"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "s" ($#k1_rewrite2 :::"^+"::: ) "p") -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v1_rewrite2 :::"XFinSequence-yielding"::: ) ; cluster (Set "p" ($#k2_rewrite2 :::"+^"::: ) "s") -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v1_rewrite2 :::"XFinSequence-yielding"::: ) ; end; theorem :: REWRITE2:5 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"XFinSequence":::) (Bool "for" (Set (Var "p")) "being" ($#v1_rewrite2 :::"XFinSequence-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "s")) ($#k1_rewrite2 :::"^+"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "p")) ($#k2_rewrite2 :::"+^"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) ")" ))) ; theorem :: REWRITE2:6 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#v1_rewrite2 :::"XFinSequence-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k1_rewrite2 :::"^+"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set (Var "p")) ($#k2_rewrite2 :::"+^"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p"))) ")" ))) ; theorem :: REWRITE2:7 (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_hidden :::"XFinSequence":::) (Bool "for" (Set (Var "p")) "being" ($#v1_rewrite2 :::"XFinSequence-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Set (Var "s")) ($#k1_rewrite2 :::"^+"::: ) (Set "(" (Set (Var "t")) ($#k1_rewrite2 :::"^+"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_ordinal4 :::"^"::: ) (Set (Var "t")) ")" ) ($#k1_rewrite2 :::"^+"::: ) (Set (Var "p")))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k2_rewrite2 :::"+^"::: ) (Set (Var "t")) ")" ) ($#k2_rewrite2 :::"+^"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k2_rewrite2 :::"+^"::: ) (Set "(" (Set (Var "t")) ($#k1_ordinal4 :::"^"::: ) (Set (Var "s")) ")" ))) ")" ))) ; theorem :: REWRITE2:8 (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_hidden :::"XFinSequence":::) (Bool "for" (Set (Var "p")) "being" ($#v1_rewrite2 :::"XFinSequence-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set (Var "s")) ($#k1_rewrite2 :::"^+"::: ) (Set "(" (Set (Var "p")) ($#k2_rewrite2 :::"+^"::: ) (Set (Var "t")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_rewrite2 :::"^+"::: ) (Set (Var "p")) ")" ) ($#k2_rewrite2 :::"+^"::: ) (Set (Var "t")))))) ; theorem :: REWRITE2:9 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"XFinSequence":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v1_rewrite2 :::"XFinSequence-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Set (Var "s")) ($#k1_rewrite2 :::"^+"::: ) (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_rewrite2 :::"^+"::: ) (Set (Var "p")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set "(" (Set (Var "s")) ($#k1_rewrite2 :::"^+"::: ) (Set (Var "q")) ")" ))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")) ")" ) ($#k2_rewrite2 :::"+^"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k2_rewrite2 :::"+^"::: ) (Set (Var "s")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set "(" (Set (Var "q")) ($#k2_rewrite2 :::"+^"::: ) (Set (Var "s")) ")" ))) ")" ))) ; begin definitionlet "E" be ($#m1_hidden :::"set"::: ) ; let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Const "E")) ($#k8_afinsq_1 :::"^omega"::: ) ); let "k" be ($#m1_hidden :::"Nat":::); :: original: :::"."::: redefine func "p" :::"."::: "k" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set "E" ($#k8_afinsq_1 :::"^omega"::: ) ); end; definitionlet "E" be ($#m1_hidden :::"set"::: ) ; let "s" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Const "E")) ($#k8_afinsq_1 :::"^omega"::: ) ); let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Const "E")) ($#k8_afinsq_1 :::"^omega"::: ) ); :: original: :::"^+"::: redefine func "s" :::"^+"::: "p" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "E" ($#k8_afinsq_1 :::"^omega"::: ) ); :: original: :::"+^"::: redefine func "p" :::"+^"::: "s" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "E" ($#k8_afinsq_1 :::"^omega"::: ) ); end; definitionlet "E" be ($#m1_hidden :::"set"::: ) ; mode semi-Thue-system of "E" is ($#m1_subset_1 :::"Relation":::) "of" (Set "(" "E" ($#k8_afinsq_1 :::"^omega"::: ) ")" ); end; registrationlet "S" be ($#m1_hidden :::"Relation":::); cluster (Set "S" ($#k2_xboole_0 :::"\/"::: ) (Set "(" "S" ($#k2_relat_1 :::"~"::: ) ")" )) -> ($#v3_relat_2 :::"symmetric"::: ) ; end; registrationlet "E" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v3_relat_2 :::"symmetric"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "(" ($#k2_zfmisc_1 :::"[#]"::: ) "(" (Set "(" "E" ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "," (Set "(" "E" ($#k8_afinsq_1 :::"^omega"::: ) ")" ) ")" ")" ))); end; definitionlet "E" be ($#m1_hidden :::"set"::: ) ; mode Thue-system of "E" is ($#v3_relat_2 :::"symmetric"::: ) ($#m1_subset_1 :::"semi-Thue-system":::) "of" "E"; end; begin definitionlet "E" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Const "E")); let "s", "t" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Const "E")) ($#k8_afinsq_1 :::"^omega"::: ) ); pred "s" :::"-->."::: "t" "," "S" means :: REWRITE2:def 4 (Bool (Set ($#k1_domain_1 :::"["::: ) "s" "," "t" ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "S"); end; :: deftheorem defines :::"-->."::: REWRITE2:def 4 : (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool "(" (Bool (Set (Var "s")) ($#r1_rewrite2 :::"-->."::: ) (Set (Var "t")) "," (Set (Var "S"))) "iff" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) ")" )))); definitionlet "E" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Const "E")); let "s", "t" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Const "E")) ($#k8_afinsq_1 :::"^omega"::: ) ); pred "s" :::"==>."::: "t" "," "S" means :: REWRITE2:def 5 (Bool "ex" (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "s1")) "," (Set (Var "t1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "E" ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool "(" (Bool "s" ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k1_flang_1 :::"^"::: ) (Set (Var "s1")) ")" ) ($#k1_flang_1 :::"^"::: ) (Set (Var "w")))) & (Bool "t" ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k1_flang_1 :::"^"::: ) (Set (Var "t1")) ")" ) ($#k1_flang_1 :::"^"::: ) (Set (Var "w")))) & (Bool (Set (Var "s1")) ($#r1_rewrite2 :::"-->."::: ) (Set (Var "t1")) "," "S") ")" )); end; :: deftheorem defines :::"==>."::: REWRITE2:def 5 : (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool "(" (Bool (Set (Var "s")) ($#r2_rewrite2 :::"==>."::: ) (Set (Var "t")) "," (Set (Var "S"))) "iff" (Bool "ex" (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "s1")) "," (Set (Var "t1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool "(" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k1_flang_1 :::"^"::: ) (Set (Var "s1")) ")" ) ($#k1_flang_1 :::"^"::: ) (Set (Var "w")))) & (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k1_flang_1 :::"^"::: ) (Set (Var "t1")) ")" ) ($#k1_flang_1 :::"^"::: ) (Set (Var "w")))) & (Bool (Set (Var "s1")) ($#r1_rewrite2 :::"-->."::: ) (Set (Var "t1")) "," (Set (Var "S"))) ")" )) ")" )))); theorem :: REWRITE2:10 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "s")) ($#r1_rewrite2 :::"-->."::: ) (Set (Var "t")) "," (Set (Var "S")))) "holds" (Bool (Set (Var "s")) ($#r2_rewrite2 :::"==>."::: ) (Set (Var "t")) "," (Set (Var "S")))))) ; theorem :: REWRITE2:11 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "s")) ($#r2_rewrite2 :::"==>."::: ) (Set (Var "s")) "," (Set (Var "S")))) "holds" (Bool "ex" (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "s1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool "(" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k1_flang_1 :::"^"::: ) (Set (Var "s1")) ")" ) ($#k1_flang_1 :::"^"::: ) (Set (Var "w")))) & (Bool (Set (Var "s1")) ($#r1_rewrite2 :::"-->."::: ) (Set (Var "s1")) "," (Set (Var "S"))) ")" ))))) ; theorem :: REWRITE2:12 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "s")) ($#r2_rewrite2 :::"==>."::: ) (Set (Var "t")) "," (Set (Var "S")))) "holds" (Bool "(" (Bool (Set (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "s"))) ($#r2_rewrite2 :::"==>."::: ) (Set (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "t"))) "," (Set (Var "S"))) & (Bool (Set (Set (Var "s")) ($#k1_flang_1 :::"^"::: ) (Set (Var "u"))) ($#r2_rewrite2 :::"==>."::: ) (Set (Set (Var "t")) ($#k1_flang_1 :::"^"::: ) (Set (Var "u"))) "," (Set (Var "S"))) ")" )))) ; theorem :: REWRITE2:13 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "s")) ($#r2_rewrite2 :::"==>."::: ) (Set (Var "t")) "," (Set (Var "S")))) "holds" (Bool (Set (Set "(" (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "s")) ")" ) ($#k1_flang_1 :::"^"::: ) (Set (Var "v"))) ($#r2_rewrite2 :::"==>."::: ) (Set (Set "(" (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "t")) ")" ) ($#k1_flang_1 :::"^"::: ) (Set (Var "v"))) "," (Set (Var "S")))))) ; theorem :: REWRITE2:14 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "s")) ($#r1_rewrite2 :::"-->."::: ) (Set (Var "t")) "," (Set (Var "S")))) "holds" (Bool "(" (Bool (Set (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "s"))) ($#r2_rewrite2 :::"==>."::: ) (Set (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "t"))) "," (Set (Var "S"))) & (Bool (Set (Set (Var "s")) ($#k1_flang_1 :::"^"::: ) (Set (Var "u"))) ($#r2_rewrite2 :::"==>."::: ) (Set (Set (Var "t")) ($#k1_flang_1 :::"^"::: ) (Set (Var "u"))) "," (Set (Var "S"))) ")" )))) ; theorem :: REWRITE2:15 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "s")) ($#r1_rewrite2 :::"-->."::: ) (Set (Var "t")) "," (Set (Var "S")))) "holds" (Bool (Set (Set "(" (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "s")) ")" ) ($#k1_flang_1 :::"^"::: ) (Set (Var "v"))) ($#r2_rewrite2 :::"==>."::: ) (Set (Set "(" (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "t")) ")" ) ($#k1_flang_1 :::"^"::: ) (Set (Var "v"))) "," (Set (Var "S")))))) ; theorem :: REWRITE2:16 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "S")) "is" ($#m1_subset_1 :::"Thue-system":::) "of" (Set (Var "E"))) & (Bool (Set (Var "s")) ($#r1_rewrite2 :::"-->."::: ) (Set (Var "t")) "," (Set (Var "S")))) "holds" (Bool (Set (Var "t")) ($#r1_rewrite2 :::"-->."::: ) (Set (Var "s")) "," (Set (Var "S")))))) ; theorem :: REWRITE2:17 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "S")) "is" ($#m1_subset_1 :::"Thue-system":::) "of" (Set (Var "E"))) & (Bool (Set (Var "s")) ($#r2_rewrite2 :::"==>."::: ) (Set (Var "t")) "," (Set (Var "S")))) "holds" (Bool (Set (Var "t")) ($#r2_rewrite2 :::"==>."::: ) (Set (Var "s")) "," (Set (Var "S")))))) ; theorem :: REWRITE2:18 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "S")) ($#r1_relset_1 :::"c="::: ) (Set (Var "T"))) & (Bool (Set (Var "s")) ($#r1_rewrite2 :::"-->."::: ) (Set (Var "t")) "," (Set (Var "S")))) "holds" (Bool (Set (Var "s")) ($#r1_rewrite2 :::"-->."::: ) (Set (Var "t")) "," (Set (Var "T")))))) ; theorem :: REWRITE2:19 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "S")) ($#r1_relset_1 :::"c="::: ) (Set (Var "T"))) & (Bool (Set (Var "s")) ($#r2_rewrite2 :::"==>."::: ) (Set (Var "t")) "," (Set (Var "S")))) "holds" (Bool (Set (Var "s")) ($#r2_rewrite2 :::"==>."::: ) (Set (Var "t")) "," (Set (Var "T")))))) ; theorem :: REWRITE2:20 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool (Bool "not" (Set (Var "s")) ($#r2_rewrite2 :::"==>."::: ) (Set (Var "t")) "," (Set ($#k1_partit_2 :::"{}"::: ) "(" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "," (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) ")" ))))) ; theorem :: REWRITE2:21 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool "(" "not" (Bool (Set (Var "s")) ($#r2_rewrite2 :::"==>."::: ) (Set (Var "t")) "," (Set (Set (Var "S")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "T")))) "or" (Bool (Set (Var "s")) ($#r2_rewrite2 :::"==>."::: ) (Set (Var "t")) "," (Set (Var "S"))) "or" (Bool (Set (Var "s")) ($#r2_rewrite2 :::"==>."::: ) (Set (Var "t")) "," (Set (Var "T"))) ")" )))) ; begin definitionlet "E" be ($#m1_hidden :::"set"::: ) ; :: original: :::"id"::: redefine func :::"id"::: "E" -> ($#m1_subset_1 :::"Relation":::) "of" "E"; end; definitionlet "E" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Const "E")); func :::"==>.-relation"::: "S" -> ($#m1_subset_1 :::"Relation":::) "of" (Set "(" "E" ($#k8_afinsq_1 :::"^omega"::: ) ")" ) means :: REWRITE2:def 6 (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "E" ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "s")) ($#r2_rewrite2 :::"==>."::: ) (Set (Var "t")) "," "S") ")" )); end; :: deftheorem defines :::"==>.-relation"::: REWRITE2:def 6 : (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k7_rewrite2 :::"==>.-relation"::: ) (Set (Var "S")))) "iff" (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool (Set (Var "s")) ($#r2_rewrite2 :::"==>."::: ) (Set (Var "t")) "," (Set (Var "S"))) ")" )) ")" )))); theorem :: REWRITE2:22 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) "holds" (Bool (Set (Var "S")) ($#r1_relset_1 :::"c="::: ) (Set ($#k7_rewrite2 :::"==>.-relation"::: ) (Set (Var "S")))))) ; theorem :: REWRITE2:23 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "p")) "is" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k7_rewrite2 :::"==>.-relation"::: ) (Set (Var "S"))))) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k5_rewrite2 :::"+^"::: ) (Set (Var "u"))) "is" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k7_rewrite2 :::"==>.-relation"::: ) (Set (Var "S")))) & (Bool (Set (Set (Var "u")) ($#k4_rewrite2 :::"^+"::: ) (Set (Var "p"))) "is" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k7_rewrite2 :::"==>.-relation"::: ) (Set (Var "S")))) ")" ))))) ; theorem :: REWRITE2:24 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "t")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "p")) "is" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k7_rewrite2 :::"==>.-relation"::: ) (Set (Var "S"))))) "holds" (Bool (Set (Set "(" (Set (Var "t")) ($#k4_rewrite2 :::"^+"::: ) (Set (Var "p")) ")" ) ($#k5_rewrite2 :::"+^"::: ) (Set (Var "u"))) "is" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k7_rewrite2 :::"==>.-relation"::: ) (Set (Var "S")))))))) ; theorem :: REWRITE2:25 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "S")) "is" ($#m1_subset_1 :::"Thue-system":::) "of" (Set (Var "E")))) "holds" (Bool (Set ($#k7_rewrite2 :::"==>.-relation"::: ) (Set (Var "S"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k7_rewrite2 :::"==>.-relation"::: ) (Set (Var "S")) ")" ) ($#k3_relset_1 :::"~"::: ) )))) ; theorem :: REWRITE2:26 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "S")) ($#r1_relset_1 :::"c="::: ) (Set (Var "T")))) "holds" (Bool (Set ($#k7_rewrite2 :::"==>.-relation"::: ) (Set (Var "S"))) ($#r1_relset_1 :::"c="::: ) (Set ($#k7_rewrite2 :::"==>.-relation"::: ) (Set (Var "T")))))) ; theorem :: REWRITE2:27 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k7_rewrite2 :::"==>.-relation"::: ) (Set "(" ($#k6_rewrite2 :::"id"::: ) (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) ")" )) ($#r2_relset_1 :::"="::: ) (Set ($#k6_rewrite2 :::"id"::: ) (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" )))) ; theorem :: REWRITE2:28 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) "holds" (Bool (Set ($#k7_rewrite2 :::"==>.-relation"::: ) (Set "(" (Set (Var "S")) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k6_rewrite2 :::"id"::: ) (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) ")" ) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k7_rewrite2 :::"==>.-relation"::: ) (Set (Var "S")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k6_rewrite2 :::"id"::: ) (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) ")" ))))) ; theorem :: REWRITE2:29 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k7_rewrite2 :::"==>.-relation"::: ) (Set "(" ($#k1_partit_2 :::"{}"::: ) "(" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "," (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) ")" ")" )) ($#r2_relset_1 :::"="::: ) (Set ($#k1_partit_2 :::"{}"::: ) "(" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "," (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) ")" ))) ; theorem :: REWRITE2:30 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "s")) ($#r2_rewrite2 :::"==>."::: ) (Set (Var "t")) "," (Set ($#k7_rewrite2 :::"==>.-relation"::: ) (Set (Var "S"))))) "holds" (Bool (Set (Var "s")) ($#r2_rewrite2 :::"==>."::: ) (Set (Var "t")) "," (Set (Var "S")))))) ; theorem :: REWRITE2:31 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) "holds" (Bool (Set ($#k7_rewrite2 :::"==>.-relation"::: ) (Set "(" ($#k7_rewrite2 :::"==>.-relation"::: ) (Set (Var "S")) ")" )) ($#r2_relset_1 :::"="::: ) (Set ($#k7_rewrite2 :::"==>.-relation"::: ) (Set (Var "S")))))) ; begin definitionlet "E" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Const "E")); let "s", "t" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Const "E")) ($#k8_afinsq_1 :::"^omega"::: ) ); pred "s" :::"==>*"::: "t" "," "S" means :: REWRITE2:def 7 (Bool (Set ($#k7_rewrite2 :::"==>.-relation"::: ) "S") ($#r1_rewrite1 :::"reduces"::: ) "s" "," "t"); end; :: deftheorem defines :::"==>*"::: REWRITE2:def 7 : (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool "(" (Bool (Set (Var "s")) ($#r3_rewrite2 :::"==>*"::: ) (Set (Var "t")) "," (Set (Var "S"))) "iff" (Bool (Set ($#k7_rewrite2 :::"==>.-relation"::: ) (Set (Var "S"))) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "s")) "," (Set (Var "t"))) ")" )))); theorem :: REWRITE2:32 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool (Set (Var "s")) ($#r3_rewrite2 :::"==>*"::: ) (Set (Var "s")) "," (Set (Var "S")))))) ; theorem :: REWRITE2:33 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "s")) ($#r2_rewrite2 :::"==>."::: ) (Set (Var "t")) "," (Set (Var "S")))) "holds" (Bool (Set (Var "s")) ($#r3_rewrite2 :::"==>*"::: ) (Set (Var "t")) "," (Set (Var "S")))))) ; theorem :: REWRITE2:34 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "s")) ($#r1_rewrite2 :::"-->."::: ) (Set (Var "t")) "," (Set (Var "S")))) "holds" (Bool (Set (Var "s")) ($#r3_rewrite2 :::"==>*"::: ) (Set (Var "t")) "," (Set (Var "S")))))) ; theorem :: REWRITE2:35 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "s")) ($#r3_rewrite2 :::"==>*"::: ) (Set (Var "t")) "," (Set (Var "S"))) & (Bool (Set (Var "t")) ($#r3_rewrite2 :::"==>*"::: ) (Set (Var "u")) "," (Set (Var "S")))) "holds" (Bool (Set (Var "s")) ($#r3_rewrite2 :::"==>*"::: ) (Set (Var "u")) "," (Set (Var "S")))))) ; theorem :: REWRITE2:36 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "s")) ($#r3_rewrite2 :::"==>*"::: ) (Set (Var "t")) "," (Set (Var "S")))) "holds" (Bool "(" (Bool (Set (Set (Var "s")) ($#k1_flang_1 :::"^"::: ) (Set (Var "u"))) ($#r3_rewrite2 :::"==>*"::: ) (Set (Set (Var "t")) ($#k1_flang_1 :::"^"::: ) (Set (Var "u"))) "," (Set (Var "S"))) & (Bool (Set (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "s"))) ($#r3_rewrite2 :::"==>*"::: ) (Set (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "t"))) "," (Set (Var "S"))) ")" )))) ; theorem :: REWRITE2:37 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "s")) ($#r3_rewrite2 :::"==>*"::: ) (Set (Var "t")) "," (Set (Var "S")))) "holds" (Bool (Set (Set "(" (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "s")) ")" ) ($#k1_flang_1 :::"^"::: ) (Set (Var "v"))) ($#r3_rewrite2 :::"==>*"::: ) (Set (Set "(" (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "t")) ")" ) ($#k1_flang_1 :::"^"::: ) (Set (Var "v"))) "," (Set (Var "S")))))) ; theorem :: REWRITE2:38 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "s")) ($#r3_rewrite2 :::"==>*"::: ) (Set (Var "t")) "," (Set (Var "S"))) & (Bool (Set (Var "u")) ($#r3_rewrite2 :::"==>*"::: ) (Set (Var "v")) "," (Set (Var "S")))) "holds" (Bool "(" (Bool (Set (Set (Var "s")) ($#k1_flang_1 :::"^"::: ) (Set (Var "u"))) ($#r3_rewrite2 :::"==>*"::: ) (Set (Set (Var "t")) ($#k1_flang_1 :::"^"::: ) (Set (Var "v"))) "," (Set (Var "S"))) & (Bool (Set (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "s"))) ($#r3_rewrite2 :::"==>*"::: ) (Set (Set (Var "v")) ($#k1_flang_1 :::"^"::: ) (Set (Var "t"))) "," (Set (Var "S"))) ")" )))) ; theorem :: REWRITE2:39 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "S")) "is" ($#m1_subset_1 :::"Thue-system":::) "of" (Set (Var "E"))) & (Bool (Set (Var "s")) ($#r3_rewrite2 :::"==>*"::: ) (Set (Var "t")) "," (Set (Var "S")))) "holds" (Bool (Set (Var "t")) ($#r3_rewrite2 :::"==>*"::: ) (Set (Var "s")) "," (Set (Var "S")))))) ; theorem :: REWRITE2:40 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "S")) ($#r1_relset_1 :::"c="::: ) (Set (Var "T"))) & (Bool (Set (Var "s")) ($#r3_rewrite2 :::"==>*"::: ) (Set (Var "t")) "," (Set (Var "S")))) "holds" (Bool (Set (Var "s")) ($#r3_rewrite2 :::"==>*"::: ) (Set (Var "t")) "," (Set (Var "T")))))) ; theorem :: REWRITE2:41 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool "(" (Bool (Set (Var "s")) ($#r3_rewrite2 :::"==>*"::: ) (Set (Var "t")) "," (Set (Var "S"))) "iff" (Bool (Set (Var "s")) ($#r3_rewrite2 :::"==>*"::: ) (Set (Var "t")) "," (Set (Set (Var "S")) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k6_rewrite2 :::"id"::: ) (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) ")" ))) ")" )))) ; theorem :: REWRITE2:42 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "s")) ($#r3_rewrite2 :::"==>*"::: ) (Set (Var "t")) "," (Set ($#k1_partit_2 :::"{}"::: ) "(" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "," (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) ")" ))) "holds" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set (Var "t"))))) ; theorem :: REWRITE2:43 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "s")) ($#r3_rewrite2 :::"==>*"::: ) (Set (Var "t")) "," (Set ($#k7_rewrite2 :::"==>.-relation"::: ) (Set (Var "S"))))) "holds" (Bool (Set (Var "s")) ($#r3_rewrite2 :::"==>*"::: ) (Set (Var "t")) "," (Set (Var "S")))))) ; theorem :: REWRITE2:44 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "s")) ($#r3_rewrite2 :::"==>*"::: ) (Set (Var "t")) "," (Set (Var "S"))) & (Bool (Set (Var "u")) ($#r2_rewrite2 :::"==>."::: ) (Set (Var "v")) "," (Set ($#k4_lang1 :::"{"::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k1_domain_1 :::"]"::: ) ) ($#k4_lang1 :::"}"::: ) ))) "holds" (Bool (Set (Var "u")) ($#r3_rewrite2 :::"==>*"::: ) (Set (Var "v")) "," (Set (Var "S")))))) ; theorem :: REWRITE2:45 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "s")) ($#r3_rewrite2 :::"==>*"::: ) (Set (Var "t")) "," (Set (Var "S"))) & (Bool (Set (Var "u")) ($#r3_rewrite2 :::"==>*"::: ) (Set (Var "v")) "," (Set (Set (Var "S")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k4_lang1 :::"{"::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k1_domain_1 :::"]"::: ) ) ($#k4_lang1 :::"}"::: ) )))) "holds" (Bool (Set (Var "u")) ($#r3_rewrite2 :::"==>*"::: ) (Set (Var "v")) "," (Set (Var "S")))))) ; begin definitionlet "E" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Const "E")); let "w" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Const "E")) ($#k8_afinsq_1 :::"^omega"::: ) ); func :::"Lang"::: "(" "w" "," "S" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "E" ($#k8_afinsq_1 :::"^omega"::: ) ")" ) equals :: REWRITE2:def 8 "{" (Set (Var "s")) where s "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set "E" ($#k8_afinsq_1 :::"^omega"::: ) ) : (Bool "w" ($#r3_rewrite2 :::"==>*"::: ) (Set (Var "s")) "," "S") "}" ; end; :: deftheorem defines :::"Lang"::: REWRITE2:def 8 : (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool (Set ($#k8_rewrite2 :::"Lang"::: ) "(" (Set (Var "w")) "," (Set (Var "S")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "s")) where s "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) : (Bool (Set (Var "w")) ($#r3_rewrite2 :::"==>*"::: ) (Set (Var "s")) "," (Set (Var "S"))) "}" )))); theorem :: REWRITE2:46 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "s")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k8_rewrite2 :::"Lang"::: ) "(" (Set (Var "w")) "," (Set (Var "S")) ")" )) "iff" (Bool (Set (Var "w")) ($#r3_rewrite2 :::"==>*"::: ) (Set (Var "s")) "," (Set (Var "S"))) ")" )))) ; theorem :: REWRITE2:47 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set ($#k8_rewrite2 :::"Lang"::: ) "(" (Set (Var "w")) "," (Set (Var "S")) ")" ))))) ; registrationlet "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Const "E")); let "w" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Const "E")) ($#k8_afinsq_1 :::"^omega"::: ) ); cluster (Set ($#k8_rewrite2 :::"Lang"::: ) "(" "w" "," "S" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: REWRITE2:48 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "S")) ($#r1_relset_1 :::"c="::: ) (Set (Var "T")))) "holds" (Bool (Set ($#k8_rewrite2 :::"Lang"::: ) "(" (Set (Var "w")) "," (Set (Var "S")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k8_rewrite2 :::"Lang"::: ) "(" (Set (Var "w")) "," (Set (Var "T")) ")" ))))) ; theorem :: REWRITE2:49 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool (Set ($#k8_rewrite2 :::"Lang"::: ) "(" (Set (Var "w")) "," (Set (Var "S")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_rewrite2 :::"Lang"::: ) "(" (Set (Var "w")) "," (Set "(" (Set (Var "S")) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k6_rewrite2 :::"id"::: ) (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) ")" ) ")" ) ")" ))))) ; theorem :: REWRITE2:50 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool (Set ($#k8_rewrite2 :::"Lang"::: ) "(" (Set (Var "w")) "," (Set "(" ($#k1_partit_2 :::"{}"::: ) "(" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "," (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set (Var "w")) ($#k4_flang_1 :::"}"::: ) )))) ; theorem :: REWRITE2:51 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool (Set ($#k8_rewrite2 :::"Lang"::: ) "(" (Set (Var "w")) "," (Set "(" ($#k6_rewrite2 :::"id"::: ) (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set (Var "w")) ($#k4_flang_1 :::"}"::: ) )))) ; begin definitionlet "E" be ($#m1_hidden :::"set"::: ) ; let "S", "T" be ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Const "E")); let "w" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Const "E")) ($#k8_afinsq_1 :::"^omega"::: ) ); pred "S" "," "T" :::"are_equivalent_wrt"::: "w" means :: REWRITE2:def 9 (Bool (Set ($#k8_rewrite2 :::"Lang"::: ) "(" "w" "," "S" ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_rewrite2 :::"Lang"::: ) "(" "w" "," "T" ")" )); end; :: deftheorem defines :::"are_equivalent_wrt"::: REWRITE2:def 9 : (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool "(" (Bool (Set (Var "S")) "," (Set (Var "T")) ($#r4_rewrite2 :::"are_equivalent_wrt"::: ) (Set (Var "w"))) "iff" (Bool (Set ($#k8_rewrite2 :::"Lang"::: ) "(" (Set (Var "w")) "," (Set (Var "S")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_rewrite2 :::"Lang"::: ) "(" (Set (Var "w")) "," (Set (Var "T")) ")" )) ")" )))); theorem :: REWRITE2:52 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool (Set (Var "S")) "," (Set (Var "S")) ($#r4_rewrite2 :::"are_equivalent_wrt"::: ) (Set (Var "w")))))) ; theorem :: REWRITE2:53 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "S")) "," (Set (Var "T")) ($#r4_rewrite2 :::"are_equivalent_wrt"::: ) (Set (Var "w")))) "holds" (Bool (Set (Var "T")) "," (Set (Var "S")) ($#r4_rewrite2 :::"are_equivalent_wrt"::: ) (Set (Var "w")))))) ; theorem :: REWRITE2:54 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "," (Set (Var "U")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "S")) "," (Set (Var "T")) ($#r4_rewrite2 :::"are_equivalent_wrt"::: ) (Set (Var "w"))) & (Bool (Set (Var "T")) "," (Set (Var "U")) ($#r4_rewrite2 :::"are_equivalent_wrt"::: ) (Set (Var "w")))) "holds" (Bool (Set (Var "S")) "," (Set (Var "U")) ($#r4_rewrite2 :::"are_equivalent_wrt"::: ) (Set (Var "w")))))) ; theorem :: REWRITE2:55 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool (Set (Var "S")) "," (Set (Set (Var "S")) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k6_rewrite2 :::"id"::: ) (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) ")" )) ($#r4_rewrite2 :::"are_equivalent_wrt"::: ) (Set (Var "w")))))) ; theorem :: REWRITE2:56 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "," (Set (Var "U")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "S")) "," (Set (Var "T")) ($#r4_rewrite2 :::"are_equivalent_wrt"::: ) (Set (Var "w"))) & (Bool (Set (Var "S")) ($#r1_relset_1 :::"c="::: ) (Set (Var "U"))) & (Bool (Set (Var "U")) ($#r1_relset_1 :::"c="::: ) (Set (Var "T")))) "holds" (Bool "(" (Bool (Set (Var "S")) "," (Set (Var "U")) ($#r4_rewrite2 :::"are_equivalent_wrt"::: ) (Set (Var "w"))) & (Bool (Set (Var "U")) "," (Set (Var "T")) ($#r4_rewrite2 :::"are_equivalent_wrt"::: ) (Set (Var "w"))) ")" )))) ; theorem :: REWRITE2:57 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool (Set (Var "S")) "," (Set ($#k7_rewrite2 :::"==>.-relation"::: ) (Set (Var "S"))) ($#r4_rewrite2 :::"are_equivalent_wrt"::: ) (Set (Var "w")))))) ; theorem :: REWRITE2:58 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "w")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "S")) "," (Set (Var "T")) ($#r4_rewrite2 :::"are_equivalent_wrt"::: ) (Set (Var "w"))) & (Bool (Set ($#k7_rewrite2 :::"==>.-relation"::: ) (Set "(" (Set (Var "S")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "T")) ")" )) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "w")) "," (Set (Var "s")))) "holds" (Bool (Set ($#k7_rewrite2 :::"==>.-relation"::: ) (Set (Var "S"))) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "w")) "," (Set (Var "s")))))) ; theorem :: REWRITE2:59 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "w")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "S")) "," (Set (Var "T")) ($#r4_rewrite2 :::"are_equivalent_wrt"::: ) (Set (Var "w"))) & (Bool (Set (Var "w")) ($#r3_rewrite2 :::"==>*"::: ) (Set (Var "s")) "," (Set (Set (Var "S")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "T"))))) "holds" (Bool (Set (Var "w")) ($#r3_rewrite2 :::"==>*"::: ) (Set (Var "s")) "," (Set (Var "S")))))) ; theorem :: REWRITE2:60 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "S")) "," (Set (Var "T")) ($#r4_rewrite2 :::"are_equivalent_wrt"::: ) (Set (Var "w")))) "holds" (Bool (Set (Var "S")) "," (Set (Set (Var "S")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "T"))) ($#r4_rewrite2 :::"are_equivalent_wrt"::: ) (Set (Var "w")))))) ; theorem :: REWRITE2:61 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "s")) ($#r2_rewrite2 :::"==>."::: ) (Set (Var "t")) "," (Set (Var "S")))) "holds" (Bool (Set (Var "S")) "," (Set (Set (Var "S")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k4_lang1 :::"{"::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k1_domain_1 :::"]"::: ) ) ($#k4_lang1 :::"}"::: ) )) ($#r4_rewrite2 :::"are_equivalent_wrt"::: ) (Set (Var "w")))))) ; theorem :: REWRITE2:62 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"semi-Thue-system":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "s")) ($#r3_rewrite2 :::"==>*"::: ) (Set (Var "t")) "," (Set (Var "S")))) "holds" (Bool (Set (Var "S")) "," (Set (Set (Var "S")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k4_lang1 :::"{"::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k1_domain_1 :::"]"::: ) ) ($#k4_lang1 :::"}"::: ) )) ($#r4_rewrite2 :::"are_equivalent_wrt"::: ) (Set (Var "w")))))) ;