:: REWRITE3 semantic presentation begin theorem :: REWRITE3:1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))))))) ; theorem :: REWRITE3:2 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::)(Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) ))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1))) ")" )))) ; theorem :: REWRITE3:3 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Bool "not" (Set (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "k"))))) ; begin theorem :: REWRITE3:4 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "P")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Set (Var "q1")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q2")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q1"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q2"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "q1")) "is" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set (Var "R"))) & (Bool (Set (Var "q2")) "is" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set (Var "R"))) ")" )))) ; theorem :: REWRITE3:5 (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 ($#k3_finseq_1 :::"len"::: ) (Set (Var "P"))) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool "ex" (Set (Var "Q")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set (Set ($#k9_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "Q"))) ($#r1_hidden :::"="::: ) (Set (Var "P"))) & (Bool (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "Q")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "P")))) ")" )))) ; theorem :: REWRITE3:6 (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 ($#k3_finseq_1 :::"len"::: ) (Set (Var "P"))) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool "ex" (Set (Var "Q")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set (Set (Var "Q")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "P")) ")" ) ")" ) ($#k9_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "P"))) & (Bool (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "Q")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "P")))) ")" )))) ; theorem :: REWRITE3:7 (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 ($#k3_finseq_1 :::"len"::: ) (Set (Var "P"))) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool "ex" (Set (Var "Q")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "Q")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "P")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "Q"))))) "holds" (Bool (Set (Set (Var "Q")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ))) ")" ) ")" )))) ; theorem :: REWRITE3:8 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "is" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set (Var "R")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))))) ; begin theorem :: REWRITE3:9 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "w")) "," (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 "w")) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "v"))))) "holds" (Bool "(" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "u"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "w")))) & (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "v"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "w")))) ")" ))) ; theorem :: REWRITE3:10 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "w")) "," (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 "w")) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "v")))) & (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")))) & (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))))) "holds" (Bool "(" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "u"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "w")))) & (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "v"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "w")))) ")" ))) ; theorem :: REWRITE3:11 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "w1")) "," (Set (Var "v1")) "," (Set (Var "w2")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Set (Var "w1")) ($#k1_flang_1 :::"^"::: ) (Set (Var "v1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "w2")) ($#k1_flang_1 :::"^"::: ) (Set (Var "v2")))) & (Bool "(" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "w1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "w2")))) "or" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "v1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "v2")))) ")" )) "holds" (Bool "(" (Bool (Set (Var "w1")) ($#r1_hidden :::"="::: ) (Set (Var "w2"))) & (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "v2"))) ")" ))) ; theorem :: REWRITE3:12 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "w1")) "," (Set (Var "v1")) "," (Set (Var "w2")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Set (Var "w1")) ($#k1_flang_1 :::"^"::: ) (Set (Var "v1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "w2")) ($#k1_flang_1 :::"^"::: ) (Set (Var "v2")))) & (Bool "(" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "w1"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "w2")))) "or" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "v1"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "v2")))) ")" )) "holds" (Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "w1")) ($#k1_flang_1 :::"^"::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set (Var "w2"))) & (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "v2")))) ")" )))) ; theorem :: REWRITE3:13 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "w1")) "," (Set (Var "v1")) "," (Set (Var "w2")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool "(" "not" (Bool (Set (Set (Var "w1")) ($#k1_flang_1 :::"^"::: ) (Set (Var "v1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "w2")) ($#k1_flang_1 :::"^"::: ) (Set (Var "v2")))) "or" (Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "w1")) ($#k1_flang_1 :::"^"::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set (Var "w2"))) & (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "v2")))) ")" )) "or" (Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "w2")) ($#k1_flang_1 :::"^"::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set (Var "w1"))) & (Bool (Set (Var "v2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "v1")))) ")" )) ")" ))) ; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; attr "c2" is :::"strict"::: ; struct :::"transition-system"::: "over" "X" -> ($#l1_struct_0 :::"1-sorted"::: ) ; aggr :::"transition-system":::(# :::"carrier":::, :::"Tran"::: #) -> ($#l1_rewrite3 :::"transition-system"::: ) "over" "X"; sel :::"Tran"::: "c2" -> ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c2") "," "X" ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c2"); end; definitionlet "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ); let "TS" be ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Const "F")); attr "TS" is :::"deterministic"::: means :: REWRITE3:def 1 (Bool "(" (Bool (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" "TS") "is" ($#m1_hidden :::"Function":::)) & (Bool (Bool "not" (Set ($#k2_flang_1 :::"<%>"::: ) "E") ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" "TS") ")" )))) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" "TS" (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "E" ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "v"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "s")) "," (Set (Var "u")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" "TS"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "s")) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" "TS")))) "holds" (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "E" ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool "(" (Bool (Bool "not" (Set (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Var "v")))) & (Bool (Bool "not" (Set (Set (Var "v")) ($#k1_flang_1 :::"^"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Var "u")))) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"deterministic"::: REWRITE3:def 1 : (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "holds" (Bool "(" (Bool (Set (Var "TS")) "is" ($#v2_rewrite3 :::"deterministic"::: ) ) "iff" (Bool "(" (Bool (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))) "is" ($#m1_hidden :::"Function":::)) & (Bool (Bool "not" (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))) ")" )))) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "TS")) (Bool "for" (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 "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "v"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "s")) "," (Set (Var "u")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "s")) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS")))))) "holds" (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool "(" (Bool (Bool "not" (Set (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Var "v")))) & (Bool (Bool "not" (Set (Set (Var "v")) ($#k1_flang_1 :::"^"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Var "u")))) ")" ))) ")" ) ")" ) ")" )))); theorem :: REWRITE3:14 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS")))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Var "TS")) "is" ($#v2_rewrite3 :::"deterministic"::: ) )))) ; registrationlet "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v1_rewrite3 :::"strict"::: ) ($#v2_rewrite3 :::"deterministic"::: ) for ($#l1_rewrite3 :::"transition-system"::: ) "over" "F"; end; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "TS" be ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Const "X")); let "x", "y", "z" be ($#m1_hidden :::"set"::: ) ; pred "x" "," "y" :::"-->."::: "z" "," "TS" means :: REWRITE3:def 2 (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) "x" "," "y" ($#k4_tarski :::"]"::: ) ) "," "z" ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" "TS")); end; :: deftheorem defines :::"-->."::: REWRITE3:def 2 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "TS")) "being" ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "X")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_rewrite3 :::"-->."::: ) (Set (Var "z")) "," (Set (Var "TS"))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS")))) ")" )))); theorem :: REWRITE3:15 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "TS")) "being" ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_rewrite3 :::"-->."::: ) (Set (Var "z")) "," (Set (Var "TS")))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Var "TS"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "z")) ($#r1_struct_0 :::"in"::: ) (Set (Var "TS"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))) ")" ))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))) ")" ))) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))))) ")" ))) ; theorem :: REWRITE3:16 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "TS1")) "being" ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "X1")) (Bool "for" (Set (Var "TS2")) "being" ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "X2")) "st" (Bool (Bool (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS2")))) & (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_rewrite3 :::"-->."::: ) (Set (Var "z")) "," (Set (Var "TS1")))) "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_rewrite3 :::"-->."::: ) (Set (Var "z")) "," (Set (Var "TS2")))))) ; theorem :: REWRITE3:17 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))) "is" ($#m1_hidden :::"Function":::)) & (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_rewrite3 :::"-->."::: ) (Set (Var "z1")) "," (Set (Var "TS"))) & (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_rewrite3 :::"-->."::: ) (Set (Var "z2")) "," (Set (Var "TS")))) "holds" (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Var "z2"))))))) ; theorem :: REWRITE3:18 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Bool "not" (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))) ")" ))))) "holds" (Bool "not" (Bool (Set (Var "x")) "," (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r1_rewrite3 :::"-->."::: ) (Set (Var "y")) "," (Set (Var "TS")))))))) ; theorem :: REWRITE3:19 (Bool "for" (Set (Var "x")) "," (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#v2_rewrite3 :::"deterministic"::: ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "v"))) & (Bool (Set (Var "x")) "," (Set (Var "u")) ($#r1_rewrite3 :::"-->."::: ) (Set (Var "z1")) "," (Set (Var "TS"))) & (Bool (Set (Var "x")) "," (Set (Var "v")) ($#r1_rewrite3 :::"-->."::: ) (Set (Var "z2")) "," (Set (Var "TS")))) "holds" (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool "(" (Bool (Bool "not" (Set (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Var "v")))) & (Bool (Bool "not" (Set (Set (Var "v")) ($#k1_flang_1 :::"^"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Var "u")))) ")" ))))))) ; begin definitionlet "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ); let "TS" be ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Const "F")); let "x1", "x2", "y1", "y2" be ($#m1_hidden :::"set"::: ) ; pred "x1" "," "x2" :::"==>."::: "y1" "," "y2" "," "TS" means :: REWRITE3:def 3 (Bool "ex" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "E" ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool "(" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) "y2") & (Bool "x1" "," (Set (Var "w")) ($#r1_rewrite3 :::"-->."::: ) "y1" "," "TS") & (Bool "x2" ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k1_flang_1 :::"^"::: ) (Set (Var "v")))) ")" )); end; :: deftheorem defines :::"==>."::: REWRITE3:def 3 : (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r2_rewrite3 :::"==>."::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "TS"))) "iff" (Bool "ex" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool "(" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) & (Bool (Set (Var "x1")) "," (Set (Var "w")) ($#r1_rewrite3 :::"-->."::: ) (Set (Var "y1")) "," (Set (Var "TS"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k1_flang_1 :::"^"::: ) (Set (Var "v")))) ")" )) ")" ))))); theorem :: REWRITE3:20 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r2_rewrite3 :::"==>."::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "TS")))) "holds" (Bool "(" (Bool (Set (Var "x1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "TS"))) & (Bool (Set (Var "y1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "TS"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) )) & (Bool (Set (Var "y2")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) )) & (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))) ")" ))) & (Bool (Set (Var "y1")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))))) ")" ))))) ; theorem :: REWRITE3:21 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS1")) "being" ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F1")) (Bool "for" (Set (Var "TS2")) "being" ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F2")) "st" (Bool (Bool (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS2")))) & (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r2_rewrite3 :::"==>."::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "TS1")))) "holds" (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r2_rewrite3 :::"==>."::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "TS2")))))))) ; theorem :: REWRITE3:22 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "u")) ($#r2_rewrite3 :::"==>."::: ) (Set (Var "y")) "," (Set (Var "v")) "," (Set (Var "TS")))) "holds" (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "w")) ($#r1_rewrite3 :::"-->."::: ) (Set (Var "y")) "," (Set (Var "TS"))) & (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k1_flang_1 :::"^"::: ) (Set (Var "v")))) ")" ))))))) ; theorem :: REWRITE3:23 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_rewrite3 :::"-->."::: ) (Set (Var "z")) "," (Set (Var "TS"))) "iff" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_rewrite3 :::"==>."::: ) (Set (Var "z")) "," (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) "," (Set (Var "TS"))) ")" ))))) ; theorem :: REWRITE3:24 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "v")) ($#r1_rewrite3 :::"-->."::: ) (Set (Var "y")) "," (Set (Var "TS"))) "iff" (Bool (Set (Var "x")) "," (Set (Set (Var "v")) ($#k1_flang_1 :::"^"::: ) (Set (Var "w"))) ($#r2_rewrite3 :::"==>."::: ) (Set (Var "y")) "," (Set (Var "w")) "," (Set (Var "TS"))) ")" )))))) ; theorem :: REWRITE3:25 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "u")) ($#r2_rewrite3 :::"==>."::: ) (Set (Var "y")) "," (Set (Var "v")) "," (Set (Var "TS")))) "holds" (Bool (Set (Var "x")) "," (Set (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "w"))) ($#r2_rewrite3 :::"==>."::: ) (Set (Var "y")) "," (Set (Set (Var "v")) ($#k1_flang_1 :::"^"::: ) (Set (Var "w"))) "," (Set (Var "TS")))))))) ; theorem :: REWRITE3:26 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "u")) ($#r2_rewrite3 :::"==>."::: ) (Set (Var "y")) "," (Set (Var "v")) "," (Set (Var "TS")))) "holds" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "u"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "v"))))))))) ; theorem :: REWRITE3:27 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "z")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))) "is" ($#m1_hidden :::"Function":::)) & (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r2_rewrite3 :::"==>."::: ) (Set (Var "y1")) "," (Set (Var "z")) "," (Set (Var "TS"))) & (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r2_rewrite3 :::"==>."::: ) (Set (Var "y2")) "," (Set (Var "z")) "," (Set (Var "TS")))) "holds" (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))))))) ; theorem :: REWRITE3:28 (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Bool "not" (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))) ")" ))))) "holds" (Bool "not" (Bool (Set (Var "x")) "," (Set (Var "z")) ($#r2_rewrite3 :::"==>."::: ) (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "TS")))))))) ; theorem :: REWRITE3:29 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Bool "not" (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))) ")" )))) & (Bool (Set (Var "x")) "," (Set (Var "u")) ($#r2_rewrite3 :::"==>."::: ) (Set (Var "y")) "," (Set (Var "v")) "," (Set (Var "TS")))) "holds" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "u"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "v"))))))))) ; theorem :: REWRITE3:30 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "z1")) "," (Set (Var "y2")) "," (Set (Var "z2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#v2_rewrite3 :::"deterministic"::: ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r2_rewrite3 :::"==>."::: ) (Set (Var "y1")) "," (Set (Var "z1")) "," (Set (Var "TS"))) & (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r2_rewrite3 :::"==>."::: ) (Set (Var "y2")) "," (Set (Var "z2")) "," (Set (Var "TS")))) "holds" (Bool "(" (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) & (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Var "z2"))) ")" ))))) ; begin definitionlet "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ); let "TS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Const "F")); func :::"==>.-relation"::: "TS" -> ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "TS") "," (Set "(" "E" ($#k8_afinsq_1 :::"^omega"::: ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) means :: REWRITE3:def 4 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r2_rewrite3 :::"==>."::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," "TS") ")" )); end; :: deftheorem defines :::"==>.-relation"::: REWRITE3:def 4 : (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "TS"))) "," (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS")))) "iff" (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r2_rewrite3 :::"==>."::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "TS"))) ")" )) ")" ))))); theorem :: REWRITE3:31 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))))) "holds" (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "TS"))(Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) )(Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "TS"))(Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "s")) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "t")) "," (Set (Var "w")) ($#k4_tarski :::"]"::: ) )) ")" ))))))))) ; theorem :: REWRITE3:32 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))))) "holds" (Bool "(" (Bool (Set (Var "x1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "TS"))) & (Bool (Set (Var "y1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "TS"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) )) & (Bool (Set (Var "y2")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) )) & (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))) ")" ))) & (Bool (Set (Var "y1")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))))) ")" ))))) ; theorem :: REWRITE3:33 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))))) "holds" (Bool "ex" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "TS"))(Bool "ex" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "s")) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "t")) "," (Set (Var "w")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) )))))))) ; theorem :: REWRITE3:34 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F1")) (Bool "for" (Set (Var "TS2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F2")) "st" (Bool (Bool (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS2"))))) "holds" (Bool (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS2")))))))) ; theorem :: REWRITE3:35 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))))) "holds" (Bool "ex" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool "(" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) & (Bool (Set (Var "x1")) "," (Set (Var "w")) ($#r1_rewrite3 :::"-->."::: ) (Set (Var "y1")) "," (Set (Var "TS"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k1_flang_1 :::"^"::: ) (Set (Var "v")))) ")" )))))) ; theorem :: REWRITE3:36 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "u")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))))) "holds" (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "w")) ($#r1_rewrite3 :::"-->."::: ) (Set (Var "y")) "," (Set (Var "TS"))) & (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k1_flang_1 :::"^"::: ) (Set (Var "v")))) ")" ))))))) ; theorem :: REWRITE3:37 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_rewrite3 :::"-->."::: ) (Set (Var "z")) "," (Set (Var "TS"))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS")))) ")" ))))) ; theorem :: REWRITE3:38 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "v")) ($#r1_rewrite3 :::"-->."::: ) (Set (Var "y")) "," (Set (Var "TS"))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set "(" (Set (Var "v")) ($#k1_flang_1 :::"^"::: ) (Set (Var "w")) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "w")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS")))) ")" )))))) ; theorem :: REWRITE3:39 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "u")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set "(" (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "w")) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set "(" (Set (Var "v")) ($#k1_flang_1 :::"^"::: ) (Set (Var "w")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))))))))) ; theorem :: REWRITE3:40 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "u")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))))) "holds" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "u"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "v"))))))))) ; theorem :: REWRITE3:41 (Bool "for" (Set (Var "x")) "," (Set (Var "y1")) "," (Set (Var "z")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))) "is" ($#m1_hidden :::"Function":::)) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y1")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y2")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))))) "holds" (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))))))) ; theorem :: REWRITE3:42 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Bool "not" (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))) ")" )))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "u")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))))) "holds" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "u"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "v"))))))))) ; theorem :: REWRITE3:43 (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Bool "not" (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))) ")" ))))) "holds" (Bool "not" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))))))))) ; theorem :: REWRITE3:44 (Bool "for" (Set (Var "x")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set (Var "TS")) "is" ($#v2_rewrite3 :::"deterministic"::: ) ) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))))) "holds" (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))))))) ; theorem :: REWRITE3:45 (Bool "for" (Set (Var "x")) "," (Set (Var "y1")) "," (Set (Var "z1")) "," (Set (Var "y2")) "," (Set (Var "z2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set (Var "TS")) "is" ($#v2_rewrite3 :::"deterministic"::: ) ) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y1")) "," (Set (Var "z1")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y2")) "," (Set (Var "z2")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))))) "holds" (Bool "(" (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) & (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Var "z2"))) ")" ))))) ; theorem :: REWRITE3:46 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set (Var "TS")) "is" ($#v2_rewrite3 :::"deterministic"::: ) )) "holds" (Bool (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) "is" ($#v1_funct_1 :::"Function-like"::: ) )))) ; begin definitionlet "x" be ($#m1_hidden :::"set"::: ) ; let "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"dim2"::: "(" "x" "," "E" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set "E" ($#k8_afinsq_1 :::"^omega"::: ) ) equals :: REWRITE3:def 5 (Set "x" ($#k2_xtuple_0 :::"`2"::: ) ) if (Bool "ex" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "E" ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "u")) ($#k4_tarski :::"]"::: ) )))) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"dim2"::: REWRITE3:def 5 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool "ex" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "u")) ($#k4_tarski :::"]"::: ) ))))) "implies" (Bool (Set ($#k2_rewrite3 :::"dim2"::: ) "(" (Set (Var "x")) "," (Set (Var "E")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`2"::: ) )) ")" & "(" (Bool (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "u")) ($#k4_tarski :::"]"::: ) )))) ")" )) "implies" (Bool (Set ($#k2_rewrite3 :::"dim2"::: ) "(" (Set (Var "x")) "," (Set (Var "E")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" ))); theorem :: REWRITE3:47 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) (Bool "for" (Set (Var "P")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "P")))) & (Bool (Set (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "P"))))) "holds" (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "TS"))(Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) )(Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "TS"))(Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "s")) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "t")) "," (Set (Var "w")) ($#k4_tarski :::"]"::: ) )) ")" )))))))))) ; theorem :: REWRITE3:48 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) (Bool "for" (Set (Var "P")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "P")))) & (Bool (Set (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "P"))))) "holds" (Bool "(" (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k4_tarski :::"]"::: ) )) ")" )))))) ; theorem :: REWRITE3:49 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) (Bool "for" (Set (Var "P")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "P")))) & (Bool (Set (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "P"))))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_struct_0 :::"in"::: ) (Set (Var "TS"))) & (Bool (Set (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) )) & (Bool (Set (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_struct_0 :::"in"::: ) (Set (Var "TS"))) & (Bool (Set (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) )) & (Bool (Set (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))) ")" ))) & (Bool (Set (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))))) ")" )))))) ; theorem :: REWRITE3:50 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F1")) (Bool "for" (Set (Var "TS2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F2")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "TS1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "TS2")))) & (Bool (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS2"))))) "holds" (Bool "for" (Set (Var "P")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS1"))) "holds" (Bool (Set (Var "P")) "is" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS2"))))))))) ; theorem :: REWRITE3:51 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) (Bool "for" (Set (Var "P")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) "st" (Bool (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "u")) ($#k4_tarski :::"]"::: ) ))))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "P"))))) "holds" (Bool (Set ($#k2_rewrite3 :::"dim2"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) "," (Set (Var "E")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ))))))) ; theorem :: REWRITE3:52 (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) (Bool "for" (Set (Var "P")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) "st" (Bool (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "P")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "w")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "P"))))) "holds" (Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Set (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "w")))))))))))) ; theorem :: REWRITE3:53 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) (Bool "for" (Set (Var "P")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) "st" (Bool (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "P")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "w")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "w"))))))))))) ; theorem :: REWRITE3:54 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) (Bool "for" (Set (Var "P")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) "st" (Bool (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "u")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "P")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "u")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "P"))))) "holds" (Bool (Set (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "u")))))))))) ; theorem :: REWRITE3:55 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) (Bool "for" (Set (Var "P")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "P")))) & (Bool (Set (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "P"))))) "holds" (Bool "ex" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool "(" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) )) & (Bool (Set (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) "," (Set (Var "w")) ($#r1_rewrite3 :::"-->."::: ) (Set (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) "," (Set (Var "TS"))) & (Bool (Set (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k1_flang_1 :::"^"::: ) (Set (Var "v")))) ")" ))))))) ; theorem :: REWRITE3:56 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) (Bool "for" (Set (Var "P")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "P")))) & (Bool (Set (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "P")))) & (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "u")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "w")) ($#r1_rewrite3 :::"-->."::: ) (Set (Var "y")) "," (Set (Var "TS"))) & (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k1_flang_1 :::"^"::: ) (Set (Var "v")))) ")" ))))))))) ; theorem :: REWRITE3:57 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_rewrite3 :::"-->."::: ) (Set (Var "z")) "," (Set (Var "TS"))) "iff" (Bool (Set ($#k10_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#k10_finseq_1 :::"*>"::: ) ) "is" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS")))) ")" ))))) ; theorem :: REWRITE3:58 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "v")) ($#r1_rewrite3 :::"-->."::: ) (Set (Var "y")) "," (Set (Var "TS"))) "iff" (Bool (Set ($#k10_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set "(" (Set (Var "v")) ($#k1_flang_1 :::"^"::: ) (Set (Var "w")) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "w")) ($#k4_tarski :::"]"::: ) ) ($#k10_finseq_1 :::"*>"::: ) ) "is" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS")))) ")" )))))) ; theorem :: REWRITE3:59 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) (Bool "for" (Set (Var "P")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) "st" (Bool (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "P")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "w")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "v"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "w")))))))))) ; theorem :: REWRITE3:60 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Bool "not" (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))) ")" ))))) "holds" (Bool "for" (Set (Var "P")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) "st" (Bool (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "u")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "P")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "u")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ))))))) ; theorem :: REWRITE3:61 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Bool "not" (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))) ")" ))))) "holds" (Bool "for" (Set (Var "P")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) "st" (Bool (Bool (Set (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "P")) ")" ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Num 1)))))) ; theorem :: REWRITE3:62 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Bool "not" (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))) ")" ))))) "holds" (Bool "for" (Set (Var "P")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) "st" (Bool (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "u")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "P")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "P"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k1_afinsq_1 :::"len"::: ) (Set (Var "u")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1))))))))) ; theorem :: REWRITE3:63 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Bool "not" (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))) ")" ))))) "holds" (Bool "for" (Set (Var "P")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) "st" (Bool (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set ($#k3_flang_1 :::"<%"::: ) (Set (Var "e")) ($#k3_flang_1 :::"%>"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "P")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Num 2)))))))) ; theorem :: REWRITE3:64 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Bool "not" (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))) ")" ))))) "holds" (Bool "for" (Set (Var "P")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) "st" (Bool (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "P")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "w")) ($#k4_tarski :::"]"::: ) )) & (Bool (Bool "not" (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "v"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "w")))))) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "w"))) ")" ))))))) ; theorem :: REWRITE3:65 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Bool "not" (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))) ")" ))))) "holds" (Bool "for" (Set (Var "P")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "P")))) & (Bool (Set (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "P"))))) "holds" (Bool (Set (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ))))))) ; theorem :: REWRITE3:66 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Bool "not" (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))) ")" ))))) "holds" (Bool "for" (Set (Var "P")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) (Bool "for" (Set (Var "k")) "," (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "P")))) & (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "P")))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "l")))) "holds" (Bool (Set (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "l")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ))))))) ; theorem :: REWRITE3:67 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set (Var "TS")) "is" ($#v2_rewrite3 :::"deterministic"::: ) )) "holds" (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) "st" (Bool (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "Q")) ($#k1_funct_1 :::"."::: ) (Num 1)))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "P")))) & (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "Q"))))) "holds" (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "Q")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))))))))) ; theorem :: REWRITE3:68 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set (Var "TS")) "is" ($#v2_rewrite3 :::"deterministic"::: ) )) "holds" (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) "st" (Bool (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "Q")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "Q"))))) "holds" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Var "Q"))))))) ; theorem :: REWRITE3:69 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set (Var "TS")) "is" ($#v2_rewrite3 :::"deterministic"::: ) )) "holds" (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) "st" (Bool (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "Q")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "P")) ")" ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "Q")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "Q")) ")" ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ))) "holds" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Var "Q"))))))) ; begin theorem :: REWRITE3:70 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) ($#r1_rewrite1 :::"reduces"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "w")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "w")))))))))) ; theorem :: REWRITE3:71 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) ($#r1_rewrite1 :::"reduces"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "u")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) ($#r1_rewrite1 :::"reduces"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set "(" (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "w")) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set "(" (Set (Var "v")) ($#k1_flang_1 :::"^"::: ) (Set (Var "w")) ")" ) ($#k4_tarski :::"]"::: ) ))))))) ; theorem :: REWRITE3:72 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_rewrite3 :::"-->."::: ) (Set (Var "z")) "," (Set (Var "TS")))) "holds" (Bool (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) ($#r1_rewrite1 :::"reduces"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_tarski :::"]"::: ) )))))) ; theorem :: REWRITE3:73 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "v")) ($#r1_rewrite3 :::"-->."::: ) (Set (Var "y")) "," (Set (Var "TS")))) "holds" (Bool (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) ($#r1_rewrite1 :::"reduces"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set "(" (Set (Var "v")) ($#k1_flang_1 :::"^"::: ) (Set (Var "w")) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "w")) ($#k4_tarski :::"]"::: ) ))))))) ; theorem :: REWRITE3:74 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r2_rewrite3 :::"==>."::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "TS")))) "holds" (Bool (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) ($#r1_rewrite1 :::"reduces"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) )))))) ; theorem :: REWRITE3:75 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) ($#r1_rewrite1 :::"reduces"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "w")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "v"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "w"))))))))) ; theorem :: REWRITE3:76 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "w")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) ($#r1_rewrite1 :::"reduces"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "w")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set "(" (Set (Var "v")) ($#k1_flang_1 :::"^"::: ) (Set (Var "w")) ")" ) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))))))))) ; theorem :: REWRITE3:77 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "holds" (Bool "(" (Bool (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))) ")" ))) "or" "not" (Bool (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) ($#r1_rewrite1 :::"reduces"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "w")) ($#k4_tarski :::"]"::: ) )) "or" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "v"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "w")))) "or" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "w"))) ")" ) ")" )))))) ; theorem :: REWRITE3:78 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Bool "not" (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))) ")" )))) & (Bool (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) ($#r1_rewrite1 :::"reduces"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "u")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "u")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))))))) ; theorem :: REWRITE3:79 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Bool "not" (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))) ")" )))) & (Bool (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) ($#r1_rewrite1 :::"reduces"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set ($#k3_flang_1 :::"<%"::: ) (Set (Var "e")) ($#k3_flang_1 :::"%>"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set ($#k3_flang_1 :::"<%"::: ) (Set (Var "e")) ($#k3_flang_1 :::"%>"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))))))))) ; theorem :: REWRITE3:80 (Bool "for" (Set (Var "x")) "," (Set (Var "y1")) "," (Set (Var "z")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set (Var "TS")) "is" ($#v2_rewrite3 :::"deterministic"::: ) ) & (Bool (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "x")) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y1")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "x")) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y2")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))))))) ; begin definitionlet "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ); let "TS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Const "F")); let "x1", "x2", "y1", "y2" be ($#m1_hidden :::"set"::: ) ; pred "x1" "," "x2" :::"==>*"::: "y1" "," "y2" "," "TS" means :: REWRITE3:def 6 (Bool (Set ($#k1_rewrite3 :::"==>.-relation"::: ) "TS") ($#r1_rewrite1 :::"reduces"::: ) (Set ($#k4_tarski :::"["::: ) "x1" "," "x2" ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) "y1" "," "y2" ($#k4_tarski :::"]"::: ) )); end; :: deftheorem defines :::"==>*"::: REWRITE3:def 6 : (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r3_rewrite3 :::"==>*"::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "TS"))) "iff" (Bool (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) ($#r1_rewrite1 :::"reduces"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) )) ")" ))))); theorem :: REWRITE3:81 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F1")) (Bool "for" (Set (Var "TS2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F2")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "TS1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "TS2")))) & (Bool (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS2")))) & (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r3_rewrite3 :::"==>*"::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "TS1")))) "holds" (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r3_rewrite3 :::"==>*"::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "TS2")))))))) ; theorem :: REWRITE3:82 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r3_rewrite3 :::"==>*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "TS"))))))) ; theorem :: REWRITE3:83 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r3_rewrite3 :::"==>*"::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "TS"))) & (Bool (Set (Var "y1")) "," (Set (Var "y2")) ($#r3_rewrite3 :::"==>*"::: ) (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "TS")))) "holds" (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r3_rewrite3 :::"==>*"::: ) (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "TS"))))))) ; theorem :: REWRITE3:84 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_rewrite3 :::"-->."::: ) (Set (Var "z")) "," (Set (Var "TS")))) "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r3_rewrite3 :::"==>*"::: ) (Set (Var "z")) "," (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) "," (Set (Var "TS"))))))) ; theorem :: REWRITE3:85 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "v")) ($#r1_rewrite3 :::"-->."::: ) (Set (Var "y")) "," (Set (Var "TS")))) "holds" (Bool (Set (Var "x")) "," (Set (Set (Var "v")) ($#k1_flang_1 :::"^"::: ) (Set (Var "w"))) ($#r3_rewrite3 :::"==>*"::: ) (Set (Var "y")) "," (Set (Var "w")) "," (Set (Var "TS")))))))) ; theorem :: REWRITE3:86 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "u")) ($#r3_rewrite3 :::"==>*"::: ) (Set (Var "y")) "," (Set (Var "v")) "," (Set (Var "TS")))) "holds" (Bool (Set (Var "x")) "," (Set (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "w"))) ($#r3_rewrite3 :::"==>*"::: ) (Set (Var "y")) "," (Set (Set (Var "v")) ($#k1_flang_1 :::"^"::: ) (Set (Var "w"))) "," (Set (Var "TS")))))))) ; theorem :: REWRITE3:87 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r2_rewrite3 :::"==>."::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "TS")))) "holds" (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r3_rewrite3 :::"==>*"::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "TS"))))))) ; theorem :: REWRITE3:88 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "v")) ($#r3_rewrite3 :::"==>*"::: ) (Set (Var "y")) "," (Set (Var "w")) "," (Set (Var "TS")))) "holds" (Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "w")))))))))) ; theorem :: REWRITE3:89 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "v")) ($#r3_rewrite3 :::"==>*"::: ) (Set (Var "y")) "," (Set (Var "w")) "," (Set (Var "TS")))) "holds" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "w"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "v"))))))))) ; theorem :: REWRITE3:90 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "w")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "w")) ($#r3_rewrite3 :::"==>*"::: ) (Set (Var "y")) "," (Set (Set (Var "v")) ($#k1_flang_1 :::"^"::: ) (Set (Var "w"))) "," (Set (Var "TS")))) "holds" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))))))))) ; theorem :: REWRITE3:91 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Bool "not" (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))) ")" ))))) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "u")) ($#r3_rewrite3 :::"==>*"::: ) (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "TS"))) "iff" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" )))))) ; theorem :: REWRITE3:92 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Bool "not" (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))) ")" )))) & (Bool (Set (Var "x")) "," (Set ($#k3_flang_1 :::"<%"::: ) (Set (Var "e")) ($#k3_flang_1 :::"%>"::: ) ) ($#r3_rewrite3 :::"==>*"::: ) (Set (Var "y")) "," (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) "," (Set (Var "TS")))) "holds" (Bool (Set (Var "x")) "," (Set ($#k3_flang_1 :::"<%"::: ) (Set (Var "e")) ($#k3_flang_1 :::"%>"::: ) ) ($#r2_rewrite3 :::"==>."::: ) (Set (Var "y")) "," (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) "," (Set (Var "TS")))))))) ; theorem :: REWRITE3:93 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "z")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set (Var "TS")) "is" ($#v2_rewrite3 :::"deterministic"::: ) ) & (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r3_rewrite3 :::"==>*"::: ) (Set (Var "y1")) "," (Set (Var "z")) "," (Set (Var "TS"))) & (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r3_rewrite3 :::"==>*"::: ) (Set (Var "y2")) "," (Set (Var "z")) "," (Set (Var "TS")))) "holds" (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))))))) ; begin definitionlet "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ); let "TS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Const "F")); let "x1", "x2", "y" be ($#m1_hidden :::"set"::: ) ; pred "x1" "," "x2" :::"==>*"::: "y" "," "TS" means :: REWRITE3:def 7 (Bool "x1" "," "x2" ($#r3_rewrite3 :::"==>*"::: ) "y" "," (Set ($#k2_flang_1 :::"<%>"::: ) "E") "," "TS"); end; :: deftheorem defines :::"==>*"::: REWRITE3:def 7 : (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r4_rewrite3 :::"==>*"::: ) (Set (Var "y")) "," (Set (Var "TS"))) "iff" (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r3_rewrite3 :::"==>*"::: ) (Set (Var "y")) "," (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) "," (Set (Var "TS"))) ")" ))))); theorem :: REWRITE3:94 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F1")) (Bool "for" (Set (Var "TS2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F2")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "TS1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "TS2")))) & (Bool (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS2")))) & (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r4_rewrite3 :::"==>*"::: ) (Set (Var "z")) "," (Set (Var "TS1")))) "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r4_rewrite3 :::"==>*"::: ) (Set (Var "z")) "," (Set (Var "TS2")))))))) ; theorem :: REWRITE3:95 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "holds" (Bool (Set (Var "x")) "," (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r4_rewrite3 :::"==>*"::: ) (Set (Var "x")) "," (Set (Var "TS"))))))) ; theorem :: REWRITE3:96 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "u")) ($#r4_rewrite3 :::"==>*"::: ) (Set (Var "y")) "," (Set (Var "TS")))) "holds" (Bool (Set (Var "x")) "," (Set (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "v"))) ($#r3_rewrite3 :::"==>*"::: ) (Set (Var "y")) "," (Set (Var "v")) "," (Set (Var "TS")))))))) ; theorem :: REWRITE3:97 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_rewrite3 :::"-->."::: ) (Set (Var "z")) "," (Set (Var "TS")))) "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r4_rewrite3 :::"==>*"::: ) (Set (Var "z")) "," (Set (Var "TS"))))))) ; theorem :: REWRITE3:98 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r2_rewrite3 :::"==>."::: ) (Set (Var "y")) "," (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) "," (Set (Var "TS")))) "holds" (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r4_rewrite3 :::"==>*"::: ) (Set (Var "y")) "," (Set (Var "TS"))))))) ; theorem :: REWRITE3:99 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "u")) ($#r4_rewrite3 :::"==>*"::: ) (Set (Var "y")) "," (Set (Var "TS"))) & (Bool (Set (Var "y")) "," (Set (Var "v")) ($#r4_rewrite3 :::"==>*"::: ) (Set (Var "z")) "," (Set (Var "TS")))) "holds" (Bool (Set (Var "x")) "," (Set (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "v"))) ($#r4_rewrite3 :::"==>*"::: ) (Set (Var "z")) "," (Set (Var "TS")))))))) ; theorem :: REWRITE3:100 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Bool "not" (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))) ")" ))))) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r4_rewrite3 :::"==>*"::: ) (Set (Var "y")) "," (Set (Var "TS"))) "iff" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ))))) ; theorem :: REWRITE3:101 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Bool "not" (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))) ")" )))) & (Bool (Set (Var "x")) "," (Set ($#k3_flang_1 :::"<%"::: ) (Set (Var "e")) ($#k3_flang_1 :::"%>"::: ) ) ($#r4_rewrite3 :::"==>*"::: ) (Set (Var "y")) "," (Set (Var "TS")))) "holds" (Bool (Set (Var "x")) "," (Set ($#k3_flang_1 :::"<%"::: ) (Set (Var "e")) ($#k3_flang_1 :::"%>"::: ) ) ($#r2_rewrite3 :::"==>."::: ) (Set (Var "y")) "," (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) "," (Set (Var "TS")))))))) ; theorem :: REWRITE3:102 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) "st" (Bool (Bool (Set (Var "TS")) "is" ($#v2_rewrite3 :::"deterministic"::: ) ) & (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r4_rewrite3 :::"==>*"::: ) (Set (Var "y1")) "," (Set (Var "TS"))) & (Bool (Set (Var "x1")) "," (Set (Var "x2")) ($#r4_rewrite3 :::"==>*"::: ) (Set (Var "y2")) "," (Set (Var "TS")))) "holds" (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))))))) ; begin definitionlet "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ); let "TS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Const "F")); let "x", "X" be ($#m1_hidden :::"set"::: ) ; func "x" :::"-succ_of"::: "(" "X" "," "TS" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "TS" equals :: REWRITE3:def 8 "{" (Set (Var "s")) where s "is" ($#m1_subset_1 :::"Element":::) "of" "TS" : (Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" "TS" "st" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Var "t")) "," "x" ($#r4_rewrite3 :::"==>*"::: ) (Set (Var "s")) "," "TS") ")" )) "}" ; end; :: deftheorem defines :::"-succ_of"::: REWRITE3:def 8 : (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k3_rewrite3 :::"-succ_of"::: ) "(" (Set (Var "X")) "," (Set (Var "TS")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "s")) where s "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "TS")) : (Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "TS")) "st" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "t")) "," (Set (Var "x")) ($#r4_rewrite3 :::"==>*"::: ) (Set (Var "s")) "," (Set (Var "TS"))) ")" )) "}" ))))); theorem :: REWRITE3:103 (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "TS")) "holds" (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "x")) ($#k3_rewrite3 :::"-succ_of"::: ) "(" (Set (Var "X")) "," (Set (Var "TS")) ")" )) "iff" (Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "TS")) "st" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "t")) "," (Set (Var "x")) ($#r4_rewrite3 :::"==>*"::: ) (Set (Var "s")) "," (Set (Var "TS"))) ")" )) ")" )))))) ; theorem :: REWRITE3:104 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Bool "not" (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))) ")" ))))) "holds" (Bool (Set (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k3_rewrite3 :::"-succ_of"::: ) "(" (Set (Var "S")) "," (Set (Var "TS")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "S"))))))) ; theorem :: REWRITE3:105 (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "TS1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F1")) (Bool "for" (Set (Var "TS2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F2")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "TS1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "TS2")))) & (Bool (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS2"))))) "holds" (Bool (Set (Set (Var "x")) ($#k3_rewrite3 :::"-succ_of"::: ) "(" (Set (Var "X")) "," (Set (Var "TS1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k3_rewrite3 :::"-succ_of"::: ) "(" (Set (Var "X")) "," (Set (Var "TS2")) ")" ))))))) ;