:: FSM_3 semantic presentation begin theorem :: FSM_3:1 (Bool "for" (Set (Var "i")) "," (Set (Var "k")) "," (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "l"))))) "holds" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "k")))) ; theorem :: FSM_3:2 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool "(" (Bool (Set (Set (Var "a")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) "or" (Bool (Set (Set (Var "b")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" )) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: FSM_3:3 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "q")))))) ; theorem :: FSM_3:4 (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"::: ) ) "st" (Bool (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "st" (Bool "(" (Bool (Set ($#k3_flang_1 :::"<%"::: ) (Set (Var "e")) ($#k3_flang_1 :::"%>"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "u"))) & (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) ")" )))) ; theorem :: FSM_3:5 (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 "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "u"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)))) "holds" (Bool "ex" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool "(" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "v1"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "v2"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v1")) ($#k1_flang_1 :::"^"::: ) (Set (Var "v2")))) ")" ))))) ; theorem :: FSM_3:6 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"XFinSequence":::) "st" (Bool (Bool (Set (Set ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) ) ($#k1_ordinal4 :::"^"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "y")) ($#k5_afinsq_1 :::"%>"::: ) ) ($#k1_ordinal4 :::"^"::: ) (Set (Var "q"))))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) ")" ))) ; theorem :: FSM_3:7 (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"::: ) ) "st" (Bool (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "u"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E"))(Bool "ex" (Set (Var "u1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set ($#k3_flang_1 :::"<%"::: ) (Set (Var "e")) ($#k3_flang_1 :::"%>"::: ) ) ($#k1_flang_1 :::"^"::: ) (Set (Var "u1")))))))) ; registrationlet "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k9_flang_1 :::"Lex"::: ) "E") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: FSM_3:8 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Bool "not" (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E")))))) ; theorem :: FSM_3:9 (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"::: ) ) "holds" (Bool "(" (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E")))) "iff" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ))) ; theorem :: FSM_3:10 (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"::: ) ) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "v"))) & (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E")))) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E"))))) "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 "w")) ($#k1_flang_1 :::"^"::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set (Var "v")))) ")" )))) ; theorem :: FSM_3:11 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "TS")) "being" ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E"))) "st" (Bool (Bool (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "TS"))) "is" ($#m1_hidden :::"Function":::))) "holds" (Bool (Set (Var "TS")) "is" ($#v2_rewrite3 :::"deterministic"::: ) ))) ; 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 :::"_bool"::: "TS" -> ($#v1_rewrite3 :::"strict"::: ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set ($#k9_flang_1 :::"Lex"::: ) "E") means :: FSM_3:def 1 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "TS"))) & (Bool "(" "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" "TS" (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "E" ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" "TS" "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "S")) "," (Set (Var "w")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "T")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" it)) "iff" (Bool "(" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k3_rewrite3 :::"-succ_of"::: ) "(" (Set (Var "S")) "," "TS" ")" )) ")" ) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"_bool"::: FSM_3: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" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Var "F")) (Bool "for" (Set (Var "b4")) "being" ($#v1_rewrite3 :::"strict"::: ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E"))) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_fsm_3 :::"_bool"::: ) (Set (Var "TS")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "TS"))))) & (Bool "(" "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "S")) "," (Set (Var "w")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "T")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "b4")))) "iff" (Bool "(" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k3_rewrite3 :::"-succ_of"::: ) "(" (Set (Var "S")) "," (Set (Var "TS")) ")" )) ")" ) ")" ))) ")" ) ")" ) ")" ))))); 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"::: ) ")" ); let "TS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Const "F")); cluster (Set ($#k1_fsm_3 :::"_bool"::: ) "TS") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_rewrite3 :::"strict"::: ) ($#v2_rewrite3 :::"deterministic"::: ) ; end; 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"::: ) ")" ); let "TS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Const "F")); cluster (Set ($#k1_fsm_3 :::"_bool"::: ) "TS") -> ($#v8_struct_0 :::"finite"::: ) ($#v1_rewrite3 :::"strict"::: ) ; end; theorem :: FSM_3:12 (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 (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 ($#k1_fsm_3 :::"_bool"::: ) (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 ($#k1_fsm_3 :::"_bool"::: ) (Set (Var "TS"))))))))) ; theorem :: FSM_3:13 (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 "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 "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k3_rewrite3 :::"-succ_of"::: ) "(" (Set (Var "S")) "," (Set (Var "TS")) ")" )) "iff" (Bool (Set (Var "S")) "," (Set (Var "w")) ($#r4_rewrite3 :::"==>*"::: ) (Set (Var "X")) "," (Set ($#k1_fsm_3 :::"_bool"::: ) (Set (Var "TS")))) ")" ))))))) ; 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"::: ) ")" ); attr "c3" is :::"strict"::: ; struct :::"semiautomaton"::: "over" "F" -> ($#l1_rewrite3 :::"transition-system"::: ) "over" "F"; aggr :::"semiautomaton":::(# :::"carrier":::, :::"Tran":::, :::"InitS"::: #) -> ($#l1_fsm_3 :::"semiautomaton"::: ) "over" "F"; sel :::"InitS"::: "c3" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c3"); 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 "SA" be ($#l1_fsm_3 :::"semiautomaton"::: ) "over" (Set (Const "F")); attr "SA" is :::"deterministic"::: means :: FSM_3:def 2 (Bool "(" (Bool (Set ($#g1_rewrite3 :::"transition-system"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "SA") "," (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" "SA") "#)" ) "is" ($#v2_rewrite3 :::"deterministic"::: ) ) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "the" ($#u1_fsm_3 :::"InitS"::: ) "of" "SA")) ($#r1_hidden :::"="::: ) (Num 1)) ")" ); end; :: deftheorem defines :::"deterministic"::: FSM_3:def 2 : (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 "SA")) "being" ($#l1_fsm_3 :::"semiautomaton"::: ) "over" (Set (Var "F")) "holds" (Bool "(" (Bool (Set (Var "SA")) "is" ($#v2_fsm_3 :::"deterministic"::: ) ) "iff" (Bool "(" (Bool (Set ($#g1_rewrite3 :::"transition-system"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "SA"))) "," (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "SA"))) "#)" ) "is" ($#v2_rewrite3 :::"deterministic"::: ) ) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "the" ($#u1_fsm_3 :::"InitS"::: ) "of" (Set (Var "SA")))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ")" )))); 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_fsm_3 :::"strict"::: ) ($#v2_fsm_3 :::"deterministic"::: ) for ($#l1_fsm_3 :::"semiautomaton"::: ) "over" "F"; end; 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"::: ) ")" ); let "SA" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_3 :::"semiautomaton"::: ) "over" (Set (Const "F")); cluster (Set ($#g1_rewrite3 :::"transition-system"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "SA") "," (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" "SA") "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; 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 "SA" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_3 :::"semiautomaton"::: ) "over" (Set (Const "F")); func :::"_bool"::: "SA" -> ($#v1_fsm_3 :::"strict"::: ) ($#l1_fsm_3 :::"semiautomaton"::: ) "over" (Set ($#k9_flang_1 :::"Lex"::: ) "E") means :: FSM_3:def 3 (Bool "(" (Bool (Set ($#g1_rewrite3 :::"transition-system"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) "," (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" it) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#k1_fsm_3 :::"_bool"::: ) (Set ($#g1_rewrite3 :::"transition-system"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "SA") "," (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" "SA") "#)" ))) & (Bool (Set "the" ($#u1_fsm_3 :::"InitS"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set "(" ($#k2_flang_1 :::"<%>"::: ) "E" ")" ) ($#k3_rewrite3 :::"-succ_of"::: ) "(" (Set "the" ($#u1_fsm_3 :::"InitS"::: ) "of" "SA") "," "SA" ")" ")" ) ($#k6_domain_1 :::"}"::: ) )) ")" ); end; :: deftheorem defines :::"_bool"::: FSM_3: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 "SA")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_3 :::"semiautomaton"::: ) "over" (Set (Var "F")) (Bool "for" (Set (Var "b4")) "being" ($#v1_fsm_3 :::"strict"::: ) ($#l1_fsm_3 :::"semiautomaton"::: ) "over" (Set ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E"))) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_fsm_3 :::"_bool"::: ) (Set (Var "SA")))) "iff" (Bool "(" (Bool (Set ($#g1_rewrite3 :::"transition-system"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b4"))) "," (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "b4"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#k1_fsm_3 :::"_bool"::: ) (Set ($#g1_rewrite3 :::"transition-system"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "SA"))) "," (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "SA"))) "#)" ))) & (Bool (Set "the" ($#u1_fsm_3 :::"InitS"::: ) "of" (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k3_rewrite3 :::"-succ_of"::: ) "(" (Set "the" ($#u1_fsm_3 :::"InitS"::: ) "of" (Set (Var "SA"))) "," (Set (Var "SA")) ")" ")" ) ($#k6_domain_1 :::"}"::: ) )) ")" ) ")" ))))); 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"::: ) ")" ); let "SA" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_3 :::"semiautomaton"::: ) "over" (Set (Const "F")); cluster (Set ($#k2_fsm_3 :::"_bool"::: ) "SA") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_fsm_3 :::"strict"::: ) ($#v2_fsm_3 :::"deterministic"::: ) ; end; theorem :: FSM_3: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 "SA")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_3 :::"semiautomaton"::: ) "over" (Set (Var "F")) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k2_fsm_3 :::"_bool"::: ) (Set (Var "SA")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "SA")))))))) ; 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"::: ) ")" ); let "SA" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l1_fsm_3 :::"semiautomaton"::: ) "over" (Set (Const "F")); cluster (Set ($#k2_fsm_3 :::"_bool"::: ) "SA") -> ($#v8_struct_0 :::"finite"::: ) ($#v1_fsm_3 :::"strict"::: ) ; 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 "SA" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_3 :::"semiautomaton"::: ) "over" (Set (Const "F")); let "Q" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "SA")); func :::"left-Lang"::: "Q" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "E" ($#k8_afinsq_1 :::"^omega"::: ) ")" ) equals :: FSM_3:def 4 "{" (Set (Var "w")) where w "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set "E" ($#k8_afinsq_1 :::"^omega"::: ) ) : (Bool "Q" ($#r1_xboole_0 :::"meets"::: ) (Set (Set (Var "w")) ($#k3_rewrite3 :::"-succ_of"::: ) "(" (Set "the" ($#u1_fsm_3 :::"InitS"::: ) "of" "SA") "," "SA" ")" )) "}" ; end; :: deftheorem defines :::"left-Lang"::: FSM_3: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 "SA")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_3 :::"semiautomaton"::: ) "over" (Set (Var "F")) (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "SA")) "holds" (Bool (Set ($#k3_fsm_3 :::"left-Lang"::: ) (Set (Var "Q"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "w")) where w "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) : (Bool (Set (Var "Q")) ($#r1_xboole_0 :::"meets"::: ) (Set (Set (Var "w")) ($#k3_rewrite3 :::"-succ_of"::: ) "(" (Set "the" ($#u1_fsm_3 :::"InitS"::: ) "of" (Set (Var "SA"))) "," (Set (Var "SA")) ")" )) "}" ))))); theorem :: FSM_3:15 (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 "SA")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_3 :::"semiautomaton"::: ) "over" (Set (Var "F")) (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "SA")) "holds" (Bool "(" (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set ($#k3_fsm_3 :::"left-Lang"::: ) (Set (Var "Q")))) "iff" (Bool (Set (Var "Q")) ($#r1_xboole_0 :::"meets"::: ) (Set (Set (Var "w")) ($#k3_rewrite3 :::"-succ_of"::: ) "(" (Set "the" ($#u1_fsm_3 :::"InitS"::: ) "of" (Set (Var "SA"))) "," (Set (Var "SA")) ")" )) ")" )))))) ; 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"::: ) ")" ); attr "c3" is :::"strict"::: ; struct :::"automaton"::: "over" "F" -> ($#l1_fsm_3 :::"semiautomaton"::: ) "over" "F"; aggr :::"automaton":::(# :::"carrier":::, :::"Tran":::, :::"InitS":::, :::"FinalS"::: #) -> ($#l2_fsm_3 :::"automaton"::: ) "over" "F"; sel :::"FinalS"::: "c3" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c3"); 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 "A" be ($#l2_fsm_3 :::"automaton"::: ) "over" (Set (Const "F")); attr "A" is :::"deterministic"::: means :: FSM_3:def 5 (Bool (Set ($#g1_fsm_3 :::"semiautomaton"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A") "," (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" "A") "," (Set "the" ($#u1_fsm_3 :::"InitS"::: ) "of" "A") "#)" ) "is" ($#v2_fsm_3 :::"deterministic"::: ) ); end; :: deftheorem defines :::"deterministic"::: FSM_3:def 5 : (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 "A")) "being" ($#l2_fsm_3 :::"automaton"::: ) "over" (Set (Var "F")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v4_fsm_3 :::"deterministic"::: ) ) "iff" (Bool (Set ($#g1_fsm_3 :::"semiautomaton"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u1_fsm_3 :::"InitS"::: ) "of" (Set (Var "A"))) "#)" ) "is" ($#v2_fsm_3 :::"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"::: ) ($#v3_fsm_3 :::"strict"::: ) ($#v4_fsm_3 :::"deterministic"::: ) for ($#l2_fsm_3 :::"automaton"::: ) "over" "F"; end; 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"::: ) ")" ); let "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_3 :::"automaton"::: ) "over" (Set (Const "F")); cluster (Set ($#g1_rewrite3 :::"transition-system"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A") "," (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" "A") "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; cluster (Set ($#g1_fsm_3 :::"semiautomaton"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A") "," (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" "A") "," (Set "the" ($#u1_fsm_3 :::"InitS"::: ) "of" "A") "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; 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 "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_3 :::"automaton"::: ) "over" (Set (Const "F")); func :::"_bool"::: "A" -> ($#v3_fsm_3 :::"strict"::: ) ($#l2_fsm_3 :::"automaton"::: ) "over" (Set ($#k9_flang_1 :::"Lex"::: ) "E") means :: FSM_3:def 6 (Bool "(" (Bool (Set ($#g1_fsm_3 :::"semiautomaton"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) "," (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" it) "," (Set "the" ($#u1_fsm_3 :::"InitS"::: ) "of" it) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#k2_fsm_3 :::"_bool"::: ) (Set ($#g1_fsm_3 :::"semiautomaton"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A") "," (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" "A") "," (Set "the" ($#u1_fsm_3 :::"InitS"::: ) "of" "A") "#)" ))) & (Bool (Set "the" ($#u2_fsm_3 :::"FinalS"::: ) "of" it) ($#r1_hidden :::"="::: ) "{" (Set (Var "Q")) where Q "is" ($#m1_subset_1 :::"Element":::) "of" it : (Bool (Set (Var "Q")) ($#r1_xboole_0 :::"meets"::: ) (Set "the" ($#u2_fsm_3 :::"FinalS"::: ) "of" "A")) "}" ) ")" ); end; :: deftheorem defines :::"_bool"::: FSM_3: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 "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_3 :::"automaton"::: ) "over" (Set (Var "F")) (Bool "for" (Set (Var "b4")) "being" ($#v3_fsm_3 :::"strict"::: ) ($#l2_fsm_3 :::"automaton"::: ) "over" (Set ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E"))) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k4_fsm_3 :::"_bool"::: ) (Set (Var "A")))) "iff" (Bool "(" (Bool (Set ($#g1_fsm_3 :::"semiautomaton"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b4"))) "," (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "b4"))) "," (Set "the" ($#u1_fsm_3 :::"InitS"::: ) "of" (Set (Var "b4"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#k2_fsm_3 :::"_bool"::: ) (Set ($#g1_fsm_3 :::"semiautomaton"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u1_rewrite3 :::"Tran"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u1_fsm_3 :::"InitS"::: ) "of" (Set (Var "A"))) "#)" ))) & (Bool (Set "the" ($#u2_fsm_3 :::"FinalS"::: ) "of" (Set (Var "b4"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "Q")) where Q "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "b4")) : (Bool (Set (Var "Q")) ($#r1_xboole_0 :::"meets"::: ) (Set "the" ($#u2_fsm_3 :::"FinalS"::: ) "of" (Set (Var "A")))) "}" ) ")" ) ")" ))))); 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"::: ) ")" ); let "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_3 :::"automaton"::: ) "over" (Set (Const "F")); cluster (Set ($#k4_fsm_3 :::"_bool"::: ) "A") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_fsm_3 :::"strict"::: ) ($#v4_fsm_3 :::"deterministic"::: ) ; end; theorem :: FSM_3:16 (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 "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_3 :::"automaton"::: ) "over" (Set (Var "F")) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k4_fsm_3 :::"_bool"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A")))))))) ; 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"::: ) ")" ); let "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_3 :::"automaton"::: ) "over" (Set (Const "F")); cluster (Set ($#k4_fsm_3 :::"_bool"::: ) "A") -> ($#v8_struct_0 :::"finite"::: ) ($#v3_fsm_3 :::"strict"::: ) ; 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 "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_3 :::"automaton"::: ) "over" (Set (Const "F")); let "Q" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A")); func :::"right-Lang"::: "Q" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "E" ($#k8_afinsq_1 :::"^omega"::: ) ")" ) equals :: FSM_3:def 7 "{" (Set (Var "w")) where w "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set "E" ($#k8_afinsq_1 :::"^omega"::: ) ) : (Bool (Set (Set (Var "w")) ($#k3_rewrite3 :::"-succ_of"::: ) "(" "Q" "," "A" ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set "the" ($#u2_fsm_3 :::"FinalS"::: ) "of" "A")) "}" ; end; :: deftheorem defines :::"right-Lang"::: FSM_3: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 "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_3 :::"automaton"::: ) "over" (Set (Var "F")) (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k5_fsm_3 :::"right-Lang"::: ) (Set (Var "Q"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "w")) where w "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) : (Bool (Set (Set (Var "w")) ($#k3_rewrite3 :::"-succ_of"::: ) "(" (Set (Var "Q")) "," (Set (Var "A")) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set "the" ($#u2_fsm_3 :::"FinalS"::: ) "of" (Set (Var "A")))) "}" ))))); theorem :: FSM_3:17 (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 "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_3 :::"automaton"::: ) "over" (Set (Var "F")) (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set ($#k5_fsm_3 :::"right-Lang"::: ) (Set (Var "Q")))) "iff" (Bool (Set (Set (Var "w")) ($#k3_rewrite3 :::"-succ_of"::: ) "(" (Set (Var "Q")) "," (Set (Var "A")) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set "the" ($#u2_fsm_3 :::"FinalS"::: ) "of" (Set (Var "A")))) ")" )))))) ; 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 "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_3 :::"automaton"::: ) "over" (Set (Const "F")); func :::"Lang"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "E" ($#k8_afinsq_1 :::"^omega"::: ) ")" ) equals :: FSM_3:def 8 "{" (Set (Var "u")) where u "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set "E" ($#k8_afinsq_1 :::"^omega"::: ) ) : (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" "A" "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_fsm_3 :::"InitS"::: ) "of" "A")) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u2_fsm_3 :::"FinalS"::: ) "of" "A")) & (Bool (Set (Var "p")) "," (Set (Var "u")) ($#r4_rewrite3 :::"==>*"::: ) (Set (Var "q")) "," "A") ")" )) "}" ; end; :: deftheorem defines :::"Lang"::: FSM_3: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 "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_3 :::"automaton"::: ) "over" (Set (Var "F")) "holds" (Bool (Set ($#k6_fsm_3 :::"Lang"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "u")) where u "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) : (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_fsm_3 :::"InitS"::: ) "of" (Set (Var "A")))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u2_fsm_3 :::"FinalS"::: ) "of" (Set (Var "A")))) & (Bool (Set (Var "p")) "," (Set (Var "u")) ($#r4_rewrite3 :::"==>*"::: ) (Set (Var "q")) "," (Set (Var "A"))) ")" )) "}" )))); theorem :: FSM_3:18 (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 "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_3 :::"automaton"::: ) "over" (Set (Var "F")) "holds" (Bool "(" (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set ($#k6_fsm_3 :::"Lang"::: ) (Set (Var "A")))) "iff" (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_fsm_3 :::"InitS"::: ) "of" (Set (Var "A")))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u2_fsm_3 :::"FinalS"::: ) "of" (Set (Var "A")))) & (Bool (Set (Var "p")) "," (Set (Var "w")) ($#r4_rewrite3 :::"==>*"::: ) (Set (Var "q")) "," (Set (Var "A"))) ")" )) ")" ))))) ; theorem :: FSM_3:19 (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 "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_3 :::"automaton"::: ) "over" (Set (Var "F")) "holds" (Bool "(" (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set ($#k6_fsm_3 :::"Lang"::: ) (Set (Var "A")))) "iff" (Bool (Set (Set (Var "w")) ($#k3_rewrite3 :::"-succ_of"::: ) "(" (Set "the" ($#u1_fsm_3 :::"InitS"::: ) "of" (Set (Var "A"))) "," (Set (Var "A")) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set "the" ($#u2_fsm_3 :::"FinalS"::: ) "of" (Set (Var "A")))) ")" ))))) ; theorem :: FSM_3:20 (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 "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_3 :::"automaton"::: ) "over" (Set (Var "F")) "holds" (Bool (Set ($#k6_fsm_3 :::"Lang"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k3_fsm_3 :::"left-Lang"::: ) (Set "the" ($#u2_fsm_3 :::"FinalS"::: ) "of" (Set (Var "A")))))))) ; theorem :: FSM_3:21 (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 "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_3 :::"automaton"::: ) "over" (Set (Var "F")) "holds" (Bool (Set ($#k6_fsm_3 :::"Lang"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k5_fsm_3 :::"right-Lang"::: ) (Set "the" ($#u1_fsm_3 :::"InitS"::: ) "of" (Set (Var "A")))))))) ; theorem :: FSM_3:22 (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 "u")) "being" ($#m1_subset_1 :::"Element"::: ) "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 (Set "(" ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) (Bool "for" (Set (Var "R")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) "st" (Bool (Bool (Set (Set "(" (Set (Var "R")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k3_flang_1 :::"<%"::: ) (Set (Var "e")) ($#k3_flang_1 :::"%>"::: ) ) ($#k1_flang_1 :::"^"::: ) (Set (Var "u")))) & (Bool (Set (Set "(" (Set (Var "R")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "R")) ")" ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")))) & (Bool (Bool "not" (Set (Set "(" (Set (Var "R")) ($#k1_funct_1 :::"."::: ) (Num 2) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k3_flang_1 :::"<%"::: ) (Set (Var "e")) ($#k3_flang_1 :::"%>"::: ) ) ($#k1_flang_1 :::"^"::: ) (Set (Var "u")))))) "holds" (Bool (Set (Set "(" (Set (Var "R")) ($#k1_funct_1 :::"."::: ) (Num 2) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "u")))))))) ; theorem :: FSM_3:23 (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 "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Set "(" ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) (Bool "for" (Set (Var "R")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) "st" (Bool (Bool (Set (Set "(" (Set (Var "R")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "u"))) & (Bool (Set (Set "(" (Set (Var "R")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "R")) ")" ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "R"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "u")))))))) ; theorem :: FSM_3:24 (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 "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Set "(" ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) (Bool "for" (Set (Var "R")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) "st" (Bool (Bool (Set (Set "(" (Set (Var "R")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "v")))) & (Bool (Set (Set "(" (Set (Var "R")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "R")) ")" ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))))) "holds" (Bool "ex" (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "R")))) & (Bool (Set (Set "(" (Set (Var "R")) ($#k1_funct_1 :::"."::: ) (Set (Var "l")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "v"))) ")" )))))) ; definitionlet "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "u", "v" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Const "E")) ($#k8_afinsq_1 :::"^omega"::: ) ); func :::"chop"::: "(" "u" "," "v" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set "E" ($#k8_afinsq_1 :::"^omega"::: ) ) means :: FSM_3:def 9 (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "E" ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Set (Var "w")) ($#k1_flang_1 :::"^"::: ) "v") ($#r1_hidden :::"="::: ) "u")) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Var "w")))) if (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "E" ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Set (Set (Var "w")) ($#k1_flang_1 :::"^"::: ) "v") ($#r1_hidden :::"="::: ) "u")) otherwise (Bool it ($#r1_hidden :::"="::: ) "u"); end; :: deftheorem defines :::"chop"::: FSM_3:def 9 : (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 "b4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool "(" "(" (Bool (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Set (Set (Var "w")) ($#k1_flang_1 :::"^"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Var "u"))))) "implies" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k7_fsm_3 :::"chop"::: ) "(" (Set (Var "u")) "," (Set (Var "v")) ")" )) "iff" (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Set (Var "w")) ($#k1_flang_1 :::"^"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Var "u")))) "holds" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Var "w")))) ")" ) ")" & "(" (Bool (Bool "(" "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool (Bool "not" (Set (Set (Var "w")) ($#k1_flang_1 :::"^"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Var "u")))) ")" )) "implies" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k7_fsm_3 :::"chop"::: ) "(" (Set (Var "u")) "," (Set (Var "v")) ")" )) "iff" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Var "u"))) ")" ) ")" ")" ))); theorem :: FSM_3: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 "w")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "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 (Set "(" ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) (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 "(" (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "w")) ")" ) ($#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 "(" (Set (Var "v")) ($#k1_flang_1 :::"^"::: ) (Set (Var "w")) ")" ) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k1_rewrite3 :::"==>.-relation"::: ) (Set (Var "TS"))) "st" (Bool "(" (Bool (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "u")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) )) ")" ))))))) ; theorem :: FSM_3: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 "w")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "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 (Set "(" ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) "st" (Bool (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 :::"]"::: ) ))) "holds" (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 :::"]"::: ) )))))) ; theorem :: FSM_3:27 (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 "w")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "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 (Set "(" ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) "st" (Bool (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")))) "holds" (Bool (Set (Var "x")) "," (Set (Var "u")) ($#r3_rewrite3 :::"==>*"::: ) (Set (Var "y")) "," (Set (Var "v")) "," (Set (Var "TS"))))))) ; theorem :: FSM_3:28 (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 "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Set "(" ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Set (Var "p")) "," (Set (Set (Var "u")) ($#k1_flang_1 :::"^"::: ) (Set (Var "v"))) ($#r4_rewrite3 :::"==>*"::: ) (Set (Var "q")) "," (Set (Var "TS")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "TS")) "st" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "u")) ($#r4_rewrite3 :::"==>*"::: ) (Set (Var "r")) "," (Set (Var "TS"))) & (Bool (Set (Var "r")) "," (Set (Var "v")) ($#r4_rewrite3 :::"==>*"::: ) (Set (Var "q")) "," (Set (Var "TS"))) ")" )))))) ; theorem :: FSM_3:29 (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 "w")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "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 (Set "(" ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "w")) ($#k1_flang_1 :::"^"::: ) (Set (Var "v")) ")" ) ($#k3_rewrite3 :::"-succ_of"::: ) "(" (Set (Var "X")) "," (Set (Var "TS")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_rewrite3 :::"-succ_of"::: ) "(" (Set "(" (Set (Var "w")) ($#k3_rewrite3 :::"-succ_of"::: ) "(" (Set (Var "X")) "," (Set (Var "TS")) ")" ")" ) "," (Set (Var "TS")) ")" )))))) ; theorem :: FSM_3:30 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Set "(" ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) "holds" (Bool (Set ($#k1_fsm_3 :::"_bool"::: ) (Set (Var "TS"))) "is" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rewrite3 :::"transition-system"::: ) "over" (Set (Set "(" ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) ))))) ; theorem :: FSM_3:31 (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 "w")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "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 (Set "(" ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) "holds" (Bool (Set (Set (Var "w")) ($#k3_rewrite3 :::"-succ_of"::: ) "(" (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "v")) ($#k3_rewrite3 :::"-succ_of"::: ) "(" (Set (Var "X")) "," (Set (Var "TS")) ")" ")" ) ($#k6_domain_1 :::"}"::: ) ) "," (Set "(" ($#k1_fsm_3 :::"_bool"::: ) (Set (Var "TS")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set "(" (Set (Var "v")) ($#k1_flang_1 :::"^"::: ) (Set (Var "w")) ")" ) ($#k3_rewrite3 :::"-succ_of"::: ) "(" (Set (Var "X")) "," (Set (Var "TS")) ")" ")" ) ($#k6_domain_1 :::"}"::: ) )))))) ; theorem :: FSM_3:32 (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 "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "SA")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_3 :::"semiautomaton"::: ) "over" (Set (Set "(" ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) "holds" (Bool (Set (Set (Var "w")) ($#k3_rewrite3 :::"-succ_of"::: ) "(" (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k3_rewrite3 :::"-succ_of"::: ) "(" (Set (Var "X")) "," (Set (Var "SA")) ")" ")" ) ($#k6_domain_1 :::"}"::: ) ) "," (Set "(" ($#k2_fsm_3 :::"_bool"::: ) (Set (Var "SA")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "w")) ($#k3_rewrite3 :::"-succ_of"::: ) "(" (Set (Var "X")) "," (Set (Var "SA")) ")" ")" ) ($#k6_domain_1 :::"}"::: ) )))))) ; theorem :: FSM_3: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 "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_3 :::"automaton"::: ) "over" (Set (Set "(" ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u2_fsm_3 :::"FinalS"::: ) "of" (Set (Var "A")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u2_fsm_3 :::"FinalS"::: ) "of" (Set "(" ($#k4_fsm_3 :::"_bool"::: ) (Set (Var "A")) ")" ))))))) ; theorem :: FSM_3:34 (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 "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_3 :::"automaton"::: ) "over" (Set (Set "(" ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u2_fsm_3 :::"FinalS"::: ) "of" (Set "(" ($#k4_fsm_3 :::"_bool"::: ) (Set (Var "A")) ")" )))) "holds" (Bool (Set (Var "X")) ($#r1_xboole_0 :::"meets"::: ) (Set "the" ($#u2_fsm_3 :::"FinalS"::: ) "of" (Set (Var "A"))))))) ; theorem :: FSM_3:35 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_3 :::"automaton"::: ) "over" (Set (Set "(" ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) "holds" (Bool (Set "the" ($#u1_fsm_3 :::"InitS"::: ) "of" (Set "(" ($#k4_fsm_3 :::"_bool"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k3_rewrite3 :::"-succ_of"::: ) "(" (Set "the" ($#u1_fsm_3 :::"InitS"::: ) "of" (Set (Var "A"))) "," (Set (Var "A")) ")" ")" ) ($#k6_domain_1 :::"}"::: ) )))) ; theorem :: FSM_3:36 (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 "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_3 :::"automaton"::: ) "over" (Set (Set "(" ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) "holds" (Bool (Set (Set (Var "w")) ($#k3_rewrite3 :::"-succ_of"::: ) "(" (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k3_rewrite3 :::"-succ_of"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" ")" ) ($#k6_domain_1 :::"}"::: ) ) "," (Set "(" ($#k4_fsm_3 :::"_bool"::: ) (Set (Var "A")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "w")) ($#k3_rewrite3 :::"-succ_of"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" ")" ) ($#k6_domain_1 :::"}"::: ) )))))) ; theorem :: FSM_3:37 (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 "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_3 :::"automaton"::: ) "over" (Set (Set "(" ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) "holds" (Bool (Set (Set (Var "w")) ($#k3_rewrite3 :::"-succ_of"::: ) "(" (Set "the" ($#u1_fsm_3 :::"InitS"::: ) "of" (Set "(" ($#k4_fsm_3 :::"_bool"::: ) (Set (Var "A")) ")" )) "," (Set "(" ($#k4_fsm_3 :::"_bool"::: ) (Set (Var "A")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "w")) ($#k3_rewrite3 :::"-succ_of"::: ) "(" (Set "the" ($#u1_fsm_3 :::"InitS"::: ) "of" (Set (Var "A"))) "," (Set (Var "A")) ")" ")" ) ($#k6_domain_1 :::"}"::: ) ))))) ; theorem :: FSM_3:38 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_3 :::"automaton"::: ) "over" (Set (Set "(" ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) "holds" (Bool (Set ($#k6_fsm_3 :::"Lang"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k6_fsm_3 :::"Lang"::: ) (Set "(" ($#k4_fsm_3 :::"_bool"::: ) (Set (Var "A")) ")" ))))) ; theorem :: FSM_3:39 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_3 :::"automaton"::: ) "over" (Set (Set "(" ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) (Bool "ex" (Set (Var "DA")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_fsm_3 :::"deterministic"::: ) ($#l2_fsm_3 :::"automaton"::: ) "over" (Set ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E"))) "st" (Bool (Set ($#k6_fsm_3 :::"Lang"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k6_fsm_3 :::"Lang"::: ) (Set (Var "DA"))))))) ; theorem :: FSM_3:40 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "FA")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_3 :::"automaton"::: ) "over" (Set (Set "(" ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) (Bool "ex" (Set (Var "DFA")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v4_fsm_3 :::"deterministic"::: ) ($#l2_fsm_3 :::"automaton"::: ) "over" (Set ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E"))) "st" (Bool (Set ($#k6_fsm_3 :::"Lang"::: ) (Set (Var "FA"))) ($#r1_hidden :::"="::: ) (Set ($#k6_fsm_3 :::"Lang"::: ) (Set (Var "DFA"))))))) ;