:: SCMFSA10  semantic presentation begin  







































definitionlet "la", "lb" be   ($#m1_subset_1 :::"Int-Location":::); let "a", "b" be   ($#m1_hidden :::"Integer":::); :: original: :::"-->"::: redefine func  "(" "la" "," "lb" ")"  :::"-->":::  "(" "a" "," "b" ")"  ->   ($#m1_hidden :::"PartState":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); end; 
theorem :: SCMFSA10:1 (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "holds"  (Bool  "("   "not" (Bool (Set (Var "o"))  ($#r2_hidden :::"in"::: )  (Set   ($#k8_struct_0 :::"Data-Locations"::: )  )) "or" (Bool (Set (Var "o")) "is"   ($#m1_subset_1 :::"Int-Location":::)) "or" (Bool (Set (Var "o")) "is"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )  )  ")" )) ; 
 
theorem :: SCMFSA10:2 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Int-Location":::) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_scmfsa_2 :::":="::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set  ($#k3_xtuple_0 :::"["::: ) (Num 1) "," (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set  ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) ; 
 
theorem :: SCMFSA10:3 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Int-Location":::) "holds"  (Bool (Set   ($#k7_scmfsa_2 :::"AddTo"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k3_xtuple_0 :::"["::: ) (Num 2) "," (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set  ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) ; 
 
theorem :: SCMFSA10:4 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Int-Location":::) "holds"  (Bool (Set   ($#k8_scmfsa_2 :::"SubFrom"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k3_xtuple_0 :::"["::: ) (Num 3) "," (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set  ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) ; 
 
theorem :: SCMFSA10:5 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Int-Location":::) "holds"  (Bool (Set   ($#k9_scmfsa_2 :::"MultBy"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k3_xtuple_0 :::"["::: ) (Num 4) "," (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set  ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) ; 
 
theorem :: SCMFSA10:6 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Int-Location":::) "holds"  (Bool (Set   ($#k10_scmfsa_2 :::"Divide"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k3_xtuple_0 :::"["::: ) (Num 5) "," (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set  ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) ; 
 
theorem :: SCMFSA10:7 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "il")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "a"))  ($#k12_scmfsa_2 :::"=0_goto"::: )  (Set (Var "il")))  ($#r1_hidden :::"="::: )  (Set  ($#k3_xtuple_0 :::"["::: ) (Num 7) "," (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "il")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))) ; 
 
theorem :: SCMFSA10:8 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "il")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "a"))  ($#k13_scmfsa_2 :::">0_goto"::: )  (Set (Var "il")))  ($#r1_hidden :::"="::: )  (Set  ($#k3_xtuple_0 :::"["::: ) (Num 8) "," (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "il")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))) ; 
 














theorem :: SCMFSA10:9 (Bool (Set   ($#k5_xtuple_0 :::"JumpPart"::: )  (Set  "("  ($#k2_compos_1 :::"halt"::: )  (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) ; 
 


















theorem :: SCMFSA10:10 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Int-Location":::) "holds"  (Bool (Set   ($#k5_xtuple_0 :::"JumpPart"::: )  (Set  "(" (Set (Var "a"))  ($#k6_scmfsa_2 :::":="::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: SCMFSA10:11 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Int-Location":::) "holds"  (Bool (Set   ($#k5_xtuple_0 :::"JumpPart"::: )  (Set  "("  ($#k7_scmfsa_2 :::"AddTo"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: SCMFSA10:12 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Int-Location":::) "holds"  (Bool (Set   ($#k5_xtuple_0 :::"JumpPart"::: )  (Set  "("  ($#k8_scmfsa_2 :::"SubFrom"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: SCMFSA10:13 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Int-Location":::) "holds"  (Bool (Set   ($#k5_xtuple_0 :::"JumpPart"::: )  (Set  "("  ($#k9_scmfsa_2 :::"MultBy"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: SCMFSA10:14 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Int-Location":::) "holds"  (Bool (Set   ($#k5_xtuple_0 :::"JumpPart"::: )  (Set  "("  ($#k10_scmfsa_2 :::"Divide"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: SCMFSA10:15 (Bool  "for" (Set (Var "i1")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Int-Location":::) "holds"  (Bool (Set   ($#k5_xtuple_0 :::"JumpPart"::: )  (Set  "(" (Set (Var "a"))  ($#k12_scmfsa_2 :::"=0_goto"::: )  (Set (Var "i1")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "i1")) ($#k12_finseq_1 :::"*>"::: ) )))) ; 
 
theorem :: SCMFSA10:16 (Bool  "for" (Set (Var "i1")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Int-Location":::) "holds"  (Bool (Set   ($#k5_xtuple_0 :::"JumpPart"::: )  (Set  "(" (Set (Var "a"))  ($#k13_scmfsa_2 :::">0_goto"::: )  (Set (Var "i1")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "i1")) ($#k12_finseq_1 :::"*>"::: ) )))) ; 
 
theorem :: SCMFSA10:17 (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))  "st" (Bool (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k3_compos_0 :::"JumpParts"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: SCMFSA10:18 (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))  "st" (Bool (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set   ($#k3_compos_0 :::"JumpParts"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: SCMFSA10:19 (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))  "st" (Bool (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Num 2))) "holds"  (Bool (Set   ($#k3_compos_0 :::"JumpParts"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: SCMFSA10:20 (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))  "st" (Bool (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Num 3))) "holds"  (Bool (Set   ($#k3_compos_0 :::"JumpParts"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: SCMFSA10:21 (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))  "st" (Bool (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Num 4))) "holds"  (Bool (Set   ($#k3_compos_0 :::"JumpParts"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: SCMFSA10:22 (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))  "st" (Bool (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Num 5))) "holds"  (Bool (Set   ($#k3_compos_0 :::"JumpParts"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: SCMFSA10:23 (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))  "st" (Bool (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Num 6))) "holds"  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k10_card_3 :::"product""::: )  (Set  "("  ($#k3_compos_0 :::"JumpParts"::: )  (Set (Var "T")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: SCMFSA10:24 (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))  "st" (Bool (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Num 7))) "holds"  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k10_card_3 :::"product""::: )  (Set  "("  ($#k3_compos_0 :::"JumpParts"::: )  (Set (Var "T")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: SCMFSA10:25 (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))  "st" (Bool (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Num 8))) "holds"  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k10_card_3 :::"product""::: )  (Set  "("  ($#k3_compos_0 :::"JumpParts"::: )  (Set (Var "T")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: SCMFSA10:26 (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))  "st" (Bool (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Num 9))) "holds"  (Bool (Set   ($#k3_compos_0 :::"JumpParts"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: SCMFSA10:27 (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))  "st" (Bool (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Num 10))) "holds"  (Bool (Set   ($#k3_compos_0 :::"JumpParts"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: SCMFSA10:28 (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))  "st" (Bool (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Num 11))) "holds"  (Bool (Set   ($#k3_compos_0 :::"JumpParts"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: SCMFSA10:29 (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))  "st" (Bool (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Num 12))) "holds"  (Bool (Set   ($#k3_compos_0 :::"JumpParts"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: SCMFSA10:30 (Bool  "for" (Set (Var "i1")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k10_card_3 :::"product""::: )  (Set  "("  ($#k3_compos_0 :::"JumpParts"::: )  (Set  "("  ($#k2_compos_0 :::"InsCode"::: )  (Set  "("  ($#k11_scmfsa_2 :::"goto"::: )  (Set (Var "i1")) ")" ) ")" ) ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k5_numbers :::"NAT"::: )  ))) ; 
 
theorem :: SCMFSA10:31 (Bool  "for" (Set (Var "i1")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Int-Location":::) "holds"  (Bool (Set (Set  "("  ($#k10_card_3 :::"product""::: )  (Set  "("  ($#k3_compos_0 :::"JumpParts"::: )  (Set  "("  ($#k2_compos_0 :::"InsCode"::: )  (Set  "(" (Set (Var "a"))  ($#k12_scmfsa_2 :::"=0_goto"::: )  (Set (Var "i1")) ")" ) ")" ) ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k5_numbers :::"NAT"::: )  )))) ; 
 
theorem :: SCMFSA10:32 (Bool  "for" (Set (Var "i1")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Int-Location":::) "holds"  (Bool (Set (Set  "("  ($#k10_card_3 :::"product""::: )  (Set  "("  ($#k3_compos_0 :::"JumpParts"::: )  (Set  "("  ($#k2_compos_0 :::"InsCode"::: )  (Set  "(" (Set (Var "a"))  ($#k13_scmfsa_2 :::">0_goto"::: )  (Set (Var "i1")) ")" ) ")" ) ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k5_numbers :::"NAT"::: )  )))) ; 
 registration
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  ($#k2_compos_1 :::"halt"::: )  (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; registrationlet "a", "b" be   ($#m1_subset_1 :::"Int-Location":::); 
cluster (Set "a"  ($#k6_scmfsa_2 :::":="::: )  "b") ->   ($#v4_amistd_1 :::"sequential"::: )   ; 

cluster (Set   ($#k7_scmfsa_2 :::"AddTo"::: )   "(" "a" "," "b" ")" ) ->   ($#v4_amistd_1 :::"sequential"::: )   ; 

cluster (Set   ($#k8_scmfsa_2 :::"SubFrom"::: )   "(" "a" "," "b" ")" ) ->   ($#v4_amistd_1 :::"sequential"::: )   ; 

cluster (Set   ($#k9_scmfsa_2 :::"MultBy"::: )   "(" "a" "," "b" ")" ) ->   ($#v4_amistd_1 :::"sequential"::: )   ; 

cluster (Set   ($#k10_scmfsa_2 :::"Divide"::: )   "(" "a" "," "b" ")" ) ->   ($#v4_amistd_1 :::"sequential"::: )   ; 
end; registrationlet "a", "b" be   ($#m1_subset_1 :::"Int-Location":::); 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "(" "a"  ($#k6_scmfsa_2 :::":="::: )  "b" ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 

cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  ($#k7_scmfsa_2 :::"AddTo"::: )   "(" "a" "," "b" ")"  ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 

cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  ($#k8_scmfsa_2 :::"SubFrom"::: )   "(" "a" "," "b" ")"  ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 

cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  ($#k9_scmfsa_2 :::"MultBy"::: )   "(" "a" "," "b" ")"  ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 

cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  ($#k10_scmfsa_2 :::"Divide"::: )   "(" "a" "," "b" ")"  ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; 
theorem :: SCMFSA10:33 (Bool  "for" (Set (Var "i1")) "," (Set (Var "il")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k1_amistd_1 :::"NIC"::: )   "(" (Set  "("  ($#k11_scmfsa_2 :::"goto"::: )  (Set (Var "i1")) ")" ) "," (Set (Var "il")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "i1")) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: SCMFSA10:34 (Bool  "for" (Set (Var "i1")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  ($#k11_scmfsa_2 :::"goto"::: )  (Set (Var "i1")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "i1")) ($#k1_tarski :::"}"::: ) ))) ; 
 registrationlet "i1" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  ($#k11_scmfsa_2 :::"goto"::: )  "i1" ")" )) -> (Num 1)  ($#v3_card_1 :::"-element"::: )   ; 
end; 
theorem :: SCMFSA10:35 (Bool  "for" (Set (Var "i1")) "," (Set (Var "il")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Int-Location":::) "holds"  (Bool (Set   ($#k1_amistd_1 :::"NIC"::: )   "(" (Set  "(" (Set (Var "a"))  ($#k12_scmfsa_2 :::"=0_goto"::: )  (Set (Var "i1")) ")" ) "," (Set (Var "il")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "i1")) "," (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "il")) ")" ) ($#k2_tarski :::"}"::: ) )))) ; 
 
theorem :: SCMFSA10:36 (Bool  "for" (Set (Var "i1")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Int-Location":::) "holds"  (Bool (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "(" (Set (Var "a"))  ($#k12_scmfsa_2 :::"=0_goto"::: )  (Set (Var "i1")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "i1")) ($#k1_tarski :::"}"::: ) )))) ; 
 registrationlet "a" be   ($#m1_subset_1 :::"Int-Location":::); let "i1" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "(" "a"  ($#k12_scmfsa_2 :::"=0_goto"::: )  "i1" ")" )) -> (Num 1)  ($#v3_card_1 :::"-element"::: )   ; 
end; 
theorem :: SCMFSA10:37 (Bool  "for" (Set (Var "i1")) "," (Set (Var "il")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Int-Location":::) "holds"  (Bool (Set   ($#k1_amistd_1 :::"NIC"::: )   "(" (Set  "(" (Set (Var "a"))  ($#k13_scmfsa_2 :::">0_goto"::: )  (Set (Var "i1")) ")" ) "," (Set (Var "il")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "i1")) "," (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "il")) ")" ) ($#k2_tarski :::"}"::: ) )))) ; 
 
theorem :: SCMFSA10:38 (Bool  "for" (Set (Var "i1")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Int-Location":::) "holds"  (Bool (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "(" (Set (Var "a"))  ($#k13_scmfsa_2 :::">0_goto"::: )  (Set (Var "i1")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "i1")) ($#k1_tarski :::"}"::: ) )))) ; 
 registrationlet "a" be   ($#m1_subset_1 :::"Int-Location":::); let "i1" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "(" "a"  ($#k13_scmfsa_2 :::">0_goto"::: )  "i1" ")" )) -> (Num 1)  ($#v3_card_1 :::"-element"::: )   ; 
end; registrationlet "a", "b" be   ($#m1_subset_1 :::"Int-Location":::); let "f" be    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )  ; 
cluster (Set "a"  ($#k14_scmfsa_2 :::":="::: )   "(" "f" "," "b" ")" ) ->   ($#v4_amistd_1 :::"sequential"::: )   ; 
end; registrationlet "a", "b" be   ($#m1_subset_1 :::"Int-Location":::); let "f" be    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )  ; 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "(" "a"  ($#k14_scmfsa_2 :::":="::: )   "(" "f" "," "b" ")"  ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; registrationlet "a", "b" be   ($#m1_subset_1 :::"Int-Location":::); let "f" be    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )  ; 
cluster (Set  "(" "f" "," "b" ")"   ($#k15_scmfsa_2 :::":="::: )  "a") ->   ($#v4_amistd_1 :::"sequential"::: )   ; 
end; registrationlet "a", "b" be   ($#m1_subset_1 :::"Int-Location":::); let "f" be    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )  ; 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  "(" "f" "," "b" ")"   ($#k15_scmfsa_2 :::":="::: )  "a" ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; registrationlet "a" be   ($#m1_subset_1 :::"Int-Location":::); let "f" be    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )  ; 
cluster (Set "a"  ($#k16_scmfsa_2 :::":=len"::: )  "f") ->   ($#v4_amistd_1 :::"sequential"::: )   ; 
end; registrationlet "a" be   ($#m1_subset_1 :::"Int-Location":::); let "f" be    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )  ; 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "(" "a"  ($#k16_scmfsa_2 :::":=len"::: )  "f" ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; registrationlet "a" be   ($#m1_subset_1 :::"Int-Location":::); let "f" be    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )  ; 
cluster (Set "f"  ($#k17_scmfsa_2 :::":=<0,...,0>"::: )  "a") ->   ($#v4_amistd_1 :::"sequential"::: )   ; 
end; registrationlet "a" be   ($#m1_subset_1 :::"Int-Location":::); let "f" be    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )  ; 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "(" "f"  ($#k17_scmfsa_2 :::":=<0,...,0>"::: )  "a" ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; 
theorem :: SCMFSA10:39 (Bool  "for" (Set (Var "il")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k3_amistd_1 :::"SUCC"::: )   "(" (Set (Var "il")) "," (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "il")) "," (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "il")) ")" ) ($#k2_tarski :::"}"::: ) ))) ; 
 
theorem :: SCMFSA10:40 (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_amistd_1 :::"SUCC"::: )   "(" (Set (Var "k")) "," (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" )) & (Bool  "("   "for" (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "j"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_amistd_1 :::"SUCC"::: )   "(" (Set (Var "k")) "," (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ))) "holds"  (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j")))  ")" )  ")" )) ; 
 registration
cluster (Set   ($#k1_scmfsa_2 :::"SCM+FSA"::: )  ) ->   ($#v3_amistd_1 :::"standard"::: )   ; 
end; registration
cluster (Set (Set  "("  ($#k2_compos_1 :::"halt"::: )  (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" )  ($#k4_xtuple_0 :::"`1_3"::: )  ) ->   ($#v1_amistd_1 :::"jump-only"::: )    for  ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )); 
end; registration
cluster (Set   ($#k2_compos_1 :::"halt"::: )  (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )) ->   ($#v2_amistd_1 :::"jump-only"::: )   ; 
end; registrationlet "i1" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set (Set  "("  ($#k11_scmfsa_2 :::"goto"::: )  "i1" ")" )  ($#k4_xtuple_0 :::"`1_3"::: )  ) ->   ($#v1_amistd_1 :::"jump-only"::: )    for  ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )); 
end; registrationlet "i1" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set   ($#k11_scmfsa_2 :::"goto"::: )  "i1") ->  ($#~v4_compos_0  "non"   ($#v4_compos_0 :::"ins-loc-free"::: )   )    ($#v2_amistd_1 :::"jump-only"::: )    ($#~v4_amistd_1  "non"   ($#v4_amistd_1 :::"sequential"::: )   )  ; 
end; registrationlet "a" be   ($#m1_subset_1 :::"Int-Location":::); let "i1" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set (Set  "(" "a"  ($#k12_scmfsa_2 :::"=0_goto"::: )  "i1" ")" )  ($#k4_xtuple_0 :::"`1_3"::: )  ) ->   ($#v1_amistd_1 :::"jump-only"::: )    for  ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )); 

cluster (Set (Set  "(" "a"  ($#k13_scmfsa_2 :::">0_goto"::: )  "i1" ")" )  ($#k4_xtuple_0 :::"`1_3"::: )  ) ->   ($#v1_amistd_1 :::"jump-only"::: )    for  ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )); 
end; registrationlet "a" be   ($#m1_subset_1 :::"Int-Location":::); let "i1" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set "a"  ($#k12_scmfsa_2 :::"=0_goto"::: )  "i1") ->  ($#~v4_compos_0  "non"   ($#v4_compos_0 :::"ins-loc-free"::: )   )    ($#v2_amistd_1 :::"jump-only"::: )    ($#~v4_amistd_1  "non"   ($#v4_amistd_1 :::"sequential"::: )   )  ; 

cluster (Set "a"  ($#k13_scmfsa_2 :::">0_goto"::: )  "i1") ->  ($#~v4_compos_0  "non"   ($#v4_compos_0 :::"ins-loc-free"::: )   )    ($#v2_amistd_1 :::"jump-only"::: )    ($#~v4_amistd_1  "non"   ($#v4_amistd_1 :::"sequential"::: )   )  ; 
end; registrationlet "a", "b" be   ($#m1_subset_1 :::"Int-Location":::); 
cluster (Set (Set  "(" "a"  ($#k6_scmfsa_2 :::":="::: )  "b" ")" )  ($#k4_xtuple_0 :::"`1_3"::: )  ) ->  ($#~v1_amistd_1  "non"   ($#v1_amistd_1 :::"jump-only"::: )   )   for  ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )); 

cluster (Set (Set  "("  ($#k7_scmfsa_2 :::"AddTo"::: )   "(" "a" "," "b" ")"  ")" )  ($#k4_xtuple_0 :::"`1_3"::: )  ) ->  ($#~v1_amistd_1  "non"   ($#v1_amistd_1 :::"jump-only"::: )   )   for  ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )); 

cluster (Set (Set  "("  ($#k8_scmfsa_2 :::"SubFrom"::: )   "(" "a" "," "b" ")"  ")" )  ($#k4_xtuple_0 :::"`1_3"::: )  ) ->  ($#~v1_amistd_1  "non"   ($#v1_amistd_1 :::"jump-only"::: )   )   for  ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )); 

cluster (Set (Set  "("  ($#k9_scmfsa_2 :::"MultBy"::: )   "(" "a" "," "b" ")"  ")" )  ($#k4_xtuple_0 :::"`1_3"::: )  ) ->  ($#~v1_amistd_1  "non"   ($#v1_amistd_1 :::"jump-only"::: )   )   for  ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )); 

cluster (Set (Set  "("  ($#k10_scmfsa_2 :::"Divide"::: )   "(" "a" "," "b" ")"  ")" )  ($#k4_xtuple_0 :::"`1_3"::: )  ) ->  ($#~v1_amistd_1  "non"   ($#v1_amistd_1 :::"jump-only"::: )   )   for  ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )); 
end; registrationlet "a", "b" be   ($#m1_subset_1 :::"Int-Location":::); let "f" be    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )  ; 
cluster (Set (Set  "(" "b"  ($#k14_scmfsa_2 :::":="::: )   "(" "f" "," "a" ")"  ")" )  ($#k4_xtuple_0 :::"`1_3"::: )  ) ->  ($#~v1_amistd_1  "non"   ($#v1_amistd_1 :::"jump-only"::: )   )   for  ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )); 

cluster (Set (Set  "("  "(" "f" "," "a" ")"   ($#k15_scmfsa_2 :::":="::: )  "b" ")" )  ($#k4_xtuple_0 :::"`1_3"::: )  ) ->  ($#~v1_amistd_1  "non"   ($#v1_amistd_1 :::"jump-only"::: )   )   for  ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )); 
end; registrationlet "a", "b" be   ($#m1_subset_1 :::"Int-Location":::); let "f" be    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )  ; 
cluster (Set "b"  ($#k14_scmfsa_2 :::":="::: )   "(" "f" "," "a" ")" ) ->  ($#~v2_amistd_1  "non"   ($#v2_amistd_1 :::"jump-only"::: )   )  ; 

cluster (Set  "(" "f" "," "a" ")"   ($#k15_scmfsa_2 :::":="::: )  "b") ->  ($#~v2_amistd_1  "non"   ($#v2_amistd_1 :::"jump-only"::: )   )  ; 
end; registrationlet "a" be   ($#m1_subset_1 :::"Int-Location":::); let "f" be    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )  ; 
cluster (Set (Set  "(" "a"  ($#k16_scmfsa_2 :::":=len"::: )  "f" ")" )  ($#k4_xtuple_0 :::"`1_3"::: )  ) ->  ($#~v1_amistd_1  "non"   ($#v1_amistd_1 :::"jump-only"::: )   )   for  ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )); 

cluster (Set (Set  "(" "f"  ($#k17_scmfsa_2 :::":=<0,...,0>"::: )  "a" ")" )  ($#k4_xtuple_0 :::"`1_3"::: )  ) ->  ($#~v1_amistd_1  "non"   ($#v1_amistd_1 :::"jump-only"::: )   )   for  ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )); 
end; registrationlet "a" be   ($#m1_subset_1 :::"Int-Location":::); let "f" be    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )  ; 
cluster (Set "a"  ($#k16_scmfsa_2 :::":=len"::: )  "f") ->  ($#~v2_amistd_1  "non"   ($#v2_amistd_1 :::"jump-only"::: )   )  ; 

cluster (Set "f"  ($#k17_scmfsa_2 :::":=<0,...,0>"::: )  "a") ->  ($#~v2_amistd_1  "non"   ($#v2_amistd_1 :::"jump-only"::: )   )  ; 
end; registration
cluster (Set   ($#k1_scmfsa_2 :::"SCM+FSA"::: )  ) ->   ($#v2_amistd_2 :::"with_explicit_jumps"::: )   ; 
end; 
theorem :: SCMFSA10:41 (Bool  "for" (Set (Var "i1")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k5_compos_0 :::"IncAddr"::: )   "(" (Set  "("  ($#k11_scmfsa_2 :::"goto"::: )  (Set (Var "i1")) ")" ) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k11_scmfsa_2 :::"goto"::: )  (Set  "(" (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "k")) ")" ))))) ; 
 
theorem :: SCMFSA10:42 (Bool  "for" (Set (Var "i1")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Int-Location":::) "holds"  (Bool (Set   ($#k5_compos_0 :::"IncAddr"::: )   "(" (Set  "(" (Set (Var "a"))  ($#k12_scmfsa_2 :::"=0_goto"::: )  (Set (Var "i1")) ")" ) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k12_scmfsa_2 :::"=0_goto"::: )  (Set  "(" (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "k")) ")" )))))) ; 
 
theorem :: SCMFSA10:43 (Bool  "for" (Set (Var "i1")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Int-Location":::) "holds"  (Bool (Set   ($#k5_compos_0 :::"IncAddr"::: )   "(" (Set  "(" (Set (Var "a"))  ($#k13_scmfsa_2 :::">0_goto"::: )  (Set (Var "i1")) ")" ) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k13_scmfsa_2 :::">0_goto"::: )  (Set  "(" (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "k")) ")" )))))) ; 
 registration
cluster (Set   ($#k1_scmfsa_2 :::"SCM+FSA"::: )  ) ->   ($#v4_amistd_2 :::"IC-relocable"::: )   ; 
end;