:: RELOC  semantic presentation begin  




registrationlet "a", "b" be   ($#m1_subset_1 :::"Data-Location":::); 
cluster (Set "a"  ($#k2_ami_3 :::":="::: )  "b") ->   ($#v4_compos_0 :::"ins-loc-free"::: )   ; 

cluster (Set   ($#k3_ami_3 :::"AddTo"::: )   "(" "a" "," "b" ")" ) ->   ($#v4_compos_0 :::"ins-loc-free"::: )   ; 

cluster (Set   ($#k4_ami_3 :::"SubFrom"::: )   "(" "a" "," "b" ")" ) ->   ($#v4_compos_0 :::"ins-loc-free"::: )   ; 

cluster (Set   ($#k5_ami_3 :::"MultBy"::: )   "(" "a" "," "b" ")" ) ->   ($#v4_compos_0 :::"ins-loc-free"::: )   ; 

cluster (Set   ($#k6_ami_3 :::"Divide"::: )   "(" "a" "," "b" ")" ) ->   ($#v4_compos_0 :::"ins-loc-free"::: )   ; 
end; 
theorem :: RELOC:1 (Bool  "for" (Set (Var "k")) "," (Set (Var "loc")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k5_compos_0 :::"IncAddr"::: )   "(" (Set  "("  ($#k7_ami_3 :::"SCM-goto"::: )  (Set (Var "loc")) ")" ) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k7_ami_3 :::"SCM-goto"::: )  (Set  "(" (Set (Var "loc"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k")) ")" )))) ; 
 
theorem :: RELOC:2 (Bool  "for" (Set (Var "k")) "," (Set (Var "loc")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Data-Location":::) "holds"  (Bool (Set   ($#k5_compos_0 :::"IncAddr"::: )   "(" (Set  "(" (Set (Var "a"))  ($#k8_ami_3 :::"=0_goto"::: )  (Set (Var "loc")) ")" ) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k8_ami_3 :::"=0_goto"::: )  (Set  "(" (Set (Var "loc"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k")) ")" ))))) ; 
 
theorem :: RELOC:3 (Bool  "for" (Set (Var "k")) "," (Set (Var "loc")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Data-Location":::) "holds"  (Bool (Set   ($#k5_compos_0 :::"IncAddr"::: )   "(" (Set  "(" (Set (Var "a"))  ($#k9_ami_3 :::">0_goto"::: )  (Set (Var "loc")) ")" ) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k9_ami_3 :::">0_goto"::: )  (Set  "(" (Set (Var "loc"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k")) ")" ))))) ; 
 
theorem :: RELOC:4 (Bool  "for" (Set (Var "I")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_ami_3 :::"SCM"::: ) )  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool  "("  (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "I")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "I")))  ($#r1_hidden :::"="::: )  (Num 1)) "or" (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "I")))  ($#r1_hidden :::"="::: )  (Num 2)) "or" (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "I")))  ($#r1_hidden :::"="::: )  (Num 3)) "or" (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "I")))  ($#r1_hidden :::"="::: )  (Num 4)) "or" (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "I")))  ($#r1_hidden :::"="::: )  (Num 5))  ")" )) "holds"  (Bool (Set   ($#k5_compos_0 :::"IncAddr"::: )   "(" (Set (Var "I")) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "I"))))) ; 
 
theorem :: RELOC:5 (Bool  "for" (Set (Var "II")) "," (Set (Var "I")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_ami_3 :::"SCM"::: ) )  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool  "("  (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "I")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "I")))  ($#r1_hidden :::"="::: )  (Num 1)) "or" (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "I")))  ($#r1_hidden :::"="::: )  (Num 2)) "or" (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "I")))  ($#r1_hidden :::"="::: )  (Num 3)) "or" (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "I")))  ($#r1_hidden :::"="::: )  (Num 4)) "or" (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "I")))  ($#r1_hidden :::"="::: )  (Num 5))  ")" ) & (Bool (Set   ($#k5_compos_0 :::"IncAddr"::: )   "(" (Set (Var "II")) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "I")))) "holds"  (Bool (Set (Var "II"))  ($#r1_hidden :::"="::: )  (Set (Var "I"))))) ; 
 registration
cluster (Set   ($#k1_ami_3 :::"SCM"::: )  ) ->   ($#v2_amistd_5 :::"relocable"::: )   ; 
end; begin  
theorem :: RELOC:6 (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "q")) "being" (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_ami_3 :::"SCM"::: ) ))  ($#v5_relat_1 :::"-valued"::: )     ($#v1_finset_1 :::"finite"::: )    ($#~v2_compos_1  "non"   ($#v2_compos_1 :::"halt-free"::: )   )   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "p")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  (Set (Var "b2"))  ($#v4_extpro_1 :::"-autonomic"::: )    ($#m1_hidden :::"FinPartState":::) "of" (Set  ($#k1_ami_3 :::"SCM"::: ) )  (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_ami_3 :::"SCM"::: ) )  "st" (Bool (Bool (Set   ($#k4_struct_0 :::"IC"::: )  )  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "p")))) & (Bool (Set (Var "p"))  ($#r1_tarski :::"c="::: )  (Set (Var "s1"))) & (Bool (Set   ($#k9_memstr_0 :::"IncIC"::: )   "(" (Set (Var "p")) "," (Set (Var "k")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Var "s2")))) "holds"  (Bool  "for" (Set (Var "P1")) "," (Set (Var "P2")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_ami_3 :::"SCM"::: ) )  "st" (Bool (Bool (Set (Var "q"))  ($#r1_tarski :::"c="::: )  (Set (Var "P1"))) & (Bool (Set   ($#k6_compos_1 :::"Reloc"::: )   "(" (Set (Var "q")) "," (Set (Var "k")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Var "P2")))) "holds"  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k5_memstr_0 :::"IC"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" ) ")" )  ($#k2_nat_1 :::"+"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_memstr_0 :::"IC"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")"  ")" ))))))))) ; 
 registration
cluster (Set   ($#k1_ami_3 :::"SCM"::: )  ) ->   ($#v5_amistd_5 :::"relocable1"::: )     ($#v6_amistd_5 :::"relocable2"::: )   ; 
end; 
theorem :: RELOC:7 (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "q")) "being" (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_ami_3 :::"SCM"::: ) ))  ($#v5_relat_1 :::"-valued"::: )     ($#v1_finset_1 :::"finite"::: )    ($#~v2_compos_1  "non"   ($#v2_compos_1 :::"halt-free"::: )   )   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "p")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  (Set (Var "b2"))  ($#v4_extpro_1 :::"-autonomic"::: )    ($#m1_hidden :::"FinPartState":::) "of" (Set  ($#k1_ami_3 :::"SCM"::: ) )  (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "s3")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_ami_3 :::"SCM"::: ) )  "st" (Bool (Bool (Set   ($#k4_struct_0 :::"IC"::: )  )  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "p")))) & (Bool (Set (Var "p"))  ($#r1_tarski :::"c="::: )  (Set (Var "s1"))) & (Bool (Set   ($#k9_memstr_0 :::"IncIC"::: )   "(" (Set (Var "p")) "," (Set (Var "k")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Var "s2"))) & (Bool (Set (Var "s3"))  ($#r6_pboole :::"="::: )  (Set (Set (Var "s1"))  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k6_memstr_0 :::"DataPart"::: )  (Set (Var "s2")) ")" )))) "holds"  (Bool  "for" (Set (Var "P1")) "," (Set (Var "P2")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_ami_3 :::"SCM"::: ) )  "st" (Bool (Bool (Set (Var "q"))  ($#r1_tarski :::"c="::: )  (Set (Var "P1"))) & (Bool (Set   ($#k6_compos_1 :::"Reloc"::: )   "(" (Set (Var "q")) "," (Set (Var "k")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Var "P2")))) "holds"  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s3")) "," (Set (Var "i")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")"  ")" ))))))))) ;