:: FSM_2 semantic presentation begin notationlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Const "I")); let "q" be ($#m1_subset_1 :::"State":::) "of" (Set (Const "S")); let "w" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "I")); synonym :::"GEN"::: "(" "w" "," "q" ")" for "(" "q" "," "w" ")" :::"-admissible"::: ; end; registrationlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Const "I")); let "q" be ($#m1_subset_1 :::"State":::) "of" (Set (Const "S")); let "w" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "I")); cluster (Set ($#k2_fsm_1 :::"GEN"::: ) "(" "w" "," "q" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: FSM_2:1 (Bool "for" (Set (Var "I")) "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 "I")) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "I")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k2_fsm_1 :::"GEN"::: ) "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "s")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "q")) "," (Set "(" (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "S"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "s")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ($#k2_finseq_4 :::"*>"::: ) )))))) ; theorem :: FSM_2:2 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "I")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k2_fsm_1 :::"GEN"::: ) "(" (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "s1")) "," (Set (Var "s2")) ($#k2_finseq_4 :::"*>"::: ) ) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "q")) "," (Set "(" (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "S"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "s1")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set "(" (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "S"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "S"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "s1")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set (Var "s2")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ($#k3_finseq_4 :::"*>"::: ) )))))) ; theorem :: FSM_2:3 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "s3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "I")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k2_fsm_1 :::"GEN"::: ) "(" (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "s3")) ($#k3_finseq_4 :::"*>"::: ) ) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_4 :::"<*"::: ) (Set (Var "q")) "," (Set "(" (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "S"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "s1")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set "(" (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "S"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "S"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "s1")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set (Var "s2")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set "(" (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "S"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "S"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "S"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "s1")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set (Var "s2")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set (Var "s3")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ($#k9_finseq_4 :::"*>"::: ) )))))) ; definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Const "I")); attr "S" is :::"calculating_type"::: means :: FSM_2:def 1 (Bool "for" (Set (Var "j")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" "I" "st" (Bool (Bool (Set (Set (Var "w1")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "w2")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "w1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "w2")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool (Set (Set "(" ($#k2_fsm_1 :::"GEN"::: ) "(" (Set (Var "w1")) "," (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" "S") ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_fsm_1 :::"GEN"::: ) "(" (Set (Var "w2")) "," (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" "S") ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "j")))))); end; :: deftheorem defines :::"calculating_type"::: FSM_2:def 1 : (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v1_fsm_2 :::"calculating_type"::: ) ) "iff" (Bool "for" (Set (Var "j")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Set (Var "w1")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "w2")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "w1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "w2")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool (Set (Set "(" ($#k2_fsm_1 :::"GEN"::: ) "(" (Set (Var "w1")) "," (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "S"))) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_fsm_1 :::"GEN"::: ) "(" (Set (Var "w2")) "," (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "S"))) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "j")))))) ")" ))); theorem :: FSM_2:4 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "I")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v1_fsm_2 :::"calculating_type"::: ) )) "holds" (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Set (Var "w1")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "w2")) ($#k1_funct_1 :::"."::: ) (Num 1)))) "holds" (Bool (Set ($#k2_fsm_1 :::"GEN"::: ) "(" (Set (Var "w1")) "," (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "S"))) ")" ) "," (Set ($#k2_fsm_1 :::"GEN"::: ) "(" (Set (Var "w2")) "," (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "S"))) ")" ) ($#r3_xboole_0 :::"are_c=-comparable"::: ) )))) ; theorem :: FSM_2:5 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "I")) "st" (Bool (Bool "(" "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Set (Var "w1")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "w2")) ($#k1_funct_1 :::"."::: ) (Num 1)))) "holds" (Bool (Set ($#k2_fsm_1 :::"GEN"::: ) "(" (Set (Var "w1")) "," (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "S"))) ")" ) "," (Set ($#k2_fsm_1 :::"GEN"::: ) "(" (Set (Var "w2")) "," (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "S"))) ")" ) ($#r3_xboole_0 :::"are_c=-comparable"::: ) ) ")" )) "holds" (Bool (Set (Var "S")) "is" ($#v1_fsm_2 :::"calculating_type"::: ) ))) ; theorem :: FSM_2:6 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "I")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v1_fsm_2 :::"calculating_type"::: ) )) "holds" (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Set (Var "w1")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "w2")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "w1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "w2"))))) "holds" (Bool (Set ($#k2_fsm_1 :::"GEN"::: ) "(" (Set (Var "w1")) "," (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "S"))) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_fsm_1 :::"GEN"::: ) "(" (Set (Var "w2")) "," (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "S"))) ")" ))))) ; theorem :: FSM_2:7 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "I")) "st" (Bool (Bool "(" "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Set (Var "w1")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "w2")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "w1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "w2"))))) "holds" (Bool (Set ($#k2_fsm_1 :::"GEN"::: ) "(" (Set (Var "w1")) "," (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "S"))) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_fsm_1 :::"GEN"::: ) "(" (Set (Var "w2")) "," (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "S"))) ")" )) ")" )) "holds" (Bool (Set (Var "S")) "is" ($#v1_fsm_2 :::"calculating_type"::: ) ))) ; definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Const "I")); let "q" be ($#m1_subset_1 :::"State":::) "of" (Set (Const "S")); let "s" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")); pred "q" :::"is_accessible_via"::: "s" means :: FSM_2:def 2 (Bool "ex" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" "I" "st" (Bool (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" "S") "," (Set (Set ($#k12_finseq_1 :::"<*"::: ) "s" ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "w"))) ($#r1_fsm_1 :::"-leads_to"::: ) "q")); end; :: deftheorem defines :::"is_accessible_via"::: FSM_2:def 2 : (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "I")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "q")) ($#r1_fsm_2 :::"is_accessible_via"::: ) (Set (Var "s"))) "iff" (Bool "ex" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "I")) "st" (Bool (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "S"))) "," (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "s")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "w"))) ($#r1_fsm_1 :::"-leads_to"::: ) (Set (Var "q")))) ")" ))))); definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Const "I")); let "q" be ($#m1_subset_1 :::"State":::) "of" (Set (Const "S")); attr "q" is :::"accessible"::: means :: FSM_2:def 3 (Bool "ex" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" "I" "st" (Bool (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" "S") "," (Set (Var "w")) ($#r1_fsm_1 :::"-leads_to"::: ) "q")); end; :: deftheorem defines :::"accessible"::: FSM_2:def 3 : (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "I")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "q")) "is" ($#v2_fsm_2 :::"accessible"::: ) ) "iff" (Bool "ex" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "I")) "st" (Bool (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "S"))) "," (Set (Var "w")) ($#r1_fsm_1 :::"-leads_to"::: ) (Set (Var "q")))) ")" )))); theorem :: FSM_2:8 (Bool "for" (Set (Var "I")) "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 "I")) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "I")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "q")) ($#r1_fsm_2 :::"is_accessible_via"::: ) (Set (Var "s")))) "holds" (Bool (Set (Var "q")) "is" ($#v2_fsm_2 :::"accessible"::: ) ))))) ; theorem :: FSM_2:9 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "I")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "q")) "is" ($#v2_fsm_2 :::"accessible"::: ) ) & (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "S"))))) "holds" (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "st" (Bool (Set (Var "q")) ($#r1_fsm_2 :::"is_accessible_via"::: ) (Set (Var "s"))))))) ; theorem :: FSM_2:10 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "I")) "holds" (Bool (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "S"))) "is" ($#v2_fsm_2 :::"accessible"::: ) ))) ; theorem :: FSM_2:11 (Bool "for" (Set (Var "I")) "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 "I")) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "I")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v1_fsm_2 :::"calculating_type"::: ) ) & (Bool (Set (Var "q")) ($#r1_fsm_2 :::"is_accessible_via"::: ) (Set (Var "s")))) "holds" (Bool "ex" (Set (Var "m")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "w")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::">="::: ) (Set (Var "m"))) & (Bool (Set (Set (Var "w")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "s")))) "holds" (Bool "(" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_fsm_1 :::"GEN"::: ) "(" (Set (Var "w")) "," (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "S"))) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "m")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool (Set (Set "(" ($#k2_fsm_1 :::"GEN"::: ) "(" (Set (Var "w")) "," (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "S"))) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) ")" ) ")" ))))))) ; definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Const "I")); attr "S" is :::"regular"::: means :: FSM_2:def 4 (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" "S" "holds" (Bool (Set (Var "q")) "is" ($#v2_fsm_2 :::"accessible"::: ) )); end; :: deftheorem defines :::"regular"::: FSM_2:def 4 : (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_fsm_2 :::"regular"::: ) ) "iff" (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "S")) "holds" (Bool (Set (Var "q")) "is" ($#v2_fsm_2 :::"accessible"::: ) )) ")" ))); theorem :: FSM_2:12 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "I")) "st" (Bool (Bool "(" "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "S"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "s1")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "S"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "s2")) ($#k1_domain_1 :::"]"::: ) )))) ")" )) "holds" (Bool (Set (Var "S")) "is" ($#v1_fsm_2 :::"calculating_type"::: ) ))) ; theorem :: FSM_2:13 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "I")) "st" (Bool (Bool "(" "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "S"))))) "holds" (Bool (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "S"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "s1")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "S"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "s2")) ($#k1_domain_1 :::"]"::: ) )))) ")" ) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "q1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "S"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "q1")) "," (Set (Var "s")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "S"))))) ")" )) "holds" (Bool (Set (Var "S")) "is" ($#v1_fsm_2 :::"calculating_type"::: ) ))) ; theorem :: FSM_2:14 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "I")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v3_fsm_2 :::"regular"::: ) ) & (Bool (Set (Var "S")) "is" ($#v1_fsm_2 :::"calculating_type"::: ) )) "holds" (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "S"))))) "holds" (Bool (Set (Set "(" ($#k2_fsm_1 :::"GEN"::: ) "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "s1")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "q")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_fsm_1 :::"GEN"::: ) "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "s2")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "q")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Num 2))))))) ; theorem :: FSM_2:15 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "I")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v3_fsm_2 :::"regular"::: ) ) & (Bool (Set (Var "S")) "is" ($#v1_fsm_2 :::"calculating_type"::: ) )) "holds" (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "S"))))) "holds" (Bool (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "S"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "s1")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "S"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "s2")) ($#k1_domain_1 :::"]"::: ) ))))))) ; theorem :: FSM_2:16 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_1 :::"FSM"::: ) "over" (Set (Var "I")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v3_fsm_2 :::"regular"::: ) ) & (Bool (Set (Var "S")) "is" ($#v1_fsm_2 :::"calculating_type"::: ) )) "holds" (Bool "for" (Set (Var "s")) "," (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "S"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "S"))) "," (Set (Var "s1")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"<>"::: ) (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "S"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "S"))) "," (Set (Var "s2")) ($#k1_domain_1 :::"]"::: ) )))) "holds" (Bool (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "S"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "s")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "S")))))))) ; begin definitionlet "I" be ($#m1_hidden :::"set"::: ) ; attr "c2" is :::"strict"::: ; struct :::"SM_Final"::: "over" "I" -> ($#l1_fsm_1 :::"FSM"::: ) "over" "I"; aggr :::"SM_Final":::(# :::"carrier":::, :::"Tran":::, :::"InitS":::, :::"FinalS"::: #) -> ($#l1_fsm_2 :::"SM_Final"::: ) "over" "I"; sel :::"FinalS"::: "c2" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c2"); end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#l1_fsm_2 :::"SM_Final"::: ) "over" "I"; end; definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "s" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")); let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_2 :::"SM_Final"::: ) "over" (Set (Const "I")); pred "s" :::"leads_to_final_state_of"::: "S" means :: FSM_2:def 5 (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" "S" "st" (Bool "(" (Bool (Set (Var "q")) ($#r1_fsm_2 :::"is_accessible_via"::: ) "s") & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_fsm_2 :::"FinalS"::: ) "of" "S")) ")" )); end; :: deftheorem defines :::"leads_to_final_state_of"::: FSM_2:def 5 : (Bool "for" (Set (Var "I")) "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 "I")) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_2 :::"SM_Final"::: ) "over" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "s")) ($#r2_fsm_2 :::"leads_to_final_state_of"::: ) (Set (Var "S"))) "iff" (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "q")) ($#r1_fsm_2 :::"is_accessible_via"::: ) (Set (Var "s"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_fsm_2 :::"FinalS"::: ) "of" (Set (Var "S")))) ")" )) ")" )))); definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_2 :::"SM_Final"::: ) "over" (Set (Const "I")); attr "S" is :::"halting"::: means :: FSM_2:def 6 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "I" "holds" (Bool (Set (Var "s")) ($#r2_fsm_2 :::"leads_to_final_state_of"::: ) "S")); end; :: deftheorem defines :::"halting"::: FSM_2:def 6 : (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fsm_2 :::"SM_Final"::: ) "over" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v5_fsm_2 :::"halting"::: ) ) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Var "s")) ($#r2_fsm_2 :::"leads_to_final_state_of"::: ) (Set (Var "S")))) ")" ))); definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "O" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; attr "c3" is :::"strict"::: ; struct :::"Moore-SM_Final"::: "over" "I" "," "O" -> ($#l1_fsm_2 :::"SM_Final"::: ) "over" "I" "," ($#l3_fsm_1 :::"Moore-FSM"::: ) "over" "I" "," "O"; aggr :::"Moore-SM_Final":::(# :::"carrier":::, :::"Tran":::, :::"OFun":::, :::"InitS":::, :::"FinalS"::: #) -> ($#l2_fsm_2 :::"Moore-SM_Final"::: ) "over" "I" "," "O"; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "O" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_fsm_2 :::"strict"::: ) for ($#l2_fsm_2 :::"Moore-SM_Final"::: ) "over" "I" "," "O"; end; definitionlet "I", "O" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "i", "f" be ($#m1_hidden :::"set"::: ) ; let "o" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_tarski :::"{"::: ) (Set (Const "i")) "," (Set (Const "f")) ($#k2_tarski :::"}"::: ) ) "," (Set (Const "O")); func "I" :::"-TwoStatesMooreSM"::: "(" "i" "," "f" "," "o" ")" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_fsm_2 :::"strict"::: ) ($#l2_fsm_2 :::"Moore-SM_Final"::: ) "over" "I" "," "O" means :: FSM_2:def 7 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) "i" "," "f" ($#k2_tarski :::"}"::: ) )) & (Bool (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" it) ($#r1_funct_2 :::"="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_tarski :::"{"::: ) "i" "," "f" ($#k2_tarski :::"}"::: ) ) "," "I" ($#k2_zfmisc_1 :::":]"::: ) ) ($#k7_funcop_1 :::"-->"::: ) "f")) & (Bool (Set "the" ($#u4_fsm_1 :::"OFun"::: ) "of" it) ($#r1_funct_2 :::"="::: ) "o") & (Bool (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" it) ($#r1_hidden :::"="::: ) "i") & (Bool (Set "the" ($#u1_fsm_2 :::"FinalS"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) "f" ($#k1_tarski :::"}"::: ) )) ")" ); end; :: deftheorem defines :::"-TwoStatesMooreSM"::: FSM_2:def 7 : (Bool "for" (Set (Var "I")) "," (Set (Var "O")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "," (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_tarski :::"{"::: ) (Set (Var "i")) "," (Set (Var "f")) ($#k2_tarski :::"}"::: ) ) "," (Set (Var "O")) (Bool "for" (Set (Var "b6")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_fsm_2 :::"strict"::: ) ($#l2_fsm_2 :::"Moore-SM_Final"::: ) "over" (Set (Var "I")) "," (Set (Var "O")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "I")) ($#k1_fsm_2 :::"-TwoStatesMooreSM"::: ) "(" (Set (Var "i")) "," (Set (Var "f")) "," (Set (Var "o")) ")" )) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b6"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "i")) "," (Set (Var "f")) ($#k2_tarski :::"}"::: ) )) & (Bool (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "b6"))) ($#r1_funct_2 :::"="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "i")) "," (Set (Var "f")) ($#k2_tarski :::"}"::: ) ) "," (Set (Var "I")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "f")))) & (Bool (Set "the" ($#u4_fsm_1 :::"OFun"::: ) "of" (Set (Var "b6"))) ($#r1_funct_2 :::"="::: ) (Set (Var "o"))) & (Bool (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "b6"))) ($#r1_hidden :::"="::: ) (Set (Var "i"))) & (Bool (Set "the" ($#u1_fsm_2 :::"FinalS"::: ) "of" (Set (Var "b6"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) )) ")" ) ")" ))))); theorem :: FSM_2:17 (Bool "for" (Set (Var "O")) "," (Set (Var "I")) "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 "I")) (Bool "for" (Set (Var "i")) "," (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_tarski :::"{"::: ) (Set (Var "i")) "," (Set (Var "f")) ($#k2_tarski :::"}"::: ) ) "," (Set (Var "O")) (Bool "for" (Set (Var "j")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "w")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool (Set (Set "(" ($#k2_fsm_1 :::"GEN"::: ) "(" (Set (Var "w")) "," (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set "(" (Set (Var "I")) ($#k1_fsm_2 :::"-TwoStatesMooreSM"::: ) "(" (Set (Var "i")) "," (Set (Var "f")) "," (Set (Var "o")) ")" ")" )) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Var "f")))))))) ; registrationlet "I", "O" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "i", "f" be ($#m1_hidden :::"set"::: ) ; let "o" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_tarski :::"{"::: ) (Set (Const "i")) "," (Set (Const "f")) ($#k2_tarski :::"}"::: ) ) "," (Set (Const "O")); cluster (Set "I" ($#k1_fsm_2 :::"-TwoStatesMooreSM"::: ) "(" "i" "," "f" "," "o" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_fsm_2 :::"calculating_type"::: ) ($#v6_fsm_2 :::"strict"::: ) ; end; registrationlet "I", "O" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "i", "f" be ($#m1_hidden :::"set"::: ) ; let "o" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_tarski :::"{"::: ) (Set (Const "i")) "," (Set (Const "f")) ($#k2_tarski :::"}"::: ) ) "," (Set (Const "O")); cluster (Set "I" ($#k1_fsm_2 :::"-TwoStatesMooreSM"::: ) "(" "i" "," "f" "," "o" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_fsm_2 :::"halting"::: ) ($#v6_fsm_2 :::"strict"::: ) ; end; theorem :: FSM_2:18 (Bool "for" (Set (Var "O")) "," (Set (Var "I")) "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 "I")) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_2 :::"Moore-SM_Final"::: ) "over" (Set (Var "I")) "," (Set (Var "O")) "st" (Bool (Bool (Set (Var "M")) "is" ($#v1_fsm_2 :::"calculating_type"::: ) ) & (Bool (Set (Var "s")) ($#r2_fsm_2 :::"leads_to_final_state_of"::: ) (Set (Var "M")))) "holds" (Bool "ex" (Set (Var "m")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool "(" "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "w")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::">="::: ) (Set (Var "m"))) & (Bool (Set (Set (Var "w")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "s")))) "holds" (Bool (Set (Set "(" ($#k2_fsm_1 :::"GEN"::: ) "(" (Set (Var "w")) "," (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M"))) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_fsm_2 :::"FinalS"::: ) "of" (Set (Var "M")))) ")" ) & (Bool "(" "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "j")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "w")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Set (Var "w")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool "not" (Bool (Set (Set "(" ($#k2_fsm_1 :::"GEN"::: ) "(" (Set (Var "w")) "," (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M"))) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_fsm_2 :::"FinalS"::: ) "of" (Set (Var "M")))))) ")" ) ")" ))))) ; begin definitionlet "I", "O" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_2 :::"Moore-SM_Final"::: ) "over" (Set (Const "I")) "," (Set (Const "O")); let "s" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")); let "t" be ($#m1_hidden :::"set"::: ) ; pred "t" :::"is_result_of"::: "s" "," "M" means :: FSM_2:def 8 (Bool "ex" (Set (Var "m")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" "I" "st" (Bool (Bool (Set (Set (Var "w")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) "s")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "w")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "implies" (Bool "(" (Bool "t" ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u4_fsm_1 :::"OFun"::: ) "of" "M") ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k2_fsm_1 :::"GEN"::: ) "(" (Set (Var "w")) "," (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" "M") ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "m")) ")" ))) & (Bool (Set (Set "(" ($#k2_fsm_1 :::"GEN"::: ) "(" (Set (Var "w")) "," (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" "M") ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_fsm_2 :::"FinalS"::: ) "of" "M")) ")" ) ")" & (Bool "(" "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "w")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool "not" (Bool (Set (Set "(" ($#k2_fsm_1 :::"GEN"::: ) "(" (Set (Var "w")) "," (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" "M") ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_fsm_2 :::"FinalS"::: ) "of" "M"))) ")" ) ")" ))); end; :: deftheorem defines :::"is_result_of"::: FSM_2:def 8 : (Bool "for" (Set (Var "I")) "," (Set (Var "O")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_2 :::"Moore-SM_Final"::: ) "over" (Set (Var "I")) "," (Set (Var "O")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "t")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r3_fsm_2 :::"is_result_of"::: ) (Set (Var "s")) "," (Set (Var "M"))) "iff" (Bool "ex" (Set (Var "m")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Set (Var "w")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "s")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "w")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "implies" (Bool "(" (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u4_fsm_1 :::"OFun"::: ) "of" (Set (Var "M"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k2_fsm_1 :::"GEN"::: ) "(" (Set (Var "w")) "," (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M"))) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "m")) ")" ))) & (Bool (Set (Set "(" ($#k2_fsm_1 :::"GEN"::: ) "(" (Set (Var "w")) "," (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M"))) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_fsm_2 :::"FinalS"::: ) "of" (Set (Var "M")))) ")" ) ")" & (Bool "(" "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "w")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool "not" (Bool (Set (Set "(" ($#k2_fsm_1 :::"GEN"::: ) "(" (Set (Var "w")) "," (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M"))) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_fsm_2 :::"FinalS"::: ) "of" (Set (Var "M"))))) ")" ) ")" ))) ")" ))))); theorem :: FSM_2:19 (Bool "for" (Set (Var "I")) "," (Set (Var "O")) "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 "I")) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_2 :::"Moore-SM_Final"::: ) "over" (Set (Var "I")) "," (Set (Var "O")) "st" (Bool (Bool (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_fsm_2 :::"FinalS"::: ) "of" (Set (Var "M"))))) "holds" (Bool (Set (Set "the" ($#u4_fsm_1 :::"OFun"::: ) "of" (Set (Var "M"))) ($#k3_funct_2 :::"."::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M")))) ($#r3_fsm_2 :::"is_result_of"::: ) (Set (Var "s")) "," (Set (Var "M")))))) ; theorem :: FSM_2:20 (Bool "for" (Set (Var "I")) "," (Set (Var "O")) "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 "I")) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_2 :::"Moore-SM_Final"::: ) "over" (Set (Var "I")) "," (Set (Var "O")) "st" (Bool (Bool (Set (Var "M")) "is" ($#v1_fsm_2 :::"calculating_type"::: ) ) & (Bool (Set (Var "s")) ($#r2_fsm_2 :::"leads_to_final_state_of"::: ) (Set (Var "M")))) "holds" (Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "O")) "st" (Bool (Set (Var "t")) ($#r3_fsm_2 :::"is_result_of"::: ) (Set (Var "s")) "," (Set (Var "M"))))))) ; theorem :: FSM_2:21 (Bool "for" (Set (Var "I")) "," (Set (Var "O")) "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 "I")) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_2 :::"Moore-SM_Final"::: ) "over" (Set (Var "I")) "," (Set (Var "O")) "st" (Bool (Bool (Set (Var "s")) ($#r2_fsm_2 :::"leads_to_final_state_of"::: ) (Set (Var "M")))) "holds" (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "O")) "st" (Bool (Bool (Set (Var "t1")) ($#r3_fsm_2 :::"is_result_of"::: ) (Set (Var "s")) "," (Set (Var "M"))) & (Bool (Set (Var "t2")) ($#r3_fsm_2 :::"is_result_of"::: ) (Set (Var "s")) "," (Set (Var "M")))) "holds" (Bool (Set (Var "t1")) ($#r1_hidden :::"="::: ) (Set (Var "t2"))))))) ; theorem :: FSM_2:22 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_2 :::"Moore-SM_Final"::: ) "over" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set (Var "M")) "is" ($#v1_fsm_2 :::"calculating_type"::: ) ) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "X")))) & (Bool (Set "the" ($#u1_fsm_2 :::"FinalS"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set "the" ($#u4_fsm_1 :::"OFun"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "M"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M"))) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v5_fsm_2 :::"halting"::: ) ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "f")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r3_fsm_2 :::"is_result_of"::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "M"))) ")" ) ")" )))) ; theorem :: FSM_2:23 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_2 :::"Moore-SM_Final"::: ) "over" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_ordinal1 :::"succ"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "st" (Bool (Bool (Set (Var "M")) "is" ($#v1_fsm_2 :::"calculating_type"::: ) ) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) & (Bool (Set "the" ($#u1_fsm_2 :::"FinalS"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set "the" ($#u4_fsm_1 :::"OFun"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "M"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M"))) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "y")))) "holds" (Bool (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "M"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M"))) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" )) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k2_square_1 :::"max"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r3_fsm_2 :::"is_result_of"::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "M"))))) ; theorem :: FSM_2:24 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_2 :::"Moore-SM_Final"::: ) "over" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_ordinal1 :::"succ"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "st" (Bool (Bool (Set (Var "M")) "is" ($#v1_fsm_2 :::"calculating_type"::: ) ) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) & (Bool (Set "the" ($#u1_fsm_2 :::"FinalS"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set "the" ($#u4_fsm_1 :::"OFun"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "y")))) "holds" (Bool (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "M"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M"))) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "M"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M"))) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" )) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k1_square_1 :::"min"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r3_fsm_2 :::"is_result_of"::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "M"))))) ; theorem :: FSM_2:25 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_2 :::"Moore-SM_Final"::: ) "over" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_ordinal1 :::"succ"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "st" (Bool (Bool (Set (Var "M")) "is" ($#v1_fsm_2 :::"calculating_type"::: ) ) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) & (Bool (Set "the" ($#u1_fsm_2 :::"FinalS"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set "the" ($#u4_fsm_1 :::"OFun"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "M"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M"))) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "y")))) ")" )) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "y"))) ($#r3_fsm_2 :::"is_result_of"::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "M"))))) ; theorem :: FSM_2:26 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_fsm_2 :::"Moore-SM_Final"::: ) "over" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_ordinal1 :::"succ"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "st" (Bool (Bool (Set (Var "M")) "is" ($#v1_fsm_2 :::"calculating_type"::: ) ) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) & (Bool (Set "the" ($#u1_fsm_2 :::"FinalS"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set "the" ($#u4_fsm_1 :::"OFun"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool "(" (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "y")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "M"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M"))) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "y")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "M"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M"))) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "y")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "M"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M"))) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) ")" )) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k2_square_1 :::"max"::: ) "(" (Set "(" ($#k2_absvalue :::"sgn"::: ) (Set (Var "x")) ")" ) "," (Set "(" ($#k2_absvalue :::"sgn"::: ) (Set (Var "y")) ")" ) ")" ) ($#r3_fsm_2 :::"is_result_of"::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "M"))))) ; registrationlet "I", "O" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_fsm_2 :::"calculating_type"::: ) ($#v5_fsm_2 :::"halting"::: ) for ($#l2_fsm_2 :::"Moore-SM_Final"::: ) "over" "I" "," "O"; end; registrationlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_fsm_2 :::"calculating_type"::: ) ($#v5_fsm_2 :::"halting"::: ) for ($#l1_fsm_2 :::"SM_Final"::: ) "over" "I"; end; definitionlet "I", "O" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_fsm_2 :::"calculating_type"::: ) ($#v5_fsm_2 :::"halting"::: ) ($#l2_fsm_2 :::"Moore-SM_Final"::: ) "over" (Set (Const "I")) "," (Set (Const "O")); let "s" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")); func :::"Result"::: "(" "s" "," "M" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" "O" means :: FSM_2:def 9 (Bool it ($#r3_fsm_2 :::"is_result_of"::: ) "s" "," "M"); end; :: deftheorem defines :::"Result"::: FSM_2:def 9 : (Bool "for" (Set (Var "I")) "," (Set (Var "O")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_fsm_2 :::"calculating_type"::: ) ($#v5_fsm_2 :::"halting"::: ) ($#l2_fsm_2 :::"Moore-SM_Final"::: ) "over" (Set (Var "I")) "," (Set (Var "O")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "O")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k2_fsm_2 :::"Result"::: ) "(" (Set (Var "s")) "," (Set (Var "M")) ")" )) "iff" (Bool (Set (Var "b5")) ($#r3_fsm_2 :::"is_result_of"::: ) (Set (Var "s")) "," (Set (Var "M"))) ")" ))))); theorem :: FSM_2:27 (Bool "for" (Set (Var "O")) "," (Set (Var "I")) "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 "I")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) ) "," (Set (Var "O")) "holds" (Bool (Set ($#k2_fsm_2 :::"Result"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "I")) ($#k1_fsm_2 :::"-TwoStatesMooreSM"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set (Var "f")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1)))))) ; theorem :: FSM_2:28 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_fsm_2 :::"calculating_type"::: ) ($#v5_fsm_2 :::"halting"::: ) ($#l2_fsm_2 :::"Moore-SM_Final"::: ) "over" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_ordinal1 :::"succ"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) & (Bool (Set "the" ($#u1_fsm_2 :::"FinalS"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set "the" ($#u4_fsm_1 :::"OFun"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "M"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M"))) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "y")))) "holds" (Bool (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "M"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M"))) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" )) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k2_fsm_2 :::"Result"::: ) "(" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "M")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_square_1 :::"max"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))) ; theorem :: FSM_2:29 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_fsm_2 :::"calculating_type"::: ) ($#v5_fsm_2 :::"halting"::: ) ($#l2_fsm_2 :::"Moore-SM_Final"::: ) "over" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_ordinal1 :::"succ"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) & (Bool (Set "the" ($#u1_fsm_2 :::"FinalS"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set "the" ($#u4_fsm_1 :::"OFun"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "y")))) "holds" (Bool (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "M"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M"))) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "M"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M"))) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" )) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k2_fsm_2 :::"Result"::: ) "(" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "M")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_square_1 :::"min"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))) ; theorem :: FSM_2:30 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_fsm_2 :::"calculating_type"::: ) ($#v5_fsm_2 :::"halting"::: ) ($#l2_fsm_2 :::"Moore-SM_Final"::: ) "over" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_ordinal1 :::"succ"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) & (Bool (Set "the" ($#u1_fsm_2 :::"FinalS"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set "the" ($#u4_fsm_1 :::"OFun"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "M"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M"))) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "y")))) ")" )) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k2_fsm_2 :::"Result"::: ) "(" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "M")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "y")))))) ; theorem :: FSM_2:31 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_fsm_2 :::"calculating_type"::: ) ($#v5_fsm_2 :::"halting"::: ) ($#l2_fsm_2 :::"Moore-SM_Final"::: ) "over" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_ordinal1 :::"succ"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) & (Bool (Set "the" ($#u1_fsm_2 :::"FinalS"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set "the" ($#u4_fsm_1 :::"OFun"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool "(" (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "y")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "M"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M"))) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "y")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "M"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M"))) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "y")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "the" ($#u1_fsm_1 :::"Tran"::: ) "of" (Set (Var "M"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u2_fsm_1 :::"InitS"::: ) "of" (Set (Var "M"))) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) ")" )) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k2_fsm_2 :::"Result"::: ) "(" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "M")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_square_1 :::"max"::: ) "(" (Set "(" ($#k2_absvalue :::"sgn"::: ) (Set (Var "x")) ")" ) "," (Set "(" ($#k2_absvalue :::"sgn"::: ) (Set (Var "y")) ")" ) ")" )))) ;