:: AMI_6  semantic presentation begin  


























theorem :: AMI_6:1 (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_ami_3 :::"SCM"::: ) ))  "holds"  (Bool  "("  (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Num 1)) "or" (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Num 2)) "or" (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Num 3)) "or" (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Num 4)) "or" (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Num 5)) "or" (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Num 6)) "or" (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Num 7)) "or" (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Num 8))  ")" )) ; 
 
theorem :: AMI_6:2 (Bool (Set   ($#k5_xtuple_0 :::"JumpPart"::: )  (Set  "("  ($#k2_compos_1 :::"halt"::: )  (Set  ($#k1_ami_3 :::"SCM"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) ; 
 
theorem :: AMI_6:3 (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_ami_3 :::"SCM"::: ) ))  "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 :: AMI_6:4 (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_ami_3 :::"SCM"::: ) ))  "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 :: AMI_6:5 (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_ami_3 :::"SCM"::: ) ))  "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 :: AMI_6:6 (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_ami_3 :::"SCM"::: ) ))  "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 :: AMI_6:7 (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_ami_3 :::"SCM"::: ) ))  "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 :: AMI_6:8 (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_ami_3 :::"SCM"::: ) ))  "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 :: AMI_6:9 (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_ami_3 :::"SCM"::: ) ))  "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 :: AMI_6:10 (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_ami_3 :::"SCM"::: ) ))  "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 :: AMI_6:11 (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_ami_3 :::"SCM"::: ) ))  "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 :: AMI_6:12 (Bool  "for" (Set (Var "k1")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "("  ($#k10_card_3 :::"product""::: )  (Set  "("  ($#k3_compos_0 :::"JumpParts"::: )  (Set  "("  ($#k2_compos_0 :::"InsCode"::: )  (Set  "("  ($#k7_ami_3 :::"SCM-goto"::: )  (Set (Var "k1")) ")" ) ")" ) ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k5_numbers :::"NAT"::: )  ))) ; 
 
theorem :: AMI_6:13 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Data-Location":::)  (Bool  "for" (Set (Var "k1")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "("  ($#k10_card_3 :::"product""::: )  (Set  "("  ($#k3_compos_0 :::"JumpParts"::: )  (Set  "("  ($#k2_compos_0 :::"InsCode"::: )  (Set  "(" (Set (Var "a"))  ($#k8_ami_3 :::"=0_goto"::: )  (Set (Var "k1")) ")" ) ")" ) ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k5_numbers :::"NAT"::: )  )))) ; 
 
theorem :: AMI_6:14 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Data-Location":::)  (Bool  "for" (Set (Var "k1")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "("  ($#k10_card_3 :::"product""::: )  (Set  "("  ($#k3_compos_0 :::"JumpParts"::: )  (Set  "("  ($#k2_compos_0 :::"InsCode"::: )  (Set  "(" (Set (Var "a"))  ($#k9_ami_3 :::">0_goto"::: )  (Set (Var "k1")) ")" ) ")" ) ")" ) ")" )  ($#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_ami_3 :::"SCM"::: ) ) ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; registrationlet "a", "b" be   ($#m1_subset_1 :::"Data-Location":::); 
cluster (Set "a"  ($#k2_ami_3 :::":="::: )  "b") ->   ($#v4_amistd_1 :::"sequential"::: )   ; 

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

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

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

cluster (Set   ($#k6_ami_3 :::"Divide"::: )   "(" "a" "," "b" ")" ) ->   ($#v4_amistd_1 :::"sequential"::: )   ; 
end; registrationlet "a", "b" be   ($#m1_subset_1 :::"Data-Location":::); 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "(" "a"  ($#k2_ami_3 :::":="::: )  "b" ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; registrationlet "a", "b" be   ($#m1_subset_1 :::"Data-Location":::); 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  ($#k3_ami_3 :::"AddTo"::: )   "(" "a" "," "b" ")"  ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; registrationlet "a", "b" be   ($#m1_subset_1 :::"Data-Location":::); 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  ($#k4_ami_3 :::"SubFrom"::: )   "(" "a" "," "b" ")"  ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; registrationlet "a", "b" be   ($#m1_subset_1 :::"Data-Location":::); 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  ($#k5_ami_3 :::"MultBy"::: )   "(" "a" "," "b" ")"  ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; registrationlet "a", "b" be   ($#m1_subset_1 :::"Data-Location":::); 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  ($#k6_ami_3 :::"Divide"::: )   "(" "a" "," "b" ")"  ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; 
theorem :: AMI_6:15 (Bool  "for" (Set (Var "il")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k1_amistd_1 :::"NIC"::: )   "(" (Set  "("  ($#k7_ami_3 :::"SCM-goto"::: )  (Set (Var "k")) ")" ) "," (Set (Var "il")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "k")) ($#k1_tarski :::"}"::: ) )))) ; 
 
theorem :: AMI_6:16 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  ($#k7_ami_3 :::"SCM-goto"::: )  (Set (Var "k")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "k")) ($#k1_tarski :::"}"::: ) ))) ; 
 registrationlet "i1" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  ($#k7_ami_3 :::"SCM-goto"::: )  "i1" ")" )) -> (Num 1)  ($#v3_card_1 :::"-element"::: )   ; 
end; 
theorem :: AMI_6:17 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Data-Location":::)  (Bool  "for" (Set (Var "il")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k1_amistd_1 :::"NIC"::: )   "(" (Set  "(" (Set (Var "a"))  ($#k8_ami_3 :::"=0_goto"::: )  (Set (Var "k")) ")" ) "," (Set (Var "il")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "k")) "," (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "il")) ")" ) ($#k2_tarski :::"}"::: ) ))))) ; 
 
theorem :: AMI_6:18 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Data-Location":::)  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "(" (Set (Var "a"))  ($#k8_ami_3 :::"=0_goto"::: )  (Set (Var "k")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "k")) ($#k1_tarski :::"}"::: ) )))) ; 
 registrationlet "a" be   ($#m1_subset_1 :::"Data-Location":::); let "i1" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "(" "a"  ($#k8_ami_3 :::"=0_goto"::: )  "i1" ")" )) -> (Num 1)  ($#v3_card_1 :::"-element"::: )   ; 
end; 
theorem :: AMI_6:19 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Data-Location":::)  (Bool  "for" (Set (Var "il")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k1_amistd_1 :::"NIC"::: )   "(" (Set  "(" (Set (Var "a"))  ($#k9_ami_3 :::">0_goto"::: )  (Set (Var "k")) ")" ) "," (Set (Var "il")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "k")) "," (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "il")) ")" ) ($#k2_tarski :::"}"::: ) ))))) ; 
 
theorem :: AMI_6:20 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Data-Location":::)  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "(" (Set (Var "a"))  ($#k9_ami_3 :::">0_goto"::: )  (Set (Var "k")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "k")) ($#k1_tarski :::"}"::: ) )))) ; 
 registrationlet "a" be   ($#m1_subset_1 :::"Data-Location":::); let "i1" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "(" "a"  ($#k9_ami_3 :::">0_goto"::: )  "i1" ")" )) -> (Num 1)  ($#v3_card_1 :::"-element"::: )   ; 
end; 
theorem :: AMI_6:21 (Bool  "for" (Set (Var "il")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k3_amistd_1 :::"SUCC"::: )   "(" (Set (Var "il")) "," (Set  ($#k1_ami_3 :::"SCM"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "il")) "," (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "il")) ")" ) ($#k2_tarski :::"}"::: ) ))) ; 
 
theorem :: AMI_6:22 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Set (Var "k"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_amistd_1 :::"SUCC"::: )   "(" (Set (Var "k")) "," (Set  ($#k1_ami_3 :::"SCM"::: ) ) ")" )) & (Bool  "("   "for" (Set (Var "j")) "being"    ($#m1_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_ami_3 :::"SCM"::: ) ) ")" ))) "holds"  (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j")))  ")" )  ")" )) ; 
 registration
cluster (Set   ($#k1_ami_3 :::"SCM"::: )  ) ->   ($#v3_amistd_1 :::"standard"::: )   ; 
end; registration
cluster (Set   ($#k4_xtuple_0 :::"InsCode"::: )  (Set  "("  ($#k2_compos_1 :::"halt"::: )  (Set  ($#k1_ami_3 :::"SCM"::: ) ) ")" )) ->   ($#v1_amistd_1 :::"jump-only"::: )    for  ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_ami_3 :::"SCM"::: ) )); 
end; registration
cluster (Set   ($#k2_compos_1 :::"halt"::: )  (Set  ($#k1_ami_3 :::"SCM"::: ) )) ->   ($#v2_amistd_1 :::"jump-only"::: )   ; 
end; registrationlet "i1" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set   ($#k4_xtuple_0 :::"InsCode"::: )  (Set  "("  ($#k7_ami_3 :::"SCM-goto"::: )  "i1" ")" )) ->   ($#v1_amistd_1 :::"jump-only"::: )    for  ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_ami_3 :::"SCM"::: ) )); 
end; registrationlet "i1" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set   ($#k7_ami_3 :::"SCM-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 :::"Data-Location":::); let "i1" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set   ($#k4_xtuple_0 :::"InsCode"::: )  (Set  "(" "a"  ($#k8_ami_3 :::"=0_goto"::: )  "i1" ")" )) ->   ($#v1_amistd_1 :::"jump-only"::: )    for  ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_ami_3 :::"SCM"::: ) )); 

cluster (Set   ($#k4_xtuple_0 :::"InsCode"::: )  (Set  "(" "a"  ($#k9_ami_3 :::">0_goto"::: )  "i1" ")" )) ->   ($#v1_amistd_1 :::"jump-only"::: )    for  ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_ami_3 :::"SCM"::: ) )); 
end; registrationlet "a" be   ($#m1_subset_1 :::"Data-Location":::); let "i1" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set "a"  ($#k8_ami_3 :::"=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"  ($#k9_ami_3 :::">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 :::"Data-Location":::); 
cluster (Set   ($#k4_xtuple_0 :::"InsCode"::: )  (Set  "(" "a"  ($#k2_ami_3 :::":="::: )  "b" ")" )) ->  ($#~v1_amistd_1  "non"   ($#v1_amistd_1 :::"jump-only"::: )   )   for  ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_ami_3 :::"SCM"::: ) )); 

cluster (Set   ($#k4_xtuple_0 :::"InsCode"::: )  (Set  "("  ($#k3_ami_3 :::"AddTo"::: )   "(" "a" "," "b" ")"  ")" )) ->  ($#~v1_amistd_1  "non"   ($#v1_amistd_1 :::"jump-only"::: )   )   for  ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_ami_3 :::"SCM"::: ) )); 

cluster (Set   ($#k4_xtuple_0 :::"InsCode"::: )  (Set  "("  ($#k4_ami_3 :::"SubFrom"::: )   "(" "a" "," "b" ")"  ")" )) ->  ($#~v1_amistd_1  "non"   ($#v1_amistd_1 :::"jump-only"::: )   )   for  ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_ami_3 :::"SCM"::: ) )); 

cluster (Set   ($#k4_xtuple_0 :::"InsCode"::: )  (Set  "("  ($#k5_ami_3 :::"MultBy"::: )   "(" "a" "," "b" ")"  ")" )) ->  ($#~v1_amistd_1  "non"   ($#v1_amistd_1 :::"jump-only"::: )   )   for  ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_ami_3 :::"SCM"::: ) )); 

cluster (Set   ($#k4_xtuple_0 :::"InsCode"::: )  (Set  "("  ($#k6_ami_3 :::"Divide"::: )   "(" "a" "," "b" ")"  ")" )) ->  ($#~v1_amistd_1  "non"   ($#v1_amistd_1 :::"jump-only"::: )   )   for  ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_ami_3 :::"SCM"::: ) )); 
end; registrationlet "a", "b" be   ($#m1_subset_1 :::"Data-Location":::); 
cluster (Set "a"  ($#k2_ami_3 :::":="::: )  "b") ->  ($#~v2_amistd_1  "non"   ($#v2_amistd_1 :::"jump-only"::: )   )  ; 

cluster (Set   ($#k3_ami_3 :::"AddTo"::: )   "(" "a" "," "b" ")" ) ->  ($#~v2_amistd_1  "non"   ($#v2_amistd_1 :::"jump-only"::: )   )  ; 

cluster (Set   ($#k4_ami_3 :::"SubFrom"::: )   "(" "a" "," "b" ")" ) ->  ($#~v2_amistd_1  "non"   ($#v2_amistd_1 :::"jump-only"::: )   )  ; 

cluster (Set   ($#k5_ami_3 :::"MultBy"::: )   "(" "a" "," "b" ")" ) ->  ($#~v2_amistd_1  "non"   ($#v2_amistd_1 :::"jump-only"::: )   )  ; 

cluster (Set   ($#k6_ami_3 :::"Divide"::: )   "(" "a" "," "b" ")" ) ->  ($#~v2_amistd_1  "non"   ($#v2_amistd_1 :::"jump-only"::: )   )  ; 
end; registration
cluster (Set   ($#k1_ami_3 :::"SCM"::: )  ) ->   ($#v2_amistd_2 :::"with_explicit_jumps"::: )   ; 
end; 
theorem :: AMI_6:23 (Bool  "for" (Set (Var "i1")) "being"    ($#m1_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  "("  ($#k7_ami_3 :::"SCM-goto"::: )  (Set (Var "i1")) ")" ) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k7_ami_3 :::"SCM-goto"::: )  (Set  "(" (Set (Var "i1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k")) ")" ))))) ; 
 
theorem :: AMI_6:24 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Data-Location":::)  (Bool  "for" (Set (Var "i1")) "being"    ($#m1_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  "(" (Set (Var "a"))  ($#k8_ami_3 :::"=0_goto"::: )  (Set (Var "i1")) ")" ) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k8_ami_3 :::"=0_goto"::: )  (Set  "(" (Set (Var "i1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k")) ")" )))))) ; 
 
theorem :: AMI_6:25 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Data-Location":::)  (Bool  "for" (Set (Var "i1")) "being"    ($#m1_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  "(" (Set (Var "a"))  ($#k9_ami_3 :::">0_goto"::: )  (Set (Var "i1")) ")" ) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k9_ami_3 :::">0_goto"::: )  (Set  "(" (Set (Var "i1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k")) ")" )))))) ; 
 registration
cluster (Set   ($#k1_ami_3 :::"SCM"::: )  ) ->   ($#v4_amistd_2 :::"IC-relocable"::: )   ; 
end;