:: FSM_1 semantic presentation begin definitionlet "IAlph" be ($#m1_hidden :::"set"::: ) ; attr "c2" is :::"strict"::: ; struct :::"FSM"::: "over" "IAlph" -> ($#l1_struct_0 :::"1-sorted"::: ) ; aggr :::"FSM":::(# :::"carrier":::, :::"Tran":::, :::"InitS"::: #) -> ($#l1_fsm_1 :::"FSM"::: ) "over" "IAlph"; sel :::"Tran"::: "c2" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c2") "," "IAlph" ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c2"); sel :::"InitS"::: "c2" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c2"); end; definitionlet "IAlph" be ($#m1_hidden :::"set"::: ) ; let "fsm" be ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Const "IAlph")); mode State of "fsm" is ($#m1_subset_1 :::"Element":::) "of" "fsm"; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) for ($#l1_fsm_1 :::"FSM"::: ) "over" "X"; end; definitionlet "IAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "fsm" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Const "IAlph")); let "s" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "IAlph")); let "q" be ($#m1_subset_1 :::"State":::) "of" (Set (Const "fsm")); func "s" :::"-succ_of"::: "q" -> ($#m1_subset_1 :::"State":::) "of" "fsm" equals :: FSM_1:def 1 (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" "fsm") ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) "q" "," "s" ($#k1_domain_1 :::"]"::: ) )); end; :: deftheorem defines :::"-succ_of"::: FSM_1:def 1 : (Bool "for" (Set (Var "IAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "fsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "IAlph")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "IAlph")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "fsm")) "holds" (Bool (Set (Set (Var "s")) ($#k1_fsm_1 :::"-succ_of"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "fsm"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "s")) ($#k1_domain_1 :::"]"::: ) ))))))); definitionlet "IAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "fsm" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Const "IAlph")); let "q" be ($#m1_subset_1 :::"State":::) "of" (Set (Const "fsm")); let "w" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "IAlph")); func "(" "q" "," "w" ")" :::"-admissible"::: -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "fsm") means :: FSM_1:def 2 (Bool "(" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) "q") & (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) "w" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "w"))) "holds" (Bool "ex" (Set (Var "wi")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "IAlph"(Bool "ex" (Set (Var "qi")) "," (Set (Var "qi1")) "being" ($#m1_subset_1 :::"State":::) "of" "fsm" "st" (Bool "(" (Bool (Set (Var "wi")) ($#r1_hidden :::"="::: ) (Set "w" ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "qi")) ($#r1_hidden :::"="::: ) (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "qi1")) ($#r1_hidden :::"="::: ) (Set it ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Set (Var "wi")) ($#k1_fsm_1 :::"-succ_of"::: ) (Set (Var "qi"))) ($#r1_hidden :::"="::: ) (Set (Var "qi1"))) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"-admissible"::: FSM_1:def 2 : (Bool "for" (Set (Var "IAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "fsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "IAlph")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "fsm")) (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "IAlph")) (Bool "for" (Set (Var "b5")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "fsm"))) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "q")) "," (Set (Var "w")) ")" ($#k2_fsm_1 :::"-admissible"::: ) )) "iff" (Bool "(" (Bool (Set (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "w")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "w"))))) "holds" (Bool "ex" (Set (Var "wi")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "IAlph"))(Bool "ex" (Set (Var "qi")) "," (Set (Var "qi1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "fsm")) "st" (Bool "(" (Bool (Set (Var "wi")) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "qi")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "qi1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Set (Var "wi")) ($#k1_fsm_1 :::"-succ_of"::: ) (Set (Var "qi"))) ($#r1_hidden :::"="::: ) (Set (Var "qi1"))) ")" ))) ")" ) ")" ) ")" )))))); theorem :: FSM_1:1 (Bool "for" (Set (Var "IAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "fsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "IAlph")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "fsm")) "holds" (Bool (Set "(" (Set (Var "q")) "," (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set (Var "IAlph")) ")" ) ")" ($#k2_fsm_1 :::"-admissible"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "q")) ($#k12_finseq_1 :::"*>"::: ) ))))) ; definitionlet "IAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "fsm" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Const "IAlph")); let "w" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "IAlph")); let "q1", "q2" be ($#m1_subset_1 :::"State":::) "of" (Set (Const "fsm")); pred "q1" "," "w" :::"-leads_to"::: "q2" means :: FSM_1:def 3 (Bool (Set (Set "(" "(" "q1" "," "w" ")" ($#k2_fsm_1 :::"-admissible"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) "w" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) "q2"); end; :: deftheorem defines :::"-leads_to"::: FSM_1:def 3 : (Bool "for" (Set (Var "IAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "fsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "IAlph")) (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "IAlph")) (Bool "for" (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "fsm")) "holds" (Bool "(" (Bool (Set (Var "q1")) "," (Set (Var "w")) ($#r1_fsm_1 :::"-leads_to"::: ) (Set (Var "q2"))) "iff" (Bool (Set (Set "(" "(" (Set (Var "q1")) "," (Set (Var "w")) ")" ($#k2_fsm_1 :::"-admissible"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "w")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "q2"))) ")" ))))); theorem :: FSM_1:2 (Bool "for" (Set (Var "IAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "fsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "IAlph")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "fsm")) "holds" (Bool (Set (Var "q")) "," (Set ($#k6_finseq_1 :::"<*>"::: ) (Set (Var "IAlph"))) ($#r1_fsm_1 :::"-leads_to"::: ) (Set (Var "q")))))) ; definitionlet "IAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "fsm" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Const "IAlph")); let "w" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "IAlph")); let "qseq" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "fsm"))); pred "qseq" :::"is_admissible_for"::: "w" means :: FSM_1:def 4 (Bool "ex" (Set (Var "q1")) "being" ($#m1_subset_1 :::"State":::) "of" "fsm" "st" (Bool "(" (Bool (Set (Var "q1")) ($#r1_hidden :::"="::: ) (Set "qseq" ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set "(" (Set (Var "q1")) "," "w" ")" ($#k2_fsm_1 :::"-admissible"::: ) ) ($#r1_hidden :::"="::: ) "qseq") ")" )); end; :: deftheorem defines :::"is_admissible_for"::: FSM_1:def 4 : (Bool "for" (Set (Var "IAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "fsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "IAlph")) (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "IAlph")) (Bool "for" (Set (Var "qseq")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "fsm"))) "holds" (Bool "(" (Bool (Set (Var "qseq")) ($#r2_fsm_1 :::"is_admissible_for"::: ) (Set (Var "w"))) "iff" (Bool "ex" (Set (Var "q1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "fsm")) "st" (Bool "(" (Bool (Set (Var "q1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "qseq")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set "(" (Set (Var "q1")) "," (Set (Var "w")) ")" ($#k2_fsm_1 :::"-admissible"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "qseq"))) ")" )) ")" ))))); theorem :: FSM_1:3 (Bool "for" (Set (Var "IAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "fsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "IAlph")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "fsm")) "holds" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "q")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_fsm_1 :::"is_admissible_for"::: ) (Set ($#k6_finseq_1 :::"<*>"::: ) (Set (Var "IAlph"))))))) ; definitionlet "IAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "fsm" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Const "IAlph")); let "q" be ($#m1_subset_1 :::"State":::) "of" (Set (Const "fsm")); let "w" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "IAlph")); func "q" :::"leads_to_under"::: "w" -> ($#m1_subset_1 :::"State":::) "of" "fsm" means :: FSM_1:def 5 (Bool "q" "," "w" ($#r1_fsm_1 :::"-leads_to"::: ) it); end; :: deftheorem defines :::"leads_to_under"::: FSM_1:def 5 : (Bool "for" (Set (Var "IAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "fsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "IAlph")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "fsm")) (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "IAlph")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "fsm")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k3_fsm_1 :::"leads_to_under"::: ) (Set (Var "w")))) "iff" (Bool (Set (Var "q")) "," (Set (Var "w")) ($#r1_fsm_1 :::"-leads_to"::: ) (Set (Var "b5"))) ")" )))))); theorem :: FSM_1:4 (Bool "for" (Set (Var "IAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "fsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "IAlph")) (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "IAlph")) (Bool "for" (Set (Var "q")) "," (Set (Var "q9")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "fsm")) "holds" (Bool "(" (Bool (Set (Set "(" "(" (Set (Var "q")) "," (Set (Var "w")) ")" ($#k2_fsm_1 :::"-admissible"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" "(" (Set (Var "q")) "," (Set (Var "w")) ")" ($#k2_fsm_1 :::"-admissible"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "q9"))) "iff" (Bool (Set (Var "q")) "," (Set (Var "w")) ($#r1_fsm_1 :::"-leads_to"::: ) (Set (Var "q9"))) ")" ))))) ; theorem :: FSM_1:5 (Bool "for" (Set (Var "IAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "fsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "IAlph")) (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "IAlph")) (Bool "for" (Set (Var "q1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "fsm")) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "w1"))))) "holds" (Bool (Set (Set "(" "(" (Set (Var "q1")) "," (Set "(" (Set (Var "w1")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "w2")) ")" ) ")" ($#k2_fsm_1 :::"-admissible"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "(" (Set (Var "q1")) "," (Set (Var "w1")) ")" ($#k2_fsm_1 :::"-admissible"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))))))))) ; theorem :: FSM_1:6 (Bool "for" (Set (Var "IAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "fsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "IAlph")) (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "IAlph")) (Bool "for" (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "fsm")) "st" (Bool (Bool (Set (Var "q1")) "," (Set (Var "w1")) ($#r1_fsm_1 :::"-leads_to"::: ) (Set (Var "q2")))) "holds" (Bool (Set (Set "(" "(" (Set (Var "q1")) "," (Set "(" (Set (Var "w1")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "w2")) ")" ) ")" ($#k2_fsm_1 :::"-admissible"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "w1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "q2"))))))) ; theorem :: FSM_1:7 (Bool "for" (Set (Var "IAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "fsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "IAlph")) (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "IAlph")) (Bool "for" (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "fsm")) "st" (Bool (Bool (Set (Var "q1")) "," (Set (Var "w1")) ($#r1_fsm_1 :::"-leads_to"::: ) (Set (Var "q2")))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "w2")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool (Set (Set "(" "(" (Set (Var "q1")) "," (Set "(" (Set (Var "w1")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "w2")) ")" ) ")" ($#k2_fsm_1 :::"-admissible"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "w1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "(" (Set (Var "q2")) "," (Set (Var "w2")) ")" ($#k2_fsm_1 :::"-admissible"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))))))))) ; theorem :: FSM_1:8 (Bool "for" (Set (Var "IAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "fsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "IAlph")) (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "IAlph")) (Bool "for" (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "fsm")) "st" (Bool (Bool (Set (Var "q1")) "," (Set (Var "w1")) ($#r1_fsm_1 :::"-leads_to"::: ) (Set (Var "q2")))) "holds" (Bool (Set "(" (Set (Var "q1")) "," (Set "(" (Set (Var "w1")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "w2")) ")" ) ")" ($#k2_fsm_1 :::"-admissible"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_finseq_3 :::"Del"::: ) "(" (Set "(" "(" (Set (Var "q1")) "," (Set (Var "w1")) ")" ($#k2_fsm_1 :::"-admissible"::: ) ")" ) "," (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "w1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k7_finseq_1 :::"^"::: ) (Set "(" "(" (Set (Var "q2")) "," (Set (Var "w2")) ")" ($#k2_fsm_1 :::"-admissible"::: ) ")" ))))))) ; begin definitionlet "IAlph" be ($#m1_hidden :::"set"::: ) ; let "OAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; attr "c3" is :::"strict"::: ; struct :::"Mealy-FSM"::: "over" "IAlph" "," "OAlph" -> ($#l1_fsm_1 :::"FSM"::: ) "over" "IAlph"; aggr :::"Mealy-FSM":::(# :::"carrier":::, :::"Tran":::, :::"OFun":::, :::"InitS"::: #) -> ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" "IAlph" "," "OAlph"; sel :::"OFun"::: "c3" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c3") "," "IAlph" ($#k2_zfmisc_1 :::":]"::: ) ) "," "OAlph"; attr "c3" is :::"strict"::: ; struct :::"Moore-FSM"::: "over" "IAlph" "," "OAlph" -> ($#l1_fsm_1 :::"FSM"::: ) "over" "IAlph"; aggr :::"Moore-FSM":::(# :::"carrier":::, :::"Tran":::, :::"OFun":::, :::"InitS"::: #) -> ($#l3_fsm_1 :::"Moore-FSM"::: ) "over" "IAlph" "," "OAlph"; sel :::"OFun"::: "c3" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c3") "," "OAlph"; end; registrationlet "IAlph" be ($#m1_hidden :::"set"::: ) ; let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "T" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "X")) "," (Set (Const "IAlph")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "X")); let "I" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); cluster (Set ($#g1_fsm_1 :::"FSM"::: ) "(#" "X" "," "T" "," "I" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ; end; registrationlet "IAlph" be ($#m1_hidden :::"set"::: ) ; let "OAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "T" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "X")) "," (Set (Const "IAlph")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "X")); let "O" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "X")) "," (Set (Const "IAlph")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "OAlph")); let "I" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); cluster (Set ($#g2_fsm_1 :::"Mealy-FSM"::: ) "(#" "X" "," "T" "," "O" "," "I" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ; end; registrationlet "IAlph" be ($#m1_hidden :::"set"::: ) ; let "OAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "T" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "X")) "," (Set (Const "IAlph")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "X")); let "O" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "OAlph")); let "I" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); cluster (Set ($#g3_fsm_1 :::"Moore-FSM"::: ) "(#" "X" "," "T" "," "O" "," "I" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ; end; registrationlet "IAlph" be ($#m1_hidden :::"set"::: ) ; let "OAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) for ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" "IAlph" "," "OAlph"; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) for ($#l3_fsm_1 :::"Moore-FSM"::: ) "over" "IAlph" "," "OAlph"; end; definitionlet "IAlph", "OAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "tfsm" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Const "IAlph")) "," (Set (Const "OAlph")); let "qt" be ($#m1_subset_1 :::"State":::) "of" (Set (Const "tfsm")); let "w" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "IAlph")); func "(" "qt" "," "w" ")" :::"-response"::: -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" "OAlph" means :: FSM_1:def 6 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "w")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "w"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_fsm_1 :::"OFun"::: ) "of" "tfsm") ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" "(" "qt" "," "w" ")" ($#k2_fsm_1 :::"-admissible"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" "w" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k4_tarski :::"]"::: ) ))) ")" ) ")" ); end; :: deftheorem defines :::"-response"::: FSM_1:def 6 : (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "qt")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "IAlph")) (Bool "for" (Set (Var "b6")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "OAlph")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "qt")) "," (Set (Var "w")) ")" ($#k4_fsm_1 :::"-response"::: ) )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b6"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "w")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "w"))))) "holds" (Bool (Set (Set (Var "b6")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_fsm_1 :::"OFun"::: ) "of" (Set (Var "tfsm"))) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" "(" (Set (Var "qt")) "," (Set (Var "w")) ")" ($#k2_fsm_1 :::"-admissible"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "w")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k4_tarski :::"]"::: ) ))) ")" ) ")" ) ")" )))))); theorem :: FSM_1:9 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "qt")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) "holds" (Bool (Set "(" (Set (Var "qt")) "," (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set (Var "IAlph")) ")" ) ")" ($#k4_fsm_1 :::"-response"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_finseq_1 :::"<*>"::: ) (Set (Var "OAlph"))))))) ; definitionlet "IAlph", "OAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "sfsm" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_fsm_1 :::"Moore-FSM"::: ) "over" (Set (Const "IAlph")) "," (Set (Const "OAlph")); let "qs" be ($#m1_subset_1 :::"State":::) "of" (Set (Const "sfsm")); let "w" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "IAlph")); func "(" "qs" "," "w" ")" :::"-response"::: -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" "OAlph" means :: FSM_1:def 7 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) "w" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) "w" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u4_fsm_1 :::"OFun"::: ) "of" "sfsm") ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" "(" "qs" "," "w" ")" ($#k2_fsm_1 :::"-admissible"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"-response"::: FSM_1:def 7 : (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "sfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_fsm_1 :::"Moore-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "qs")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "sfsm")) (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "IAlph")) (Bool "for" (Set (Var "b6")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "OAlph")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "qs")) "," (Set (Var "w")) ")" ($#k5_fsm_1 :::"-response"::: ) )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b6"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "w")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "w")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool (Set (Set (Var "b6")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u4_fsm_1 :::"OFun"::: ) "of" (Set (Var "sfsm"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" "(" (Set (Var "qs")) "," (Set (Var "w")) ")" ($#k2_fsm_1 :::"-admissible"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ) ")" )))))); theorem :: FSM_1:10 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "IAlph")) (Bool "for" (Set (Var "sfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_fsm_1 :::"Moore-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "qs")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "sfsm")) "holds" (Bool (Set (Set "(" "(" (Set (Var "qs")) "," (Set (Var "w")) ")" ($#k5_fsm_1 :::"-response"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u4_fsm_1 :::"OFun"::: ) "of" (Set (Var "sfsm"))) ($#k3_funct_2 :::"."::: ) (Set (Var "qs")))))))) ; theorem :: FSM_1:11 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "IAlph")) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "q1t")) "," (Set (Var "q2t")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) "st" (Bool (Bool (Set (Var "q1t")) "," (Set (Var "w1")) ($#r1_fsm_1 :::"-leads_to"::: ) (Set (Var "q2t")))) "holds" (Bool (Set "(" (Set (Var "q1t")) "," (Set "(" (Set (Var "w1")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "w2")) ")" ) ")" ($#k4_fsm_1 :::"-response"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" "(" (Set (Var "q1t")) "," (Set (Var "w1")) ")" ($#k4_fsm_1 :::"-response"::: ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" "(" (Set (Var "q2t")) "," (Set (Var "w2")) ")" ($#k4_fsm_1 :::"-response"::: ) ")" ))))))) ; theorem :: FSM_1:12 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "IAlph")) (Bool "for" (Set (Var "tfsm1")) "," (Set (Var "tfsm2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "q11")) "," (Set (Var "q12")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm1")) (Bool "for" (Set (Var "q21")) "," (Set (Var "q22")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm2")) "st" (Bool (Bool (Set (Var "q11")) "," (Set (Var "w1")) ($#r1_fsm_1 :::"-leads_to"::: ) (Set (Var "q12"))) & (Bool (Set (Var "q21")) "," (Set (Var "w1")) ($#r1_fsm_1 :::"-leads_to"::: ) (Set (Var "q22"))) & (Bool (Set "(" (Set (Var "q12")) "," (Set (Var "w2")) ")" ($#k4_fsm_1 :::"-response"::: ) ) ($#r1_hidden :::"<>"::: ) (Set "(" (Set (Var "q22")) "," (Set (Var "w2")) ")" ($#k4_fsm_1 :::"-response"::: ) ))) "holds" (Bool (Set "(" (Set (Var "q11")) "," (Set "(" (Set (Var "w1")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "w2")) ")" ) ")" ($#k4_fsm_1 :::"-response"::: ) ) ($#r1_hidden :::"<>"::: ) (Set "(" (Set (Var "q21")) "," (Set "(" (Set (Var "w1")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "w2")) ")" ) ")" ($#k4_fsm_1 :::"-response"::: ) ))))))) ; definitionlet "IAlph", "OAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "tfsm" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Const "IAlph")) "," (Set (Const "OAlph")); let "sfsm" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_fsm_1 :::"Moore-FSM"::: ) "over" (Set (Const "IAlph")) "," (Set (Const "OAlph")); pred "tfsm" :::"is_similar_to"::: "sfsm" means :: FSM_1:def 8 (Bool "for" (Set (Var "tw")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" "IAlph" "holds" (Bool (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set "the" ($#u4_fsm_1 :::"OFun"::: ) "of" "sfsm") ($#k3_funct_2 :::"."::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" "sfsm") ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set "(" "(" (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" "tfsm") "," (Set (Var "tw")) ")" ($#k4_fsm_1 :::"-response"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set "(" (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" "sfsm") "," (Set (Var "tw")) ")" ($#k5_fsm_1 :::"-response"::: ) ))); end; :: deftheorem defines :::"is_similar_to"::: FSM_1:def 8 : (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "sfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_fsm_1 :::"Moore-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "holds" (Bool "(" (Bool (Set (Var "tfsm")) ($#r3_fsm_1 :::"is_similar_to"::: ) (Set (Var "sfsm"))) "iff" (Bool "for" (Set (Var "tw")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "IAlph")) "holds" (Bool (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set "the" ($#u4_fsm_1 :::"OFun"::: ) "of" (Set (Var "sfsm"))) ($#k3_funct_2 :::"."::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "sfsm"))) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set "(" "(" (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "tfsm"))) "," (Set (Var "tw")) ")" ($#k4_fsm_1 :::"-response"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set "(" (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "sfsm"))) "," (Set (Var "tw")) ")" ($#k5_fsm_1 :::"-response"::: ) ))) ")" )))); theorem :: FSM_1:13 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "sfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l3_fsm_1 :::"Moore-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "ex" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "st" (Bool (Set (Var "tfsm")) ($#r3_fsm_1 :::"is_similar_to"::: ) (Set (Var "sfsm")))))) ; theorem :: FSM_1:14 (Bool "for" (Set (Var "IAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "OAlphf")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsmf")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlphf")) (Bool "ex" (Set (Var "sfsmf")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l3_fsm_1 :::"Moore-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlphf")) "st" (Bool (Set (Var "tfsmf")) ($#r3_fsm_1 :::"is_similar_to"::: ) (Set (Var "sfsmf"))))))) ; begin definitionlet "IAlph", "OAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "tfsm1", "tfsm2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Const "IAlph")) "," (Set (Const "OAlph")); pred "tfsm1" "," "tfsm2" :::"-are_equivalent"::: means :: FSM_1:def 9 (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" "IAlph" "holds" (Bool (Set "(" (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" "tfsm1") "," (Set (Var "w")) ")" ($#k4_fsm_1 :::"-response"::: ) ) ($#r1_hidden :::"="::: ) (Set "(" (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" "tfsm2") "," (Set (Var "w")) ")" ($#k4_fsm_1 :::"-response"::: ) ))); reflexivity (Bool "for" (Set (Var "tfsm1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Const "IAlph")) "," (Set (Const "OAlph")) (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "IAlph")) "holds" (Bool (Set "(" (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "tfsm1"))) "," (Set (Var "w")) ")" ($#k4_fsm_1 :::"-response"::: ) ) ($#r1_hidden :::"="::: ) (Set "(" (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "tfsm1"))) "," (Set (Var "w")) ")" ($#k4_fsm_1 :::"-response"::: ) )))) ; symmetry (Bool "for" (Set (Var "tfsm1")) "," (Set (Var "tfsm2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Const "IAlph")) "," (Set (Const "OAlph")) "st" (Bool (Bool "(" "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "IAlph")) "holds" (Bool (Set "(" (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "tfsm1"))) "," (Set (Var "w")) ")" ($#k4_fsm_1 :::"-response"::: ) ) ($#r1_hidden :::"="::: ) (Set "(" (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "tfsm2"))) "," (Set (Var "w")) ")" ($#k4_fsm_1 :::"-response"::: ) )) ")" )) "holds" (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "IAlph")) "holds" (Bool (Set "(" (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "tfsm2"))) "," (Set (Var "w")) ")" ($#k4_fsm_1 :::"-response"::: ) ) ($#r1_hidden :::"="::: ) (Set "(" (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "tfsm1"))) "," (Set (Var "w")) ")" ($#k4_fsm_1 :::"-response"::: ) )))) ; end; :: deftheorem defines :::"-are_equivalent"::: FSM_1:def 9 : (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm1")) "," (Set (Var "tfsm2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "holds" (Bool "(" (Bool (Set (Var "tfsm1")) "," (Set (Var "tfsm2")) ($#r4_fsm_1 :::"-are_equivalent"::: ) ) "iff" (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "IAlph")) "holds" (Bool (Set "(" (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "tfsm1"))) "," (Set (Var "w")) ")" ($#k4_fsm_1 :::"-response"::: ) ) ($#r1_hidden :::"="::: ) (Set "(" (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "tfsm2"))) "," (Set (Var "w")) ")" ($#k4_fsm_1 :::"-response"::: ) ))) ")" ))); theorem :: FSM_1:15 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm1")) "," (Set (Var "tfsm2")) "," (Set (Var "tfsm3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "st" (Bool (Bool (Set (Var "tfsm1")) "," (Set (Var "tfsm2")) ($#r4_fsm_1 :::"-are_equivalent"::: ) ) & (Bool (Set (Var "tfsm2")) "," (Set (Var "tfsm3")) ($#r4_fsm_1 :::"-are_equivalent"::: ) )) "holds" (Bool (Set (Var "tfsm1")) "," (Set (Var "tfsm3")) ($#r4_fsm_1 :::"-are_equivalent"::: ) ))) ; definitionlet "IAlph", "OAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "tfsm" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Const "IAlph")) "," (Set (Const "OAlph")); let "qa", "qb" be ($#m1_subset_1 :::"State":::) "of" (Set (Const "tfsm")); pred "qa" "," "qb" :::"-are_equivalent"::: means :: FSM_1:def 10 (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" "IAlph" "holds" (Bool (Set "(" "qa" "," (Set (Var "w")) ")" ($#k4_fsm_1 :::"-response"::: ) ) ($#r1_hidden :::"="::: ) (Set "(" "qb" "," (Set (Var "w")) ")" ($#k4_fsm_1 :::"-response"::: ) ))); reflexivity (Bool "for" (Set (Var "qa")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Const "tfsm")) (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "IAlph")) "holds" (Bool (Set "(" (Set (Var "qa")) "," (Set (Var "w")) ")" ($#k4_fsm_1 :::"-response"::: ) ) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "qa")) "," (Set (Var "w")) ")" ($#k4_fsm_1 :::"-response"::: ) )))) ; symmetry (Bool "for" (Set (Var "qa")) "," (Set (Var "qb")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Const "tfsm")) "st" (Bool (Bool "(" "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "IAlph")) "holds" (Bool (Set "(" (Set (Var "qa")) "," (Set (Var "w")) ")" ($#k4_fsm_1 :::"-response"::: ) ) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "qb")) "," (Set (Var "w")) ")" ($#k4_fsm_1 :::"-response"::: ) )) ")" )) "holds" (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "IAlph")) "holds" (Bool (Set "(" (Set (Var "qb")) "," (Set (Var "w")) ")" ($#k4_fsm_1 :::"-response"::: ) ) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "qa")) "," (Set (Var "w")) ")" ($#k4_fsm_1 :::"-response"::: ) )))) ; end; :: deftheorem defines :::"-are_equivalent"::: FSM_1:def 10 : (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "qa")) "," (Set (Var "qb")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) "holds" (Bool "(" (Bool (Set (Var "qa")) "," (Set (Var "qb")) ($#r5_fsm_1 :::"-are_equivalent"::: ) ) "iff" (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "IAlph")) "holds" (Bool (Set "(" (Set (Var "qa")) "," (Set (Var "w")) ")" ($#k4_fsm_1 :::"-response"::: ) ) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "qb")) "," (Set (Var "w")) ")" ($#k4_fsm_1 :::"-response"::: ) ))) ")" )))); theorem :: FSM_1:16 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "q3")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) "st" (Bool (Bool (Set (Var "q1")) "," (Set (Var "q2")) ($#r5_fsm_1 :::"-are_equivalent"::: ) ) & (Bool (Set (Var "q2")) "," (Set (Var "q3")) ($#r5_fsm_1 :::"-are_equivalent"::: ) )) "holds" (Bool (Set (Var "q1")) "," (Set (Var "q3")) ($#r5_fsm_1 :::"-are_equivalent"::: ) )))) ; theorem :: FSM_1:17 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "IAlph")) (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "IAlph")) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "qa9")) "," (Set (Var "qa")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) "st" (Bool (Bool (Set (Var "qa9")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "tfsm"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "qa")) "," (Set (Var "s")) ($#k1_domain_1 :::"]"::: ) )))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "w")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool (Set (Set "(" "(" (Set (Var "qa")) "," (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "s")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "w")) ")" ) ")" ($#k2_fsm_1 :::"-admissible"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "(" (Set (Var "qa9")) "," (Set (Var "w")) ")" ($#k2_fsm_1 :::"-admissible"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))))))))) ; theorem :: FSM_1:18 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "IAlph")) (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "IAlph")) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "qa9")) "," (Set (Var "qa")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) "st" (Bool (Bool (Set (Var "qa9")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "tfsm"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "qa")) "," (Set (Var "s")) ($#k1_domain_1 :::"]"::: ) )))) "holds" (Bool (Set "(" (Set (Var "qa")) "," (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "s")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "w")) ")" ) ")" ($#k4_fsm_1 :::"-response"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set "the" ($#u3_fsm_1 :::"OFun"::: ) "of" (Set (Var "tfsm"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "qa")) "," (Set (Var "s")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set "(" "(" (Set (Var "qa9")) "," (Set (Var "w")) ")" ($#k4_fsm_1 :::"-response"::: ) ")" )))))))) ; theorem :: FSM_1:19 (Bool "for" (Set (Var "OAlph")) "," (Set (Var "IAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "qa")) "," (Set (Var "qb")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) "holds" (Bool "(" (Bool (Set (Var "qa")) "," (Set (Var "qb")) ($#r5_fsm_1 :::"-are_equivalent"::: ) ) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "IAlph")) "holds" (Bool "(" (Bool (Set (Set "the" ($#u3_fsm_1 :::"OFun"::: ) "of" (Set (Var "tfsm"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "qa")) "," (Set (Var "s")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_fsm_1 :::"OFun"::: ) "of" (Set (Var "tfsm"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "qb")) "," (Set (Var "s")) ($#k1_domain_1 :::"]"::: ) ))) & (Bool (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "tfsm"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "qa")) "," (Set (Var "s")) ($#k1_domain_1 :::"]"::: ) )) "," (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "tfsm"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "qb")) "," (Set (Var "s")) ($#k1_domain_1 :::"]"::: ) )) ($#r5_fsm_1 :::"-are_equivalent"::: ) ) ")" )) ")" )))) ; theorem :: FSM_1:20 (Bool "for" (Set (Var "OAlph")) "," (Set (Var "IAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "qa")) "," (Set (Var "qb")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) "st" (Bool (Bool (Set (Var "qa")) "," (Set (Var "qb")) ($#r5_fsm_1 :::"-are_equivalent"::: ) )) "holds" (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "IAlph")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "w"))))) "holds" (Bool "ex" (Set (Var "qai")) "," (Set (Var "qbi")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) "st" (Bool "(" (Bool (Set (Var "qai")) ($#r1_hidden :::"="::: ) (Set (Set "(" "(" (Set (Var "qa")) "," (Set (Var "w")) ")" ($#k2_fsm_1 :::"-admissible"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "qbi")) ($#r1_hidden :::"="::: ) (Set (Set "(" "(" (Set (Var "qb")) "," (Set (Var "w")) ")" ($#k2_fsm_1 :::"-admissible"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "qai")) "," (Set (Var "qbi")) ($#r5_fsm_1 :::"-are_equivalent"::: ) ) ")" ))))))) ; definitionlet "IAlph", "OAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "tfsm" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Const "IAlph")) "," (Set (Const "OAlph")); let "qa", "qb" be ($#m1_subset_1 :::"State":::) "of" (Set (Const "tfsm")); let "k" be ($#m1_hidden :::"Nat":::); pred "k" :::"-equivalent"::: "qa" "," "qb" means :: FSM_1:def 11 (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" "IAlph" "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "w"))) ($#r1_xxreal_0 :::"<="::: ) "k")) "holds" (Bool (Set "(" "qa" "," (Set (Var "w")) ")" ($#k4_fsm_1 :::"-response"::: ) ) ($#r1_hidden :::"="::: ) (Set "(" "qb" "," (Set (Var "w")) ")" ($#k4_fsm_1 :::"-response"::: ) ))); end; :: deftheorem defines :::"-equivalent"::: FSM_1:def 11 : (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "qa")) "," (Set (Var "qb")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "k")) ($#r6_fsm_1 :::"-equivalent"::: ) (Set (Var "qa")) "," (Set (Var "qb"))) "iff" (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "IAlph")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "w"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (Set "(" (Set (Var "qa")) "," (Set (Var "w")) ")" ($#k4_fsm_1 :::"-response"::: ) ) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "qb")) "," (Set (Var "w")) ")" ($#k4_fsm_1 :::"-response"::: ) ))) ")" ))))); theorem :: FSM_1:21 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "qa")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Var "k")) ($#r6_fsm_1 :::"-equivalent"::: ) (Set (Var "qa")) "," (Set (Var "qa"))))))) ; theorem :: FSM_1:22 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "qa")) "," (Set (Var "qb")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r6_fsm_1 :::"-equivalent"::: ) (Set (Var "qa")) "," (Set (Var "qb")))) "holds" (Bool (Set (Var "k")) ($#r6_fsm_1 :::"-equivalent"::: ) (Set (Var "qb")) "," (Set (Var "qa"))))))) ; theorem :: FSM_1:23 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "qa")) "," (Set (Var "qb")) "," (Set (Var "qc")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r6_fsm_1 :::"-equivalent"::: ) (Set (Var "qa")) "," (Set (Var "qb"))) & (Bool (Set (Var "k")) ($#r6_fsm_1 :::"-equivalent"::: ) (Set (Var "qb")) "," (Set (Var "qc")))) "holds" (Bool (Set (Var "k")) ($#r6_fsm_1 :::"-equivalent"::: ) (Set (Var "qa")) "," (Set (Var "qc"))))))) ; theorem :: FSM_1:24 (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "qa")) "," (Set (Var "qb")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) "st" (Bool (Bool (Set (Var "qa")) "," (Set (Var "qb")) ($#r5_fsm_1 :::"-are_equivalent"::: ) )) "holds" (Bool (Set (Var "k")) ($#r6_fsm_1 :::"-equivalent"::: ) (Set (Var "qa")) "," (Set (Var "qb"))))))) ; theorem :: FSM_1:25 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "qa")) "," (Set (Var "qb")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r6_fsm_1 :::"-equivalent"::: ) (Set (Var "qa")) "," (Set (Var "qb")))))) ; theorem :: FSM_1:26 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "qa")) "," (Set (Var "qb")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) (Bool "for" (Set (Var "k")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "m"))) ($#r6_fsm_1 :::"-equivalent"::: ) (Set (Var "qa")) "," (Set (Var "qb")))) "holds" (Bool (Set (Var "k")) ($#r6_fsm_1 :::"-equivalent"::: ) (Set (Var "qa")) "," (Set (Var "qb"))))))) ; theorem :: FSM_1:27 (Bool "for" (Set (Var "OAlph")) "," (Set (Var "IAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "qa")) "," (Set (Var "qb")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool "(" (Bool (Set (Var "k")) ($#r6_fsm_1 :::"-equivalent"::: ) (Set (Var "qa")) "," (Set (Var "qb"))) "iff" (Bool "(" (Bool (Num 1) ($#r6_fsm_1 :::"-equivalent"::: ) (Set (Var "qa")) "," (Set (Var "qb"))) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "IAlph")) (Bool "for" (Set (Var "k1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1)))) "holds" (Bool (Set (Var "k1")) ($#r6_fsm_1 :::"-equivalent"::: ) (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "tfsm"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "qa")) "," (Set (Var "s")) ($#k1_domain_1 :::"]"::: ) )) "," (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "tfsm"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "qb")) "," (Set (Var "s")) ($#k1_domain_1 :::"]"::: ) )))) ")" ) ")" ) ")" ))))) ; definitionlet "IAlph", "OAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "tfsm" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Const "IAlph")) "," (Set (Const "OAlph")); let "i" be ($#m1_hidden :::"Nat":::); func "i" :::"-eq_states_EqR"::: "tfsm" -> ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "tfsm") means :: FSM_1:def 12 (Bool "for" (Set (Var "qa")) "," (Set (Var "qb")) "being" ($#m1_subset_1 :::"State":::) "of" "tfsm" "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "qa")) "," (Set (Var "qb")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "i" ($#r6_fsm_1 :::"-equivalent"::: ) (Set (Var "qa")) "," (Set (Var "qb"))) ")" )); end; :: deftheorem defines :::"-eq_states_EqR"::: FSM_1:def 12 : (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "tfsm"))) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k6_fsm_1 :::"-eq_states_EqR"::: ) (Set (Var "tfsm")))) "iff" (Bool "for" (Set (Var "qa")) "," (Set (Var "qb")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "qa")) "," (Set (Var "qb")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b5"))) "iff" (Bool (Set (Var "i")) ($#r6_fsm_1 :::"-equivalent"::: ) (Set (Var "qa")) "," (Set (Var "qb"))) ")" )) ")" ))))); definitionlet "IAlph", "OAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "tfsm" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Const "IAlph")) "," (Set (Const "OAlph")); let "i" be ($#m1_hidden :::"Nat":::); func "i" :::"-eq_states_partition"::: "tfsm" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "tfsm") equals :: FSM_1:def 13 (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" "i" ($#k6_fsm_1 :::"-eq_states_EqR"::: ) "tfsm" ")" )); end; :: deftheorem defines :::"-eq_states_partition"::: FSM_1:def 13 : (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "i")) ($#k7_fsm_1 :::"-eq_states_partition"::: ) (Set (Var "tfsm"))) ($#r1_hidden :::"="::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" (Set (Var "i")) ($#k6_fsm_1 :::"-eq_states_EqR"::: ) (Set (Var "tfsm")) ")" )))))); theorem :: FSM_1:28 (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "holds" (Bool (Set (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k7_fsm_1 :::"-eq_states_partition"::: ) (Set (Var "tfsm"))) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set (Set (Var "k")) ($#k7_fsm_1 :::"-eq_states_partition"::: ) (Set (Var "tfsm"))))))) ; theorem :: FSM_1:29 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" (Set (Var "k")) ($#k6_fsm_1 :::"-eq_states_EqR"::: ) (Set (Var "tfsm")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k6_fsm_1 :::"-eq_states_EqR"::: ) (Set (Var "tfsm")) ")" )))) "holds" (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" (Set "(" (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "m")) ")" ) ($#k6_fsm_1 :::"-eq_states_EqR"::: ) (Set (Var "tfsm")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" (Set (Var "k")) ($#k6_fsm_1 :::"-eq_states_EqR"::: ) (Set (Var "tfsm")) ")" ))))))) ; theorem :: FSM_1:30 (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "st" (Bool (Bool (Set (Set (Var "k")) ($#k7_fsm_1 :::"-eq_states_partition"::: ) (Set (Var "tfsm"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k7_fsm_1 :::"-eq_states_partition"::: ) (Set (Var "tfsm"))))) "holds" (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Set (Var "m")) ")" ) ($#k7_fsm_1 :::"-eq_states_partition"::: ) (Set (Var "tfsm"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k7_fsm_1 :::"-eq_states_partition"::: ) (Set (Var "tfsm")))))))) ; theorem :: FSM_1:31 (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "st" (Bool (Bool (Set (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k7_fsm_1 :::"-eq_states_partition"::: ) (Set (Var "tfsm"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "k")) ($#k7_fsm_1 :::"-eq_states_partition"::: ) (Set (Var "tfsm"))))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (Set (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k7_fsm_1 :::"-eq_states_partition"::: ) (Set (Var "tfsm"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "i")) ($#k7_fsm_1 :::"-eq_states_partition"::: ) (Set (Var "tfsm")))))))) ; theorem :: FSM_1:32 (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "holds" (Bool "(" (Bool (Set (Set (Var "k")) ($#k7_fsm_1 :::"-eq_states_partition"::: ) (Set (Var "tfsm"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k7_fsm_1 :::"-eq_states_partition"::: ) (Set (Var "tfsm")))) "or" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "k")) ($#k7_fsm_1 :::"-eq_states_partition"::: ) (Set (Var "tfsm")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k7_fsm_1 :::"-eq_states_partition"::: ) (Set (Var "tfsm")) ")" ))) ")" )))) ; theorem :: FSM_1:33 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) "holds" (Bool (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k6_fsm_1 :::"-eq_states_EqR"::: ) (Set (Var "tfsm")) ")" ) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "tfsm"))))))) ; theorem :: FSM_1:34 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "holds" (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k7_fsm_1 :::"-eq_states_partition"::: ) (Set (Var "tfsm"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "tfsm"))) ($#k1_tarski :::"}"::: ) )))) ; theorem :: FSM_1:35 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "st" (Bool (Bool (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "tfsm")))))) "holds" (Bool (Set (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k7_fsm_1 :::"-eq_states_partition"::: ) (Set (Var "tfsm"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k7_fsm_1 :::"-eq_states_partition"::: ) (Set (Var "tfsm"))))))) ; definitionlet "IAlph", "OAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "tfsm" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Const "IAlph")) "," (Set (Const "OAlph")); let "IT" be ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "tfsm"))); attr "IT" is :::"final"::: means :: FSM_1:def 14 (Bool "for" (Set (Var "qa")) "," (Set (Var "qb")) "being" ($#m1_subset_1 :::"State":::) "of" "tfsm" "holds" (Bool "(" (Bool (Set (Var "qa")) "," (Set (Var "qb")) ($#r5_fsm_1 :::"-are_equivalent"::: ) ) "iff" (Bool "ex" (Set (Var "X")) "being" ($#m2_subset_1 :::"Element"::: ) "of" "IT" "st" (Bool "(" (Bool (Set (Var "qa")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "qb")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )) ")" )); end; :: deftheorem defines :::"final"::: FSM_1:def 14 : (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "IT")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "tfsm"))) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_fsm_1 :::"final"::: ) ) "iff" (Bool "for" (Set (Var "qa")) "," (Set (Var "qb")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) "holds" (Bool "(" (Bool (Set (Var "qa")) "," (Set (Var "qb")) ($#r5_fsm_1 :::"-are_equivalent"::: ) ) "iff" (Bool "ex" (Set (Var "X")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "IT")) "st" (Bool "(" (Bool (Set (Var "qa")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "qb")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )) ")" )) ")" )))); theorem :: FSM_1:36 (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "st" (Bool (Bool (Set (Set (Var "k")) ($#k7_fsm_1 :::"-eq_states_partition"::: ) (Set (Var "tfsm"))) "is" ($#v4_fsm_1 :::"final"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k6_fsm_1 :::"-eq_states_EqR"::: ) (Set (Var "tfsm"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k6_fsm_1 :::"-eq_states_EqR"::: ) (Set (Var "tfsm"))))))) ; theorem :: FSM_1:37 (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "st" (Bool (Bool (Set (Set (Var "k")) ($#k7_fsm_1 :::"-eq_states_partition"::: ) (Set (Var "tfsm"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k7_fsm_1 :::"-eq_states_partition"::: ) (Set (Var "tfsm"))))) "holds" (Bool (Set (Set (Var "k")) ($#k7_fsm_1 :::"-eq_states_partition"::: ) (Set (Var "tfsm"))) "is" ($#v4_fsm_1 :::"final"::: ) )))) ; theorem :: FSM_1:38 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "st" (Bool (Bool (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "tfsm")))))) "holds" (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "k")) ($#k7_fsm_1 :::"-eq_states_partition"::: ) (Set (Var "tfsm"))) "is" ($#v4_fsm_1 :::"final"::: ) ) ")" ))))) ; definitionlet "IAlph", "OAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "tfsm" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Const "IAlph")) "," (Set (Const "OAlph")); func :::"final_states_partition"::: "tfsm" -> ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "tfsm") means :: FSM_1:def 15 (Bool it "is" ($#v4_fsm_1 :::"final"::: ) ); end; :: deftheorem defines :::"final_states_partition"::: FSM_1:def 15 : (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "b4")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "tfsm"))) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k8_fsm_1 :::"final_states_partition"::: ) (Set (Var "tfsm")))) "iff" (Bool (Set (Var "b4")) "is" ($#v4_fsm_1 :::"final"::: ) ) ")" )))); theorem :: FSM_1:39 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "st" (Bool (Bool (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "tfsm")))))) "holds" (Bool (Set ($#k8_fsm_1 :::"final_states_partition"::: ) (Set (Var "tfsm"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k7_fsm_1 :::"-eq_states_partition"::: ) (Set (Var "tfsm"))))))) ; begin definitionlet "IAlph", "OAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "tfsm" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Const "IAlph")) "," (Set (Const "OAlph")); let "qf" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_fsm_1 :::"final_states_partition"::: ) (Set (Const "tfsm"))); let "s" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "IAlph")); func "(" "s" "," "qf" ")" :::"-succ_class"::: -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_fsm_1 :::"final_states_partition"::: ) "tfsm") means :: FSM_1:def 16 (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" "tfsm"(Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) "qf") & (Bool (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "tfsm"))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" (Set (Var "n")) ($#k6_fsm_1 :::"-eq_states_EqR"::: ) "tfsm" ")" ) "," (Set "(" (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" "tfsm") ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "q")) "," "s" ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" )) ")" ))); end; :: deftheorem defines :::"-succ_class"::: FSM_1:def 16 : (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "qf")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_fsm_1 :::"final_states_partition"::: ) (Set (Var "tfsm"))) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "IAlph")) (Bool "for" (Set (Var "b6")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_fsm_1 :::"final_states_partition"::: ) (Set (Var "tfsm"))) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "s")) "," (Set (Var "qf")) ")" ($#k9_fsm_1 :::"-succ_class"::: ) )) "iff" (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm"))(Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "qf"))) & (Bool (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "tfsm"))))) & (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" (Set (Var "n")) ($#k6_fsm_1 :::"-eq_states_EqR"::: ) (Set (Var "tfsm")) ")" ) "," (Set "(" (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "tfsm"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "s")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" )) ")" ))) ")" )))))); definitionlet "IAlph", "OAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "tfsm" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Const "IAlph")) "," (Set (Const "OAlph")); let "qf" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_fsm_1 :::"final_states_partition"::: ) (Set (Const "tfsm"))); let "s" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "IAlph")); func "(" "qf" "," "s" ")" :::"-class_response"::: -> ($#m1_subset_1 :::"Element"::: ) "of" "OAlph" means :: FSM_1:def 17 (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" "tfsm" "st" (Bool "(" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) "qf") & (Bool it ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_fsm_1 :::"OFun"::: ) "of" "tfsm") ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "q")) "," "s" ($#k1_domain_1 :::"]"::: ) ))) ")" )); end; :: deftheorem defines :::"-class_response"::: FSM_1:def 17 : (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "qf")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_fsm_1 :::"final_states_partition"::: ) (Set (Var "tfsm"))) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "IAlph")) (Bool "for" (Set (Var "b6")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "OAlph")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "qf")) "," (Set (Var "s")) ")" ($#k10_fsm_1 :::"-class_response"::: ) )) "iff" (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) "st" (Bool "(" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "qf"))) & (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_fsm_1 :::"OFun"::: ) "of" (Set (Var "tfsm"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "s")) ($#k1_domain_1 :::"]"::: ) ))) ")" )) ")" )))))); definitionlet "IAlph", "OAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "tfsm" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Const "IAlph")) "," (Set (Const "OAlph")); func :::"the_reduction_of"::: "tfsm" -> ($#v2_fsm_1 :::"strict"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" "IAlph" "," "OAlph" means :: FSM_1:def 18 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k8_fsm_1 :::"final_states_partition"::: ) "tfsm")) & (Bool "(" "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"State":::) "of" it (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "IAlph" (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" "tfsm" "st" (Bool (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "Q")))) "holds" (Bool "(" (Bool (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" "tfsm") ($#k2_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "s")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" it) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "Q")) "," (Set (Var "s")) ")" )) & (Bool (Set (Set "the" ($#u3_fsm_1 :::"OFun"::: ) "of" "tfsm") ($#k2_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_fsm_1 :::"OFun"::: ) "of" it) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "Q")) "," (Set (Var "s")) ")" )) ")" ))) ")" ) & (Bool (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" "tfsm") ($#r2_hidden :::"in"::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" it)) ")" ); end; :: deftheorem defines :::"the_reduction_of"::: FSM_1:def 18 : (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "b4")) "being" ($#v2_fsm_1 :::"strict"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k11_fsm_1 :::"the_reduction_of"::: ) (Set (Var "tfsm")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k8_fsm_1 :::"final_states_partition"::: ) (Set (Var "tfsm")))) & (Bool "(" "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "b4")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "IAlph")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) "st" (Bool (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "Q")))) "holds" (Bool "(" (Bool (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "tfsm"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "s")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "b4"))) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "Q")) "," (Set (Var "s")) ")" )) & (Bool (Set (Set "the" ($#u3_fsm_1 :::"OFun"::: ) "of" (Set (Var "tfsm"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_fsm_1 :::"OFun"::: ) "of" (Set (Var "b4"))) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "Q")) "," (Set (Var "s")) ")" )) ")" ))) ")" ) & (Bool (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "tfsm"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "b4")))) ")" ) ")" )))); registrationlet "IAlph", "OAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "tfsm" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Const "IAlph")) "," (Set (Const "OAlph")); cluster (Set ($#k11_fsm_1 :::"the_reduction_of"::: ) "tfsm") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v2_fsm_1 :::"strict"::: ) ; end; theorem :: FSM_1:40 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "IAlph")) (Bool "for" (Set (Var "rtfsm")) "," (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) (Bool "for" (Set (Var "qr")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "rtfsm")) "st" (Bool (Bool (Set (Var "rtfsm")) ($#r1_hidden :::"="::: ) (Set ($#k11_fsm_1 :::"the_reduction_of"::: ) (Set (Var "tfsm")))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "qr")))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "w")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool (Set (Set "(" "(" (Set (Var "q")) "," (Set (Var "w")) ")" ($#k2_fsm_1 :::"-admissible"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set (Set "(" "(" (Set (Var "qr")) "," (Set (Var "w")) ")" ($#k2_fsm_1 :::"-admissible"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k")))))))))) ; theorem :: FSM_1:41 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "holds" (Bool (Set (Var "tfsm")) "," (Set ($#k11_fsm_1 :::"the_reduction_of"::: ) (Set (Var "tfsm"))) ($#r4_fsm_1 :::"-are_equivalent"::: ) ))) ; begin definitionlet "IAlph", "OAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "tfsm1", "tfsm2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Const "IAlph")) "," (Set (Const "OAlph")); pred "tfsm1" "," "tfsm2" :::"-are_isomorphic"::: means :: FSM_1:def 19 (Bool "ex" (Set (Var "Tf")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "tfsm1") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "tfsm2") "st" (Bool "(" (Bool (Set (Var "Tf")) "is" ($#v3_funct_2 :::"bijective"::: ) ) & (Bool (Set (Set (Var "Tf")) ($#k3_funct_2 :::"."::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" "tfsm1")) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" "tfsm2")) & (Bool "(" "for" (Set (Var "q11")) "being" ($#m1_subset_1 :::"State":::) "of" "tfsm1" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "IAlph" "holds" (Bool "(" (Bool (Set (Set (Var "Tf")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" "tfsm1") ($#k2_binop_1 :::"."::: ) "(" (Set (Var "q11")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" "tfsm2") ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "Tf")) ($#k3_funct_2 :::"."::: ) (Set (Var "q11")) ")" ) "," (Set (Var "s")) ")" )) & (Bool (Set (Set "the" ($#u3_fsm_1 :::"OFun"::: ) "of" "tfsm1") ($#k2_binop_1 :::"."::: ) "(" (Set (Var "q11")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_fsm_1 :::"OFun"::: ) "of" "tfsm2") ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "Tf")) ($#k3_funct_2 :::"."::: ) (Set (Var "q11")) ")" ) "," (Set (Var "s")) ")" )) ")" )) ")" ) ")" )); reflexivity (Bool "for" (Set (Var "tfsm1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Const "IAlph")) "," (Set (Const "OAlph")) (Bool "ex" (Set (Var "Tf")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "tfsm1"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "tfsm1"))) "st" (Bool "(" (Bool (Set (Var "Tf")) "is" ($#v3_funct_2 :::"bijective"::: ) ) & (Bool (Set (Set (Var "Tf")) ($#k3_funct_2 :::"."::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "tfsm1")))) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "tfsm1")))) & (Bool "(" "for" (Set (Var "q11")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm1")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "IAlph")) "holds" (Bool "(" (Bool (Set (Set (Var "Tf")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "tfsm1"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "q11")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "tfsm1"))) ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "Tf")) ($#k3_funct_2 :::"."::: ) (Set (Var "q11")) ")" ) "," (Set (Var "s")) ")" )) & (Bool (Set (Set "the" ($#u3_fsm_1 :::"OFun"::: ) "of" (Set (Var "tfsm1"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "q11")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_fsm_1 :::"OFun"::: ) "of" (Set (Var "tfsm1"))) ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "Tf")) ($#k3_funct_2 :::"."::: ) (Set (Var "q11")) ")" ) "," (Set (Var "s")) ")" )) ")" )) ")" ) ")" ))) ; symmetry (Bool "for" (Set (Var "tfsm1")) "," (Set (Var "tfsm2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Const "IAlph")) "," (Set (Const "OAlph")) "st" (Bool (Bool "ex" (Set (Var "Tf")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "tfsm1"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "tfsm2"))) "st" (Bool "(" (Bool (Set (Var "Tf")) "is" ($#v3_funct_2 :::"bijective"::: ) ) & (Bool (Set (Set (Var "Tf")) ($#k3_funct_2 :::"."::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "tfsm1")))) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "tfsm2")))) & (Bool "(" "for" (Set (Var "q11")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm1")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "IAlph")) "holds" (Bool "(" (Bool (Set (Set (Var "Tf")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "tfsm1"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "q11")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "tfsm2"))) ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "Tf")) ($#k3_funct_2 :::"."::: ) (Set (Var "q11")) ")" ) "," (Set (Var "s")) ")" )) & (Bool (Set (Set "the" ($#u3_fsm_1 :::"OFun"::: ) "of" (Set (Var "tfsm1"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "q11")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_fsm_1 :::"OFun"::: ) "of" (Set (Var "tfsm2"))) ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "Tf")) ($#k3_funct_2 :::"."::: ) (Set (Var "q11")) ")" ) "," (Set (Var "s")) ")" )) ")" )) ")" ) ")" ))) "holds" (Bool "ex" (Set (Var "Tf")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "tfsm2"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "tfsm1"))) "st" (Bool "(" (Bool (Set (Var "Tf")) "is" ($#v3_funct_2 :::"bijective"::: ) ) & (Bool (Set (Set (Var "Tf")) ($#k3_funct_2 :::"."::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "tfsm2")))) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "tfsm1")))) & (Bool "(" "for" (Set (Var "q11")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm2")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "IAlph")) "holds" (Bool "(" (Bool (Set (Set (Var "Tf")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "tfsm2"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "q11")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "tfsm1"))) ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "Tf")) ($#k3_funct_2 :::"."::: ) (Set (Var "q11")) ")" ) "," (Set (Var "s")) ")" )) & (Bool (Set (Set "the" ($#u3_fsm_1 :::"OFun"::: ) "of" (Set (Var "tfsm2"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "q11")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_fsm_1 :::"OFun"::: ) "of" (Set (Var "tfsm1"))) ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "Tf")) ($#k3_funct_2 :::"."::: ) (Set (Var "q11")) ")" ) "," (Set (Var "s")) ")" )) ")" )) ")" ) ")" ))) ; end; :: deftheorem defines :::"-are_isomorphic"::: FSM_1:def 19 : (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm1")) "," (Set (Var "tfsm2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "holds" (Bool "(" (Bool (Set (Var "tfsm1")) "," (Set (Var "tfsm2")) ($#r7_fsm_1 :::"-are_isomorphic"::: ) ) "iff" (Bool "ex" (Set (Var "Tf")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "tfsm1"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "tfsm2"))) "st" (Bool "(" (Bool (Set (Var "Tf")) "is" ($#v3_funct_2 :::"bijective"::: ) ) & (Bool (Set (Set (Var "Tf")) ($#k3_funct_2 :::"."::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "tfsm1")))) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "tfsm2")))) & (Bool "(" "for" (Set (Var "q11")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm1")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "IAlph")) "holds" (Bool "(" (Bool (Set (Set (Var "Tf")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "tfsm1"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "q11")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "tfsm2"))) ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "Tf")) ($#k3_funct_2 :::"."::: ) (Set (Var "q11")) ")" ) "," (Set (Var "s")) ")" )) & (Bool (Set (Set "the" ($#u3_fsm_1 :::"OFun"::: ) "of" (Set (Var "tfsm1"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "q11")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_fsm_1 :::"OFun"::: ) "of" (Set (Var "tfsm2"))) ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "Tf")) ($#k3_funct_2 :::"."::: ) (Set (Var "q11")) ")" ) "," (Set (Var "s")) ")" )) ")" )) ")" ) ")" )) ")" ))); theorem :: FSM_1:42 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm1")) "," (Set (Var "tfsm2")) "," (Set (Var "tfsm3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "st" (Bool (Bool (Set (Var "tfsm1")) "," (Set (Var "tfsm2")) ($#r7_fsm_1 :::"-are_isomorphic"::: ) ) & (Bool (Set (Var "tfsm2")) "," (Set (Var "tfsm3")) ($#r7_fsm_1 :::"-are_isomorphic"::: ) )) "holds" (Bool (Set (Var "tfsm1")) "," (Set (Var "tfsm3")) ($#r7_fsm_1 :::"-are_isomorphic"::: ) ))) ; theorem :: FSM_1:43 (Bool "for" (Set (Var "OAlph")) "," (Set (Var "IAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "IAlph")) (Bool "for" (Set (Var "tfsm1")) "," (Set (Var "tfsm2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "q11")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm1")) (Bool "for" (Set (Var "Tf")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "tfsm1"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "tfsm2"))) "st" (Bool (Bool "(" "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm1")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "IAlph")) "holds" (Bool (Set (Set (Var "Tf")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "tfsm1"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "tfsm2"))) ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "Tf")) ($#k3_funct_2 :::"."::: ) (Set (Var "q")) ")" ) "," (Set (Var "s")) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "w")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool (Set (Set (Var "Tf")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" "(" (Set (Var "q11")) "," (Set (Var "w")) ")" ($#k2_fsm_1 :::"-admissible"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "(" (Set "(" (Set (Var "Tf")) ($#k3_funct_2 :::"."::: ) (Set (Var "q11")) ")" ) "," (Set (Var "w")) ")" ($#k2_fsm_1 :::"-admissible"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k")))))))))) ; theorem :: FSM_1:44 (Bool "for" (Set (Var "OAlph")) "," (Set (Var "IAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm1")) "," (Set (Var "tfsm2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "q11")) "," (Set (Var "q12")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm1")) (Bool "for" (Set (Var "Tf")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "tfsm1"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "tfsm2"))) "st" (Bool (Bool "(" "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm1")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "IAlph")) "holds" (Bool "(" (Bool (Set (Set (Var "Tf")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "tfsm1"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "tfsm2"))) ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "Tf")) ($#k3_funct_2 :::"."::: ) (Set (Var "q")) ")" ) "," (Set (Var "s")) ")" )) & (Bool (Set (Set "the" ($#u3_fsm_1 :::"OFun"::: ) "of" (Set (Var "tfsm1"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_fsm_1 :::"OFun"::: ) "of" (Set (Var "tfsm2"))) ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "Tf")) ($#k3_funct_2 :::"."::: ) (Set (Var "q")) ")" ) "," (Set (Var "s")) ")" )) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Var "q11")) "," (Set (Var "q12")) ($#r5_fsm_1 :::"-are_equivalent"::: ) ) "iff" (Bool (Set (Set (Var "Tf")) ($#k3_funct_2 :::"."::: ) (Set (Var "q11"))) "," (Set (Set (Var "Tf")) ($#k3_funct_2 :::"."::: ) (Set (Var "q12"))) ($#r5_fsm_1 :::"-are_equivalent"::: ) ) ")" ))))) ; theorem :: FSM_1:45 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "rtfsm")) "," (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "qr1")) "," (Set (Var "qr2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "rtfsm")) "st" (Bool (Bool (Set (Var "rtfsm")) ($#r1_hidden :::"="::: ) (Set ($#k11_fsm_1 :::"the_reduction_of"::: ) (Set (Var "tfsm")))) & (Bool (Set (Var "qr1")) ($#r1_hidden :::"<>"::: ) (Set (Var "qr2")))) "holds" (Bool "not" (Bool (Set (Var "qr1")) "," (Set (Var "qr2")) ($#r5_fsm_1 :::"-are_equivalent"::: ) ))))) ; begin definitionlet "IAlph", "OAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Const "IAlph")) "," (Set (Const "OAlph")); attr "IT" is :::"reduced"::: means :: FSM_1:def 20 (Bool "for" (Set (Var "qa")) "," (Set (Var "qb")) "being" ($#m1_subset_1 :::"State":::) "of" "IT" "st" (Bool (Bool (Set (Var "qa")) ($#r1_hidden :::"<>"::: ) (Set (Var "qb")))) "holds" (Bool "not" (Bool (Set (Var "qa")) "," (Set (Var "qb")) ($#r5_fsm_1 :::"-are_equivalent"::: ) ))); end; :: deftheorem defines :::"reduced"::: FSM_1:def 20 : (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v5_fsm_1 :::"reduced"::: ) ) "iff" (Bool "for" (Set (Var "qa")) "," (Set (Var "qb")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "qa")) ($#r1_hidden :::"<>"::: ) (Set (Var "qb")))) "holds" (Bool "not" (Bool (Set (Var "qa")) "," (Set (Var "qb")) ($#r5_fsm_1 :::"-are_equivalent"::: ) ))) ")" ))); registrationlet "IAlph", "OAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "tfsm" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Const "IAlph")) "," (Set (Const "OAlph")); cluster (Set ($#k11_fsm_1 :::"the_reduction_of"::: ) "tfsm") -> ($#v2_fsm_1 :::"strict"::: ) ($#v5_fsm_1 :::"reduced"::: ) ; end; registrationlet "IAlph", "OAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v5_fsm_1 :::"reduced"::: ) for ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" "IAlph" "," "OAlph"; end; theorem :: FSM_1:46 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Rtfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v5_fsm_1 :::"reduced"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "holds" (Bool (Set (Var "Rtfsm")) "," (Set ($#k11_fsm_1 :::"the_reduction_of"::: ) (Set (Var "Rtfsm"))) ($#r7_fsm_1 :::"-are_isomorphic"::: ) ))) ; theorem :: FSM_1:47 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "holds" (Bool "(" (Bool (Set (Var "tfsm")) "is" ($#v5_fsm_1 :::"reduced"::: ) ) "iff" (Bool "ex" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "st" (Bool (Set (Var "tfsm")) "," (Set ($#k11_fsm_1 :::"the_reduction_of"::: ) (Set (Var "M"))) ($#r7_fsm_1 :::"-are_isomorphic"::: ) )) ")" ))) ; definitionlet "IAlph", "OAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "tfsm" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Const "IAlph")) "," (Set (Const "OAlph")); let "IT" be ($#m1_subset_1 :::"State":::) "of" (Set (Const "tfsm")); attr "IT" is :::"accessible"::: means :: FSM_1:def 21 (Bool "ex" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" "IAlph" "st" (Bool (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" "tfsm") "," (Set (Var "w")) ($#r1_fsm_1 :::"-leads_to"::: ) "IT")); end; :: deftheorem defines :::"accessible"::: FSM_1:def 21 : (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v6_fsm_1 :::"accessible"::: ) ) "iff" (Bool "ex" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "IAlph")) "st" (Bool (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "tfsm"))) "," (Set (Var "w")) ($#r1_fsm_1 :::"-leads_to"::: ) (Set (Var "IT")))) ")" )))); definitionlet "IAlph", "OAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Const "IAlph")) "," (Set (Const "OAlph")); attr "IT" is :::"connected"::: means :: FSM_1:def 22 (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" "IT" "holds" (Bool (Set (Var "q")) "is" ($#v6_fsm_1 :::"accessible"::: ) )); end; :: deftheorem defines :::"connected"::: FSM_1:def 22 : (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v7_fsm_1 :::"connected"::: ) ) "iff" (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Var "q")) "is" ($#v6_fsm_1 :::"accessible"::: ) )) ")" ))); registrationlet "IAlph", "OAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v7_fsm_1 :::"connected"::: ) for ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" "IAlph" "," "OAlph"; end; registrationlet "IAlph", "OAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Ctfsm" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v7_fsm_1 :::"connected"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Const "IAlph")) "," (Set (Const "OAlph")); cluster (Set ($#k11_fsm_1 :::"the_reduction_of"::: ) "Ctfsm") -> ($#v2_fsm_1 :::"strict"::: ) ($#v7_fsm_1 :::"connected"::: ) ; end; registrationlet "IAlph", "OAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v5_fsm_1 :::"reduced"::: ) ($#v7_fsm_1 :::"connected"::: ) for ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" "IAlph" "," "OAlph"; end; definitionlet "IAlph", "OAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "tfsm" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Const "IAlph")) "," (Set (Const "OAlph")); func :::"accessibleStates"::: "tfsm" -> ($#m1_hidden :::"set"::: ) equals :: FSM_1:def 23 "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"State":::) "of" "tfsm" : (Bool (Set (Var "q")) "is" ($#v6_fsm_1 :::"accessible"::: ) ) "}" ; end; :: deftheorem defines :::"accessibleStates"::: FSM_1:def 23 : (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "holds" (Bool (Set ($#k12_fsm_1 :::"accessibleStates"::: ) (Set (Var "tfsm"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) : (Bool (Set (Var "q")) "is" ($#v6_fsm_1 :::"accessible"::: ) ) "}" ))); registrationlet "IAlph", "OAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "tfsm" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Const "IAlph")) "," (Set (Const "OAlph")); cluster (Set ($#k12_fsm_1 :::"accessibleStates"::: ) "tfsm") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: FSM_1:48 (Bool "for" (Set (Var "OAlph")) "," (Set (Var "IAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "holds" (Bool "(" (Bool (Set ($#k12_fsm_1 :::"accessibleStates"::: ) (Set (Var "tfsm"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "tfsm")))) & (Bool "(" "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) "holds" (Bool "(" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k12_fsm_1 :::"accessibleStates"::: ) (Set (Var "tfsm")))) "iff" (Bool (Set (Var "q")) "is" ($#v6_fsm_1 :::"accessible"::: ) ) ")" ) ")" ) ")" ))) ; theorem :: FSM_1:49 (Bool "for" (Set (Var "OAlph")) "," (Set (Var "IAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "holds" (Bool (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "tfsm"))) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k12_fsm_1 :::"accessibleStates"::: ) (Set (Var "tfsm")) ")" ) "," (Set (Var "IAlph")) ($#k2_zfmisc_1 :::":]"::: ) )) "is" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k12_fsm_1 :::"accessibleStates"::: ) (Set (Var "tfsm")) ")" ) "," (Set (Var "IAlph")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k12_fsm_1 :::"accessibleStates"::: ) (Set (Var "tfsm")) ")" )))) ; theorem :: FSM_1:50 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "cTran")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k12_fsm_1 :::"accessibleStates"::: ) (Set (Var "tfsm")) ")" ) "," (Set (Var "IAlph")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k12_fsm_1 :::"accessibleStates"::: ) (Set (Var "tfsm")) ")" ) (Bool "for" (Set (Var "cOFun")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k12_fsm_1 :::"accessibleStates"::: ) (Set (Var "tfsm")) ")" ) "," (Set (Var "IAlph")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "cInitS")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k12_fsm_1 :::"accessibleStates"::: ) (Set (Var "tfsm"))) "st" (Bool (Bool (Set (Var "cTran")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "tfsm"))) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k12_fsm_1 :::"accessibleStates"::: ) (Set (Var "tfsm")) ")" ) "," (Set (Var "IAlph")) ($#k2_zfmisc_1 :::":]"::: ) ))) & (Bool (Set (Var "cOFun")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_fsm_1 :::"OFun"::: ) "of" (Set (Var "tfsm"))) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k12_fsm_1 :::"accessibleStates"::: ) (Set (Var "tfsm")) ")" ) "," (Set (Var "IAlph")) ($#k2_zfmisc_1 :::":]"::: ) ))) & (Bool (Set (Var "cInitS")) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "tfsm"))))) "holds" (Bool (Set (Var "tfsm")) "," (Set ($#g2_fsm_1 :::"Mealy-FSM"::: ) "(#" (Set "(" ($#k12_fsm_1 :::"accessibleStates"::: ) (Set (Var "tfsm")) ")" ) "," (Set (Var "cTran")) "," (Set (Var "cOFun")) "," (Set (Var "cInitS")) "#)" ) ($#r4_fsm_1 :::"-are_equivalent"::: ) )))))) ; theorem :: FSM_1:51 (Bool "for" (Set (Var "OAlph")) "," (Set (Var "IAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "ex" (Set (Var "Ctfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v7_fsm_1 :::"connected"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "st" (Bool "(" (Bool (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "Ctfsm"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "tfsm"))) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k12_fsm_1 :::"accessibleStates"::: ) (Set (Var "tfsm")) ")" ) "," (Set (Var "IAlph")) ($#k2_zfmisc_1 :::":]"::: ) ))) & (Bool (Set "the" ($#u3_fsm_1 :::"OFun"::: ) "of" (Set (Var "Ctfsm"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_fsm_1 :::"OFun"::: ) "of" (Set (Var "tfsm"))) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k12_fsm_1 :::"accessibleStates"::: ) (Set (Var "tfsm")) ")" ) "," (Set (Var "IAlph")) ($#k2_zfmisc_1 :::":]"::: ) ))) & (Bool (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "Ctfsm"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "tfsm")))) & (Bool (Set (Var "tfsm")) "," (Set (Var "Ctfsm")) ($#r4_fsm_1 :::"-are_equivalent"::: ) ) ")" )))) ; begin definitionlet "IAlph" be ($#m1_hidden :::"set"::: ) ; let "OAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "tfsm1", "tfsm2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Const "IAlph")) "," (Set (Const "OAlph")); func "tfsm1" :::"-Mealy_union"::: "tfsm2" -> ($#v2_fsm_1 :::"strict"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" "IAlph" "," "OAlph" means :: FSM_1:def 24 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "tfsm1") ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "tfsm2"))) & (Bool (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" "tfsm1") ($#k1_funct_4 :::"+*"::: ) (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" "tfsm2"))) & (Bool (Set "the" ($#u3_fsm_1 :::"OFun"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_fsm_1 :::"OFun"::: ) "of" "tfsm1") ($#k1_funct_4 :::"+*"::: ) (Set "the" ($#u3_fsm_1 :::"OFun"::: ) "of" "tfsm2"))) & (Bool (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" "tfsm1")) ")" ); end; :: deftheorem defines :::"-Mealy_union"::: FSM_1:def 24 : (Bool "for" (Set (Var "IAlph")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm1")) "," (Set (Var "tfsm2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "b5")) "being" ($#v2_fsm_1 :::"strict"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "tfsm1")) ($#k13_fsm_1 :::"-Mealy_union"::: ) (Set (Var "tfsm2")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "tfsm1"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "tfsm2"))))) & (Bool (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "tfsm1"))) ($#k1_funct_4 :::"+*"::: ) (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "tfsm2"))))) & (Bool (Set "the" ($#u3_fsm_1 :::"OFun"::: ) "of" (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_fsm_1 :::"OFun"::: ) "of" (Set (Var "tfsm1"))) ($#k1_funct_4 :::"+*"::: ) (Set "the" ($#u3_fsm_1 :::"OFun"::: ) "of" (Set (Var "tfsm2"))))) & (Bool (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "tfsm1")))) ")" ) ")" ))))); registrationlet "IAlph" be ($#m1_hidden :::"set"::: ) ; let "OAlph" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "tfsm1", "tfsm2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Const "IAlph")) "," (Set (Const "OAlph")); cluster (Set "tfsm1" ($#k13_fsm_1 :::"-Mealy_union"::: ) "tfsm2") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v2_fsm_1 :::"strict"::: ) ; end; theorem :: FSM_1:52 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "IAlph")) (Bool "for" (Set (Var "tfsm1")) "," (Set (Var "tfsm2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "q11")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm1")) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) "st" (Bool (Bool (Set (Var "tfsm")) ($#r1_hidden :::"="::: ) (Set (Set (Var "tfsm1")) ($#k13_fsm_1 :::"-Mealy_union"::: ) (Set (Var "tfsm2")))) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "tfsm1"))) ($#r1_subset_1 :::"misses"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "tfsm2")))) & (Bool (Set (Var "q11")) ($#r1_hidden :::"="::: ) (Set (Var "q")))) "holds" (Bool (Set "(" (Set (Var "q11")) "," (Set (Var "w")) ")" ($#k2_fsm_1 :::"-admissible"::: ) ) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "q")) "," (Set (Var "w")) ")" ($#k2_fsm_1 :::"-admissible"::: ) )))))))) ; theorem :: FSM_1:53 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "IAlph")) (Bool "for" (Set (Var "tfsm1")) "," (Set (Var "tfsm2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "q11")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm1")) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) "st" (Bool (Bool (Set (Var "tfsm")) ($#r1_hidden :::"="::: ) (Set (Set (Var "tfsm1")) ($#k13_fsm_1 :::"-Mealy_union"::: ) (Set (Var "tfsm2")))) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "tfsm1"))) ($#r1_subset_1 :::"misses"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "tfsm2")))) & (Bool (Set (Var "q11")) ($#r1_hidden :::"="::: ) (Set (Var "q")))) "holds" (Bool (Set "(" (Set (Var "q11")) "," (Set (Var "w")) ")" ($#k4_fsm_1 :::"-response"::: ) ) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "q")) "," (Set (Var "w")) ")" ($#k4_fsm_1 :::"-response"::: ) )))))))) ; theorem :: FSM_1:54 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "IAlph")) (Bool "for" (Set (Var "tfsm1")) "," (Set (Var "tfsm2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "q21")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm2")) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) "st" (Bool (Bool (Set (Var "tfsm")) ($#r1_hidden :::"="::: ) (Set (Set (Var "tfsm1")) ($#k13_fsm_1 :::"-Mealy_union"::: ) (Set (Var "tfsm2")))) & (Bool (Set (Var "q21")) ($#r1_hidden :::"="::: ) (Set (Var "q")))) "holds" (Bool (Set "(" (Set (Var "q21")) "," (Set (Var "w")) ")" ($#k2_fsm_1 :::"-admissible"::: ) ) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "q")) "," (Set (Var "w")) ")" ($#k2_fsm_1 :::"-admissible"::: ) )))))))) ; theorem :: FSM_1:55 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "IAlph")) (Bool "for" (Set (Var "tfsm1")) "," (Set (Var "tfsm2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "q21")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm2")) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) "st" (Bool (Bool (Set (Var "tfsm")) ($#r1_hidden :::"="::: ) (Set (Set (Var "tfsm1")) ($#k13_fsm_1 :::"-Mealy_union"::: ) (Set (Var "tfsm2")))) & (Bool (Set (Var "q21")) ($#r1_hidden :::"="::: ) (Set (Var "q")))) "holds" (Bool (Set "(" (Set (Var "q21")) "," (Set (Var "w")) ")" ($#k4_fsm_1 :::"-response"::: ) ) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "q")) "," (Set (Var "w")) ")" ($#k4_fsm_1 :::"-response"::: ) )))))))) ; theorem :: FSM_1:56 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "Rtfsm1")) "," (Set (Var "Rtfsm2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_fsm_1 :::"reduced"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "st" (Bool (Bool (Set (Var "tfsm")) ($#r1_hidden :::"="::: ) (Set (Set (Var "Rtfsm1")) ($#k13_fsm_1 :::"-Mealy_union"::: ) (Set (Var "Rtfsm2")))) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Rtfsm1"))) ($#r1_subset_1 :::"misses"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Rtfsm2")))) & (Bool (Set (Var "Rtfsm1")) "," (Set (Var "Rtfsm2")) ($#r4_fsm_1 :::"-are_equivalent"::: ) )) "holds" (Bool "ex" (Set (Var "Q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k11_fsm_1 :::"the_reduction_of"::: ) (Set (Var "tfsm")) ")" ) "st" (Bool "(" (Bool (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "Rtfsm1"))) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "Rtfsm2"))) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set "(" ($#k11_fsm_1 :::"the_reduction_of"::: ) (Set (Var "tfsm")) ")" ))) ")" ))))) ; theorem :: FSM_1:57 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "CRtfsm1")) "," (Set (Var "CRtfsm2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_fsm_1 :::"reduced"::: ) ($#v7_fsm_1 :::"connected"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "q1u")) "," (Set (Var "q2u")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) (Bool "for" (Set (Var "crq11")) "," (Set (Var "crq12")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "CRtfsm1")) "st" (Bool (Bool (Set (Var "crq11")) ($#r1_hidden :::"="::: ) (Set (Var "q1u"))) & (Bool (Set (Var "crq12")) ($#r1_hidden :::"="::: ) (Set (Var "q2u"))) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CRtfsm1"))) ($#r1_subset_1 :::"misses"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CRtfsm2")))) & (Bool (Set (Var "tfsm")) ($#r1_hidden :::"="::: ) (Set (Set (Var "CRtfsm1")) ($#k13_fsm_1 :::"-Mealy_union"::: ) (Set (Var "CRtfsm2")))) & (Bool (Bool "not" (Set (Var "crq11")) "," (Set (Var "crq12")) ($#r5_fsm_1 :::"-are_equivalent"::: ) ))) "holds" (Bool "not" (Bool (Set (Var "q1u")) "," (Set (Var "q2u")) ($#r5_fsm_1 :::"-are_equivalent"::: ) ))))))) ; theorem :: FSM_1:58 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "CRtfsm2")) "," (Set (Var "CRtfsm1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_fsm_1 :::"reduced"::: ) ($#v7_fsm_1 :::"connected"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "q1u")) "," (Set (Var "q2u")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "tfsm")) (Bool "for" (Set (Var "crq21")) "," (Set (Var "crq22")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "CRtfsm2")) "st" (Bool (Bool (Set (Var "crq21")) ($#r1_hidden :::"="::: ) (Set (Var "q1u"))) & (Bool (Set (Var "crq22")) ($#r1_hidden :::"="::: ) (Set (Var "q2u"))) & (Bool (Set (Var "tfsm")) ($#r1_hidden :::"="::: ) (Set (Set (Var "CRtfsm1")) ($#k13_fsm_1 :::"-Mealy_union"::: ) (Set (Var "CRtfsm2")))) & (Bool (Bool "not" (Set (Var "crq21")) "," (Set (Var "crq22")) ($#r5_fsm_1 :::"-are_equivalent"::: ) ))) "holds" (Bool "not" (Bool (Set (Var "q1u")) "," (Set (Var "q2u")) ($#r5_fsm_1 :::"-are_equivalent"::: ) ))))))) ; theorem :: FSM_1:59 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "CRtfsm1")) "," (Set (Var "CRtfsm2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v5_fsm_1 :::"reduced"::: ) ($#v7_fsm_1 :::"connected"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CRtfsm1"))) ($#r1_subset_1 :::"misses"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CRtfsm2")))) & (Bool (Set (Var "tfsm")) ($#r1_hidden :::"="::: ) (Set (Set (Var "CRtfsm1")) ($#k13_fsm_1 :::"-Mealy_union"::: ) (Set (Var "CRtfsm2"))))) "holds" (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k11_fsm_1 :::"the_reduction_of"::: ) (Set (Var "tfsm")) ")" ) (Bool "for" (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Q")) "holds" (Bool "(" "not" (Bool (Set (Var "q1")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CRtfsm1")))) "or" "not" (Bool (Set (Var "q2")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CRtfsm1")))) "or" "not" (Bool (Set (Var "q1")) ($#r1_hidden :::"<>"::: ) (Set (Var "q2"))) ")" )))))) ; theorem :: FSM_1:60 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "CRtfsm1")) "," (Set (Var "CRtfsm2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v5_fsm_1 :::"reduced"::: ) ($#v7_fsm_1 :::"connected"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "st" (Bool (Bool (Set (Var "tfsm")) ($#r1_hidden :::"="::: ) (Set (Set (Var "CRtfsm1")) ($#k13_fsm_1 :::"-Mealy_union"::: ) (Set (Var "CRtfsm2"))))) "holds" (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k11_fsm_1 :::"the_reduction_of"::: ) (Set (Var "tfsm")) ")" ) (Bool "for" (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Q")) "holds" (Bool "(" "not" (Bool (Set (Var "q1")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CRtfsm2")))) "or" "not" (Bool (Set (Var "q2")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CRtfsm2")))) "or" "not" (Bool (Set (Var "q1")) ($#r1_hidden :::"<>"::: ) (Set (Var "q2"))) ")" )))))) ; theorem :: FSM_1:61 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "for" (Set (Var "CRtfsm1")) "," (Set (Var "CRtfsm2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v5_fsm_1 :::"reduced"::: ) ($#v7_fsm_1 :::"connected"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CRtfsm1"))) ($#r1_subset_1 :::"misses"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CRtfsm2")))) & (Bool (Set (Var "CRtfsm1")) "," (Set (Var "CRtfsm2")) ($#r4_fsm_1 :::"-are_equivalent"::: ) ) & (Bool (Set (Var "tfsm")) ($#r1_hidden :::"="::: ) (Set (Set (Var "CRtfsm1")) ($#k13_fsm_1 :::"-Mealy_union"::: ) (Set (Var "CRtfsm2"))))) "holds" (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k11_fsm_1 :::"the_reduction_of"::: ) (Set (Var "tfsm")) ")" ) (Bool "ex" (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Q")) "st" (Bool "(" (Bool (Set (Var "q1")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CRtfsm1")))) & (Bool (Set (Var "q2")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CRtfsm2")))) & (Bool "(" "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Q")) "holds" (Bool "(" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "q1"))) "or" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "q2"))) ")" ) ")" ) ")" )))))) ; begin theorem :: FSM_1:62 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm1")) "," (Set (Var "tfsm2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) (Bool "ex" (Set (Var "fsm1")) "," (Set (Var "fsm2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "st" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "fsm1"))) ($#r1_subset_1 :::"misses"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "fsm2")))) & (Bool (Set (Var "fsm1")) "," (Set (Var "tfsm1")) ($#r7_fsm_1 :::"-are_isomorphic"::: ) ) & (Bool (Set (Var "fsm2")) "," (Set (Var "tfsm2")) ($#r7_fsm_1 :::"-are_isomorphic"::: ) ) ")" )))) ; theorem :: FSM_1:63 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "tfsm1")) "," (Set (Var "tfsm2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "st" (Bool (Bool (Set (Var "tfsm1")) "," (Set (Var "tfsm2")) ($#r7_fsm_1 :::"-are_isomorphic"::: ) )) "holds" (Bool (Set (Var "tfsm1")) "," (Set (Var "tfsm2")) ($#r4_fsm_1 :::"-are_equivalent"::: ) ))) ; theorem :: FSM_1:64 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "CRtfsm1")) "," (Set (Var "CRtfsm2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v5_fsm_1 :::"reduced"::: ) ($#v7_fsm_1 :::"connected"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CRtfsm1"))) ($#r1_subset_1 :::"misses"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CRtfsm2")))) & (Bool (Set (Var "CRtfsm1")) "," (Set (Var "CRtfsm2")) ($#r4_fsm_1 :::"-are_equivalent"::: ) )) "holds" (Bool (Set (Var "CRtfsm1")) "," (Set (Var "CRtfsm2")) ($#r7_fsm_1 :::"-are_isomorphic"::: ) ))) ; theorem :: FSM_1:65 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Ctfsm1")) "," (Set (Var "Ctfsm2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v7_fsm_1 :::"connected"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "st" (Bool (Bool (Set (Var "Ctfsm1")) "," (Set (Var "Ctfsm2")) ($#r4_fsm_1 :::"-are_equivalent"::: ) )) "holds" (Bool (Set ($#k11_fsm_1 :::"the_reduction_of"::: ) (Set (Var "Ctfsm1"))) "," (Set ($#k11_fsm_1 :::"the_reduction_of"::: ) (Set (Var "Ctfsm2"))) ($#r7_fsm_1 :::"-are_isomorphic"::: ) ))) ; theorem :: FSM_1:66 (Bool "for" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v5_fsm_1 :::"reduced"::: ) ($#v7_fsm_1 :::"connected"::: ) ($#l2_fsm_1 :::"Mealy-FSM"::: ) "over" (Set (Var "IAlph")) "," (Set (Var "OAlph")) "holds" (Bool "(" (Bool (Set (Var "M1")) "," (Set (Var "M2")) ($#r7_fsm_1 :::"-are_isomorphic"::: ) ) "iff" (Bool (Set (Var "M1")) "," (Set (Var "M2")) ($#r4_fsm_1 :::"-are_equivalent"::: ) ) ")" ))) ;