:: SCMFSA_2 semantic presentation begin definitionfunc :::"SCM+FSA"::: -> ($#v1_extpro_1 :::"strict"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Num 3) equals :: SCMFSA_2:def 1 (Set ($#g1_extpro_1 :::"AMI-Struct"::: ) "(#" (Set ($#k1_scmfsa_1 :::"SCM+FSA-Memory"::: ) ) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k1_scmfsa_1 :::"SCM+FSA-Memory"::: ) ) ")" ")" ) "," (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) ) "," (Set ($#k4_scmfsa_1 :::"SCM+FSA-OK"::: ) ) "," (Set ($#k5_scmfsa_1 :::"SCM*-VAL"::: ) ) "," (Set ($#k12_scmfsa_1 :::"SCM+FSA-Exec"::: ) ) "#)" ); end; :: deftheorem defines :::"SCM+FSA"::: SCMFSA_2:def 1 : (Bool (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_extpro_1 :::"AMI-Struct"::: ) "(#" (Set ($#k1_scmfsa_1 :::"SCM+FSA-Memory"::: ) ) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k1_scmfsa_1 :::"SCM+FSA-Memory"::: ) ) ")" ")" ) "," (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) ) "," (Set ($#k4_scmfsa_1 :::"SCM+FSA-OK"::: ) ) "," (Set ($#k5_scmfsa_1 :::"SCM*-VAL"::: ) ) "," (Set ($#k12_scmfsa_1 :::"SCM+FSA-Exec"::: ) ) "#)" )); registration cluster (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v1_extpro_1 :::"strict"::: ) ; end; registration cluster (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) -> ($#v1_extpro_1 :::"strict"::: ) ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ; end; theorem :: SCMFSA_2:1 (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) ; begin notationsynonym :::"Int-Locations"::: for :::"SCM+FSA-Data-Loc"::: ; end; definition:: original: :::"Int-Locations"::: redefine func :::"Int-Locations"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); canceled; func :::"FinSeq-Locations"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) equals :: SCMFSA_2:def 3 (Set ($#k3_scmfsa_1 :::"SCM+FSA-Data*-Loc"::: ) ); end; :: deftheorem SCMFSA_2:def 2 : canceled; :: deftheorem defines :::"FinSeq-Locations"::: SCMFSA_2:def 3 : (Bool (Set ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_scmfsa_1 :::"SCM+FSA-Data*-Loc"::: ) )); registration cluster ($#v1_ami_2 :::"Int-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )); end; definitionmode Int-Location is ($#v1_ami_2 :::"Int-like"::: ) ($#m1_subset_1 :::"Object":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); canceled; mode :::"FinSeq-Location"::: -> ($#m1_subset_1 :::"Object":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) means :: SCMFSA_2:def 5 (Bool it ($#r2_hidden :::"in"::: ) (Set ($#k3_scmfsa_1 :::"SCM+FSA-Data*-Loc"::: ) )); end; :: deftheorem SCMFSA_2:def 4 : canceled; :: deftheorem defines :::"FinSeq-Location"::: SCMFSA_2:def 5 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) "is" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) ) "iff" (Bool (Set (Var "b1")) ($#r2_hidden :::"in"::: ) (Set ($#k3_scmfsa_1 :::"SCM+FSA-Data*-Loc"::: ) )) ")" )); theorem :: SCMFSA_2:2 canceled; theorem :: SCMFSA_2:3 canceled; theorem :: SCMFSA_2:4 canceled; theorem :: SCMFSA_2:5 canceled; theorem :: SCMFSA_2:6 canceled; definitionlet "k" be ($#m1_hidden :::"Nat":::); func :::"intloc"::: "k" -> ($#m1_subset_1 :::"Int-Location":::) equals :: SCMFSA_2:def 6 (Set ($#k10_ami_3 :::"dl."::: ) "k"); func :::"fsloc"::: "k" -> ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) equals :: SCMFSA_2:def 7 (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" "k" ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )); end; :: deftheorem defines :::"intloc"::: SCMFSA_2:def 6 : (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k4_scmfsa_2 :::"intloc"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k10_ami_3 :::"dl."::: ) (Set (Var "k"))))); :: deftheorem defines :::"fsloc"::: SCMFSA_2:def 7 : (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k5_scmfsa_2 :::"fsloc"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))); theorem :: SCMFSA_2:7 (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k1")) ($#r1_hidden :::"<>"::: ) (Set (Var "k2")))) "holds" (Bool (Set ($#k5_scmfsa_2 :::"fsloc"::: ) (Set (Var "k1"))) ($#r1_hidden :::"<>"::: ) (Set ($#k5_scmfsa_2 :::"fsloc"::: ) (Set (Var "k2"))))) ; theorem :: SCMFSA_2:8 (Bool "for" (Set (Var "dl")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "dl")) ($#r1_hidden :::"="::: ) (Set ($#k4_scmfsa_2 :::"intloc"::: ) (Set (Var "i")))))) ; theorem :: SCMFSA_2:9 (Bool "for" (Set (Var "fl")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "fl")) ($#r1_hidden :::"="::: ) (Set ($#k5_scmfsa_2 :::"fsloc"::: ) (Set (Var "i")))))) ; registration cluster (Set ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) ) -> ($#v1_finset_1 :::"infinite"::: ) ; end; theorem :: SCMFSA_2:10 (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set (Var "I")) "is" ($#m1_subset_1 :::"Data-Location":::))) ; theorem :: SCMFSA_2:11 (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set ($#k4_memstr_0 :::"Values"::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set ($#k4_numbers :::"INT"::: ) ))) ; theorem :: SCMFSA_2:12 (Bool "for" (Set (Var "l")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set ($#k4_memstr_0 :::"Values"::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_numbers :::"INT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ))) ; begin theorem :: SCMFSA_2:13 canceled; theorem :: SCMFSA_2:14 canceled; theorem :: SCMFSA_2:15 (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "I"))) ($#r1_xxreal_0 :::"<="::: ) (Num 8))) "holds" (Bool (Set (Var "I")) "is" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ))) ; theorem :: SCMFSA_2:16 (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "I"))) ($#r1_xxreal_0 :::"<="::: ) (Num 12))) ; theorem :: SCMFSA_2:17 (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "holds" (Bool (Set (Var "I")) "is" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))) ; definitionlet "a", "b" be ($#m1_subset_1 :::"Int-Location":::); func "a" :::":="::: "b" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) means :: SCMFSA_2:def 8 (Bool "ex" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool "(" (Bool "a" ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool "b" ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k2_ami_3 :::":="::: ) (Set (Var "B")))) ")" )); func :::"AddTo"::: "(" "a" "," "b" ")" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) means :: SCMFSA_2:def 9 (Bool "ex" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool "(" (Bool "a" ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool "b" ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_ami_3 :::"AddTo"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) ")" )); func :::"SubFrom"::: "(" "a" "," "b" ")" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) means :: SCMFSA_2:def 10 (Bool "ex" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool "(" (Bool "a" ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool "b" ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k4_ami_3 :::"SubFrom"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) ")" )); func :::"MultBy"::: "(" "a" "," "b" ")" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) means :: SCMFSA_2:def 11 (Bool "ex" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool "(" (Bool "a" ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool "b" ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k5_ami_3 :::"MultBy"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) ")" )); func :::"Divide"::: "(" "a" "," "b" ")" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) means :: SCMFSA_2:def 12 (Bool "ex" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool "(" (Bool "a" ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool "b" ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_ami_3 :::"Divide"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) ")" )); end; :: deftheorem defines :::":="::: SCMFSA_2:def 8 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_scmfsa_2 :::":="::: ) (Set (Var "b")))) "iff" (Bool "ex" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k2_ami_3 :::":="::: ) (Set (Var "B")))) ")" )) ")" ))); :: deftheorem defines :::"AddTo"::: SCMFSA_2:def 9 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k7_scmfsa_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool "ex" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_ami_3 :::"AddTo"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) ")" )) ")" ))); :: deftheorem defines :::"SubFrom"::: SCMFSA_2:def 10 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool "ex" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_ami_3 :::"SubFrom"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) ")" )) ")" ))); :: deftheorem defines :::"MultBy"::: SCMFSA_2:def 11 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k9_scmfsa_2 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool "ex" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_ami_3 :::"MultBy"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) ")" )) ")" ))); :: deftheorem defines :::"Divide"::: SCMFSA_2:def 12 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k10_scmfsa_2 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool "ex" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_ami_3 :::"Divide"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) ")" )) ")" ))); definitionlet "la" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"goto"::: "la" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) equals :: SCMFSA_2:def 13 (Set ($#k7_ami_3 :::"SCM-goto"::: ) "la"); let "a" be ($#m1_subset_1 :::"Int-Location":::); func "a" :::"=0_goto"::: "la" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) means :: SCMFSA_2:def 14 (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool "(" (Bool "a" ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k8_ami_3 :::"=0_goto"::: ) "la")) ")" )); func "a" :::">0_goto"::: "la" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) means :: SCMFSA_2:def 15 (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool "(" (Bool "a" ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k9_ami_3 :::">0_goto"::: ) "la")) ")" )); end; :: deftheorem defines :::"goto"::: SCMFSA_2:def 13 : (Bool "for" (Set (Var "la")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k11_scmfsa_2 :::"goto"::: ) (Set (Var "la"))) ($#r1_hidden :::"="::: ) (Set ($#k7_ami_3 :::"SCM-goto"::: ) (Set (Var "la"))))); :: deftheorem defines :::"=0_goto"::: SCMFSA_2:def 14 : (Bool "for" (Set (Var "la")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k12_scmfsa_2 :::"=0_goto"::: ) (Set (Var "la")))) "iff" (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k8_ami_3 :::"=0_goto"::: ) (Set (Var "la")))) ")" )) ")" )))); :: deftheorem defines :::">0_goto"::: SCMFSA_2:def 15 : (Bool "for" (Set (Var "la")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k13_scmfsa_2 :::">0_goto"::: ) (Set (Var "la")))) "iff" (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k9_ami_3 :::">0_goto"::: ) (Set (Var "la")))) ")" )) ")" )))); definitionlet "c", "i" be ($#m1_subset_1 :::"Int-Location":::); let "a" be ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) ; func "c" :::":="::: "(" "a" "," "i" ")" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) equals :: SCMFSA_2:def 16 (Set ($#k3_xtuple_0 :::"["::: ) (Num 9) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k11_finseq_1 :::"<*"::: ) "c" "," "a" "," "i" ($#k11_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); func "(" "a" "," "i" ")" :::":="::: "c" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) equals :: SCMFSA_2:def 17 (Set ($#k3_xtuple_0 :::"["::: ) (Num 10) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k11_finseq_1 :::"<*"::: ) "c" "," "a" "," "i" ($#k11_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); end; :: deftheorem defines :::":="::: SCMFSA_2:def 16 : (Bool "for" (Set (Var "c")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "a")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Set (Var "c")) ($#k14_scmfsa_2 :::":="::: ) "(" (Set (Var "a")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 9) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "i")) ($#k11_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))); :: deftheorem defines :::":="::: SCMFSA_2:def 17 : (Bool "for" (Set (Var "c")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "a")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set "(" (Set (Var "a")) "," (Set (Var "i")) ")" ($#k15_scmfsa_2 :::":="::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 10) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "i")) ($#k11_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))); definitionlet "i" be ($#m1_subset_1 :::"Int-Location":::); let "a" be ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) ; func "i" :::":=len"::: "a" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) equals :: SCMFSA_2:def 18 (Set ($#k3_xtuple_0 :::"["::: ) (Num 11) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) "i" "," "a" ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); func "a" :::":=<0,...,0>"::: "i" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) equals :: SCMFSA_2:def 19 (Set ($#k3_xtuple_0 :::"["::: ) (Num 12) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) "i" "," "a" ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); end; :: deftheorem defines :::":=len"::: SCMFSA_2:def 18 : (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "a")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Set (Var "i")) ($#k16_scmfsa_2 :::":=len"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 11) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "i")) "," (Set (Var "a")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))); :: deftheorem defines :::":=<0,...,0>"::: SCMFSA_2:def 19 : (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "a")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k17_scmfsa_2 :::":=<0,...,0>"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 12) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "i")) "," (Set (Var "a")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))); theorem :: SCMFSA_2:18 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set "(" (Set (Var "a")) ($#k6_scmfsa_2 :::":="::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: SCMFSA_2:19 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set "(" ($#k7_scmfsa_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Num 2))) ; theorem :: SCMFSA_2:20 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Num 3))) ; theorem :: SCMFSA_2:21 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set "(" ($#k9_scmfsa_2 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Num 4))) ; theorem :: SCMFSA_2:22 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set "(" ($#k10_scmfsa_2 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Num 5))) ; theorem :: SCMFSA_2:23 (Bool "for" (Set (Var "lb")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set "(" ($#k11_scmfsa_2 :::"goto"::: ) (Set (Var "lb")) ")" )) ($#r1_hidden :::"="::: ) (Num 6))) ; theorem :: SCMFSA_2:24 (Bool "for" (Set (Var "lb")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set "(" (Set (Var "a")) ($#k12_scmfsa_2 :::"=0_goto"::: ) (Set (Var "lb")) ")" )) ($#r1_hidden :::"="::: ) (Num 7)))) ; theorem :: SCMFSA_2:25 (Bool "for" (Set (Var "lb")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set "(" (Set (Var "a")) ($#k13_scmfsa_2 :::">0_goto"::: ) (Set (Var "lb")) ")" )) ($#r1_hidden :::"="::: ) (Num 8)))) ; theorem :: SCMFSA_2:26 (Bool "for" (Set (Var "fa")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "c")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set "(" (Set (Var "c")) ($#k14_scmfsa_2 :::":="::: ) "(" (Set (Var "fa")) "," (Set (Var "a")) ")" ")" )) ($#r1_hidden :::"="::: ) (Num 9)))) ; theorem :: SCMFSA_2:27 (Bool "for" (Set (Var "fa")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set "(" "(" (Set (Var "fa")) "," (Set (Var "a")) ")" ($#k15_scmfsa_2 :::":="::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Num 10)))) ; theorem :: SCMFSA_2:28 (Bool "for" (Set (Var "fa")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set "(" (Set (Var "a")) ($#k16_scmfsa_2 :::":=len"::: ) (Set (Var "fa")) ")" )) ($#r1_hidden :::"="::: ) (Num 11)))) ; theorem :: SCMFSA_2:29 (Bool "for" (Set (Var "fa")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set "(" (Set (Var "fa")) ($#k17_scmfsa_2 :::":=<0,...,0>"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Num 12)))) ; theorem :: SCMFSA_2:30 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool "ex" (Set (Var "da")) "," (Set (Var "db")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set (Set (Var "da")) ($#k6_scmfsa_2 :::":="::: ) (Set (Var "db")))))) ; theorem :: SCMFSA_2:31 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 2))) "holds" (Bool "ex" (Set (Var "da")) "," (Set (Var "db")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set ($#k7_scmfsa_2 :::"AddTo"::: ) "(" (Set (Var "da")) "," (Set (Var "db")) ")" )))) ; theorem :: SCMFSA_2:32 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 3))) "holds" (Bool "ex" (Set (Var "da")) "," (Set (Var "db")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "da")) "," (Set (Var "db")) ")" )))) ; theorem :: SCMFSA_2:33 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 4))) "holds" (Bool "ex" (Set (Var "da")) "," (Set (Var "db")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set ($#k9_scmfsa_2 :::"MultBy"::: ) "(" (Set (Var "da")) "," (Set (Var "db")) ")" )))) ; theorem :: SCMFSA_2:34 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 5))) "holds" (Bool "ex" (Set (Var "da")) "," (Set (Var "db")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set ($#k10_scmfsa_2 :::"Divide"::: ) "(" (Set (Var "da")) "," (Set (Var "db")) ")" )))) ; theorem :: SCMFSA_2:35 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 6))) "holds" (Bool "ex" (Set (Var "lb")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_2 :::"goto"::: ) (Set (Var "lb")))))) ; theorem :: SCMFSA_2:36 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 7))) "holds" (Bool "ex" (Set (Var "lb")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "da")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set (Set (Var "da")) ($#k12_scmfsa_2 :::"=0_goto"::: ) (Set (Var "lb"))))))) ; theorem :: SCMFSA_2:37 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 8))) "holds" (Bool "ex" (Set (Var "lb")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "da")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set (Set (Var "da")) ($#k13_scmfsa_2 :::">0_goto"::: ) (Set (Var "lb"))))))) ; theorem :: SCMFSA_2:38 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 9))) "holds" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::)(Bool "ex" (Set (Var "fa")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k14_scmfsa_2 :::":="::: ) "(" (Set (Var "fa")) "," (Set (Var "a")) ")" ))))) ; theorem :: SCMFSA_2:39 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 10))) "holds" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::)(Bool "ex" (Set (Var "fa")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "fa")) "," (Set (Var "a")) ")" ($#k15_scmfsa_2 :::":="::: ) (Set (Var "b"))))))) ; theorem :: SCMFSA_2:40 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 11))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::)(Bool "ex" (Set (Var "fa")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k16_scmfsa_2 :::":=len"::: ) (Set (Var "fa"))))))) ; theorem :: SCMFSA_2:41 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 12))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::)(Bool "ex" (Set (Var "fa")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set (Set (Var "fa")) ($#k17_scmfsa_2 :::":=<0,...,0>"::: ) (Set (Var "a"))))))) ; begin theorem :: SCMFSA_2:42 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "s")))))) ; theorem :: SCMFSA_2:43 (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "s")))))) ; theorem :: SCMFSA_2:44 (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "holds" (Bool (Bool "not" (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "S"))))))) ; theorem :: SCMFSA_2:45 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "s"))))) ; theorem :: SCMFSA_2:46 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "s"))))) ; theorem :: SCMFSA_2:47 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_scmfsa_2 :::"Int-Locations"::: ) ))) ; theorem :: SCMFSA_2:48 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) ))) ; theorem :: SCMFSA_2:49 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "holds" (Bool (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set ($#k1_ami_2 :::"SCM-Memory"::: ) )) "is" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )))) ; theorem :: SCMFSA_2:50 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s9")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "holds" (Bool (Set (Set (Var "s")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "s9"))) "is" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )))) ; theorem :: SCMFSA_2:51 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "ii")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "ss")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "ii"))) & (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set (Set (Var "ss")) ($#k5_relat_1 :::"|"::: ) (Set ($#k1_ami_2 :::"SCM-Memory"::: ) )))) "holds" (Bool (Set ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "ii")) "," (Set (Var "ss")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "ss")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "i")) "," (Set (Var "s")) ")" ")" ))))))) ; registrationlet "s" be ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "d" be ($#m1_subset_1 :::"Int-Location":::); cluster (Set "s" ($#k1_funct_1 :::"."::: ) "d") -> ($#v1_int_1 :::"integer"::: ) ; end; definitionlet "s" be ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "d" be ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) ; :: original: :::"."::: redefine func "s" :::"."::: "d" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ); end; theorem :: SCMFSA_2:52 (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set ($#k1_ami_2 :::"SCM-Memory"::: ) )))) "holds" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "S")))))) ; theorem :: SCMFSA_2:53 (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "S"))))) "holds" (Bool (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" ))))) ; theorem :: SCMFSA_2:54 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Data-Location":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "S")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "holds" (Bool (Set (Set (Var "S")) ($#k1_funct_1 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))))))) ; theorem :: SCMFSA_2:55 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Data-Location":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set ($#k1_ami_2 :::"SCM-Memory"::: ) ))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "holds" (Bool (Set (Set (Var "S")) ($#k1_funct_1 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))))))) ; registration cluster (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) -> ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#v1_extpro_1 :::"strict"::: ) ; end; theorem :: SCMFSA_2:56 (Bool "for" (Set (Var "dl")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set (Var "dl")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"IC"::: ) ))) ; theorem :: SCMFSA_2:57 (Bool "for" (Set (Var "dl")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Var "dl")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"IC"::: ) ))) ; theorem :: SCMFSA_2:58 (Bool "for" (Set (Var "il")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "dl")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Var "il")) ($#r1_hidden :::"<>"::: ) (Set (Var "dl"))))) ; theorem :: SCMFSA_2:59 (Bool "for" (Set (Var "il")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "dl")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set (Var "il")) ($#r1_hidden :::"<>"::: ) (Set (Var "dl"))))) ; theorem :: SCMFSA_2:60 (Bool "for" (Set (Var "il")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "dl")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Var "il")) ($#r1_hidden :::"<>"::: ) (Set (Var "dl"))))) ; theorem :: SCMFSA_2:61 (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s2")))) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s2")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Set (Var "s1")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "s2")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")))) ")" )) "holds" (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Var "s2")))) ; theorem :: SCMFSA_2:62 (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set ($#k1_ami_2 :::"SCM-Memory"::: ) )))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "S")))))) ; begin theorem :: SCMFSA_2:63 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k6_scmfsa_2 :::":="::: ) (Set (Var "b")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k6_scmfsa_2 :::":="::: ) (Set (Var "b")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k6_scmfsa_2 :::":="::: ) (Set (Var "b")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k6_scmfsa_2 :::":="::: ) (Set (Var "b")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "s")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")))) ")" ) ")" ))) ; theorem :: SCMFSA_2:64 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k7_scmfsa_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k7_scmfsa_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k7_scmfsa_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k7_scmfsa_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "s")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")))) ")" ) ")" ))) ; theorem :: SCMFSA_2:65 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "s")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")))) ")" ) ")" ))) ; theorem :: SCMFSA_2:66 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k9_scmfsa_2 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k9_scmfsa_2 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k9_scmfsa_2 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k9_scmfsa_2 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "s")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")))) ")" ) ")" ))) ; theorem :: SCMFSA_2:67 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k10_scmfsa_2 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) & "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "implies" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k10_scmfsa_2 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k5_int_1 :::"div"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ))) ")" & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k10_scmfsa_2 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k10_scmfsa_2 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k10_scmfsa_2 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "s")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")))) ")" ) ")" ))) ; theorem :: SCMFSA_2:68 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k10_scmfsa_2 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "a")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k10_scmfsa_2 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "a")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k10_scmfsa_2 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "a")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k10_scmfsa_2 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "a")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "s")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")))) ")" ) ")" ))) ; theorem :: SCMFSA_2:69 (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k11_scmfsa_2 :::"goto"::: ) (Set (Var "l")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "l"))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k11_scmfsa_2 :::"goto"::: ) (Set (Var "l")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k11_scmfsa_2 :::"goto"::: ) (Set (Var "l")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "s")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")))) ")" ) ")" ))) ; theorem :: SCMFSA_2:70 (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k12_scmfsa_2 :::"=0_goto"::: ) (Set (Var "l")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "l"))) ")" & "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k12_scmfsa_2 :::"=0_goto"::: ) (Set (Var "l")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) ")" & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k12_scmfsa_2 :::"=0_goto"::: ) (Set (Var "l")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k12_scmfsa_2 :::"=0_goto"::: ) (Set (Var "l")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "s")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")))) ")" ) ")" )))) ; theorem :: SCMFSA_2:71 (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k13_scmfsa_2 :::">0_goto"::: ) (Set (Var "l")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "l"))) ")" & "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k13_scmfsa_2 :::">0_goto"::: ) (Set (Var "l")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) ")" & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k13_scmfsa_2 :::">0_goto"::: ) (Set (Var "l")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k13_scmfsa_2 :::">0_goto"::: ) (Set (Var "l")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "s")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")))) ")" ) ")" )))) ; theorem :: SCMFSA_2:72 (Bool "for" (Set (Var "g")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "c")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "c")) ($#k14_scmfsa_2 :::":="::: ) "(" (Set (Var "g")) "," (Set (Var "a")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) & (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set ($#k1_int_2 :::"abs"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ))) & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "c")) ($#k14_scmfsa_2 :::":="::: ) "(" (Set (Var "g")) "," (Set (Var "a")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "g")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")))) ")" )) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "c")))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "c")) ($#k14_scmfsa_2 :::":="::: ) "(" (Set (Var "g")) "," (Set (Var "a")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "c")) ($#k14_scmfsa_2 :::":="::: ) "(" (Set (Var "g")) "," (Set (Var "a")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "s")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")))) ")" ) ")" )))) ; theorem :: SCMFSA_2:73 (Bool "for" (Set (Var "g")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" "(" (Set (Var "g")) "," (Set (Var "a")) ")" ($#k15_scmfsa_2 :::":="::: ) (Set (Var "c")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) & (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set ($#k1_int_2 :::"abs"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ))) & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" "(" (Set (Var "g")) "," (Set (Var "a")) ")" ($#k15_scmfsa_2 :::":="::: ) (Set (Var "c")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "g")) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "k")) "," (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ")" )) ")" )) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" "(" (Set (Var "g")) "," (Set (Var "a")) ")" ($#k15_scmfsa_2 :::":="::: ) (Set (Var "c")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"<>"::: ) (Set (Var "g")))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" "(" (Set (Var "g")) "," (Set (Var "a")) ")" ($#k15_scmfsa_2 :::":="::: ) (Set (Var "c")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "s")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")))) ")" ) ")" )))) ; theorem :: SCMFSA_2:74 (Bool "for" (Set (Var "g")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "c")) ($#k16_scmfsa_2 :::":=len"::: ) (Set (Var "g")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "c")) ($#k16_scmfsa_2 :::":=len"::: ) (Set (Var "g")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "s")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "g")) ")" ))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "c")))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "c")) ($#k16_scmfsa_2 :::":=len"::: ) (Set (Var "g")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "c")) ($#k16_scmfsa_2 :::":=len"::: ) (Set (Var "g")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "s")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")))) ")" ) ")" )))) ; theorem :: SCMFSA_2:75 (Bool "for" (Set (Var "g")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "g")) ($#k17_scmfsa_2 :::":=<0,...,0>"::: ) (Set (Var "c")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) & (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set ($#k1_int_2 :::"abs"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ))) & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "g")) ($#k17_scmfsa_2 :::":=<0,...,0>"::: ) (Set (Var "c")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k5_finseq_2 :::"|->"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ")" )) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "g")) ($#k17_scmfsa_2 :::":=<0,...,0>"::: ) (Set (Var "c")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"<>"::: ) (Set (Var "g")))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "g")) ($#k17_scmfsa_2 :::":=<0,...,0>"::: ) (Set (Var "c")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "s")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")))) ")" ) ")" )))) ; begin theorem :: SCMFSA_2:76 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SCM+FSA-State":::) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Var "s")))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k10_scmfsa_1 :::"IC"::: ) (Set (Var "S")))))) ; theorem :: SCMFSA_2:77 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "I"))) & (Bool (Set (Var "i")) "is" ($#v2_extpro_1 :::"halting"::: ) )) "holds" (Bool (Set (Var "I")) "is" ($#v2_extpro_1 :::"halting"::: ) ))) ; theorem :: SCMFSA_2:78 (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool "ex" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "I")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))))) "holds" (Bool "not" (Bool (Set (Var "I")) "is" ($#v2_extpro_1 :::"halting"::: ) ))) ; registrationlet "a", "b" be ($#m1_subset_1 :::"Int-Location":::); cluster (Set "a" ($#k6_scmfsa_2 :::":="::: ) "b") -> ($#~v2_extpro_1 "non" ($#v2_extpro_1 :::"halting"::: ) ) ; cluster (Set ($#k7_scmfsa_2 :::"AddTo"::: ) "(" "a" "," "b" ")" ) -> ($#~v2_extpro_1 "non" ($#v2_extpro_1 :::"halting"::: ) ) ; cluster (Set ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" "a" "," "b" ")" ) -> ($#~v2_extpro_1 "non" ($#v2_extpro_1 :::"halting"::: ) ) ; cluster (Set ($#k9_scmfsa_2 :::"MultBy"::: ) "(" "a" "," "b" ")" ) -> ($#~v2_extpro_1 "non" ($#v2_extpro_1 :::"halting"::: ) ) ; cluster (Set ($#k10_scmfsa_2 :::"Divide"::: ) "(" "a" "," "b" ")" ) -> ($#~v2_extpro_1 "non" ($#v2_extpro_1 :::"halting"::: ) ) ; end; theorem :: SCMFSA_2:79 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Bool "not" (Set (Set (Var "a")) ($#k6_scmfsa_2 :::":="::: ) (Set (Var "b"))) "is" ($#v2_extpro_1 :::"halting"::: ) ))) ; theorem :: SCMFSA_2:80 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Bool "not" (Set ($#k7_scmfsa_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#v2_extpro_1 :::"halting"::: ) ))) ; theorem :: SCMFSA_2:81 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Bool "not" (Set ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#v2_extpro_1 :::"halting"::: ) ))) ; theorem :: SCMFSA_2:82 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Bool "not" (Set ($#k9_scmfsa_2 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#v2_extpro_1 :::"halting"::: ) ))) ; theorem :: SCMFSA_2:83 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Bool "not" (Set ($#k10_scmfsa_2 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#v2_extpro_1 :::"halting"::: ) ))) ; registrationlet "la" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k11_scmfsa_2 :::"goto"::: ) "la") -> ($#~v2_extpro_1 "non" ($#v2_extpro_1 :::"halting"::: ) ) ; end; theorem :: SCMFSA_2:84 (Bool "for" (Set (Var "la")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Bool "not" (Set ($#k11_scmfsa_2 :::"goto"::: ) (Set (Var "la"))) "is" ($#v2_extpro_1 :::"halting"::: ) ))) ; registrationlet "a" be ($#m1_subset_1 :::"Int-Location":::); let "la" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set "a" ($#k12_scmfsa_2 :::"=0_goto"::: ) "la") -> ($#~v2_extpro_1 "non" ($#v2_extpro_1 :::"halting"::: ) ) ; cluster (Set "a" ($#k13_scmfsa_2 :::">0_goto"::: ) "la") -> ($#~v2_extpro_1 "non" ($#v2_extpro_1 :::"halting"::: ) ) ; end; theorem :: SCMFSA_2:85 (Bool "for" (Set (Var "la")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Bool "not" (Set (Set (Var "a")) ($#k12_scmfsa_2 :::"=0_goto"::: ) (Set (Var "la"))) "is" ($#v2_extpro_1 :::"halting"::: ) )))) ; theorem :: SCMFSA_2:86 (Bool "for" (Set (Var "la")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Bool "not" (Set (Set (Var "a")) ($#k13_scmfsa_2 :::">0_goto"::: ) (Set (Var "la"))) "is" ($#v2_extpro_1 :::"halting"::: ) )))) ; registrationlet "c" be ($#m1_subset_1 :::"Int-Location":::); let "f" be ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) ; let "a" be ($#m1_subset_1 :::"Int-Location":::); cluster (Set "c" ($#k14_scmfsa_2 :::":="::: ) "(" "f" "," "a" ")" ) -> ($#~v2_extpro_1 "non" ($#v2_extpro_1 :::"halting"::: ) ) ; cluster (Set "(" "f" "," "a" ")" ($#k15_scmfsa_2 :::":="::: ) "c") -> ($#~v2_extpro_1 "non" ($#v2_extpro_1 :::"halting"::: ) ) ; end; theorem :: SCMFSA_2:87 (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "c")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Bool "not" (Set (Set (Var "c")) ($#k14_scmfsa_2 :::":="::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ) "is" ($#v2_extpro_1 :::"halting"::: ) )))) ; theorem :: SCMFSA_2:88 (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Bool "not" (Set "(" (Set (Var "f")) "," (Set (Var "a")) ")" ($#k15_scmfsa_2 :::":="::: ) (Set (Var "c"))) "is" ($#v2_extpro_1 :::"halting"::: ) )))) ; registrationlet "c" be ($#m1_subset_1 :::"Int-Location":::); let "f" be ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) ; cluster (Set "c" ($#k16_scmfsa_2 :::":=len"::: ) "f") -> ($#~v2_extpro_1 "non" ($#v2_extpro_1 :::"halting"::: ) ) ; cluster (Set "f" ($#k17_scmfsa_2 :::":=<0,...,0>"::: ) "c") -> ($#~v2_extpro_1 "non" ($#v2_extpro_1 :::"halting"::: ) ) ; end; theorem :: SCMFSA_2:89 (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Bool "not" (Set (Set (Var "c")) ($#k16_scmfsa_2 :::":=len"::: ) (Set (Var "f"))) "is" ($#v2_extpro_1 :::"halting"::: ) )))) ; theorem :: SCMFSA_2:90 (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Bool "not" (Set (Set (Var "f")) ($#k17_scmfsa_2 :::":=<0,...,0>"::: ) (Set (Var "c"))) "is" ($#v2_extpro_1 :::"halting"::: ) )))) ; theorem :: SCMFSA_2:91 (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool (Set (Var "I")) "is" ($#v2_extpro_1 :::"halting"::: ) )) ; theorem :: SCMFSA_2:92 (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) ; theorem :: SCMFSA_2:93 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )) "iff" (Bool "(" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )) "or" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_scmfsa_2 :::":="::: ) (Set (Var "b"))))) "or" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k7_scmfsa_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) "or" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) "or" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k9_scmfsa_2 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) "or" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k10_scmfsa_2 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) "or" (Bool "ex" (Set (Var "la")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_2 :::"goto"::: ) (Set (Var "la"))))) "or" (Bool "ex" (Set (Var "lb")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "da")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set (Set (Var "da")) ($#k12_scmfsa_2 :::"=0_goto"::: ) (Set (Var "lb")))))) "or" (Bool "ex" (Set (Var "lb")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "da")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set (Set (Var "da")) ($#k13_scmfsa_2 :::">0_goto"::: ) (Set (Var "lb")))))) "or" (Bool "ex" (Set (Var "b")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::)(Bool "ex" (Set (Var "fa")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k14_scmfsa_2 :::":="::: ) "(" (Set (Var "fa")) "," (Set (Var "b")) ")" )))) "or" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::)(Bool "ex" (Set (Var "fa")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "fa")) "," (Set (Var "a")) ")" ($#k15_scmfsa_2 :::":="::: ) (Set (Var "b")))))) "or" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::)(Bool "ex" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k16_scmfsa_2 :::":=len"::: ) (Set (Var "f")))))) "or" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::)(Bool "ex" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k17_scmfsa_2 :::":=<0,...,0>"::: ) (Set (Var "a")))))) ")" ) ")" )) ; registration cluster (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) -> ($#v1_extpro_1 :::"strict"::: ) ($#v3_extpro_1 :::"halting"::: ) ; end; theorem :: SCMFSA_2:94 (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) "is" ($#v2_extpro_1 :::"halting"::: ) )) "holds" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )))) ; theorem :: SCMFSA_2:95 (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )))) ; theorem :: SCMFSA_2:96 (Bool (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))) ; theorem :: SCMFSA_2:97 canceled; theorem :: SCMFSA_2:98 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "I"))) & (Bool (Bool "not" (Set (Var "i")) "is" ($#v2_extpro_1 :::"halting"::: ) ))) "holds" (Bool "not" (Bool (Set (Var "I")) "is" ($#v2_extpro_1 :::"halting"::: ) )))) ; theorem :: SCMFSA_2:99 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k5_scmfsa_2 :::"fsloc"::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Set ($#k4_scmfsa_2 :::"intloc"::: ) (Set (Var "j"))))) ; theorem :: SCMFSA_2:100 (Bool (Set ($#k8_struct_0 :::"Data-Locations"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) ))) ; theorem :: SCMFSA_2:101 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j")))) "holds" (Bool (Set ($#k4_scmfsa_2 :::"intloc"::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Set ($#k4_scmfsa_2 :::"intloc"::: ) (Set (Var "j"))))) ; theorem :: SCMFSA_2:102 (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set (Var "l")) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ")" )))))) ; theorem :: SCMFSA_2:103 (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Bool "not" (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set (Var "l")) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ")" )))))) ; theorem :: SCMFSA_2:104 (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s2")))) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s2")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Set (Var "s1")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "s2")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")))) ")" )) "holds" (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Var "s2")))) ; registrationlet "f" be ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) ; let "w" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ); cluster (Set "f" ($#k16_funcop_1 :::".-->"::: ) "w") -> ($#v4_memstr_0 :::"data-only"::: ) for ($#m1_hidden :::"PartState":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); end; registrationlet "x" be ($#m1_subset_1 :::"Int-Location":::); let "i" be ($#m1_hidden :::"Integer":::); cluster (Set "x" ($#k16_funcop_1 :::".-->"::: ) "i") -> ($#v4_memstr_0 :::"data-only"::: ) for ($#m1_hidden :::"PartState":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); end; registrationlet "a", "b" be ($#m1_subset_1 :::"Int-Location":::); cluster (Set "a" ($#k6_scmfsa_2 :::":="::: ) "b") -> ($#v6_compos_0 :::"No-StopCode"::: ) ; end; registrationlet "a", "b" be ($#m1_subset_1 :::"Int-Location":::); cluster (Set ($#k7_scmfsa_2 :::"AddTo"::: ) "(" "a" "," "b" ")" ) -> ($#v6_compos_0 :::"No-StopCode"::: ) ; end; registrationlet "a", "b" be ($#m1_subset_1 :::"Int-Location":::); cluster (Set ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" "a" "," "b" ")" ) -> ($#v6_compos_0 :::"No-StopCode"::: ) ; end; registrationlet "a", "b" be ($#m1_subset_1 :::"Int-Location":::); cluster (Set ($#k9_scmfsa_2 :::"MultBy"::: ) "(" "a" "," "b" ")" ) -> ($#v6_compos_0 :::"No-StopCode"::: ) ; end; registrationlet "a", "b" be ($#m1_subset_1 :::"Int-Location":::); cluster (Set ($#k10_scmfsa_2 :::"Divide"::: ) "(" "a" "," "b" ")" ) -> ($#v6_compos_0 :::"No-StopCode"::: ) ; end; registrationlet "lb" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k11_scmfsa_2 :::"goto"::: ) "lb") -> ($#v6_compos_0 :::"No-StopCode"::: ) ; end; registrationlet "lb" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "a" be ($#m1_subset_1 :::"Int-Location":::); cluster (Set "a" ($#k12_scmfsa_2 :::"=0_goto"::: ) "lb") -> ($#v6_compos_0 :::"No-StopCode"::: ) ; end; registrationlet "lb" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "a" be ($#m1_subset_1 :::"Int-Location":::); cluster (Set "a" ($#k13_scmfsa_2 :::">0_goto"::: ) "lb") -> ($#v6_compos_0 :::"No-StopCode"::: ) ; end; registrationlet "fa" be ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) ; let "a", "c" be ($#m1_subset_1 :::"Int-Location":::); cluster (Set "c" ($#k14_scmfsa_2 :::":="::: ) "(" "fa" "," "a" ")" ) -> ($#v6_compos_0 :::"No-StopCode"::: ) ; end; registrationlet "fa" be ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) ; let "a", "c" be ($#m1_subset_1 :::"Int-Location":::); cluster (Set "(" "fa" "," "a" ")" ($#k15_scmfsa_2 :::":="::: ) "c") -> ($#v6_compos_0 :::"No-StopCode"::: ) ; end; registrationlet "fa" be ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) ; let "a" be ($#m1_subset_1 :::"Int-Location":::); cluster (Set "a" ($#k16_scmfsa_2 :::":=len"::: ) "fa") -> ($#v6_compos_0 :::"No-StopCode"::: ) ; end; registrationlet "fa" be ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) ; let "a" be ($#m1_subset_1 :::"Int-Location":::); cluster (Set "fa" ($#k17_scmfsa_2 :::":=<0,...,0>"::: ) "a") -> ($#v6_compos_0 :::"No-StopCode"::: ) ; end;