:: SCMFSA_4  semantic presentation begin  















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

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

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

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

cluster (Set   ($#k10_scmfsa_2 :::"Divide"::: )   "(" "a" "," "b" ")" ) ->   ($#v4_compos_0 :::"ins-loc-free"::: )   ; 
end; 
theorem :: SCMFSA_4:1 (Bool  "for" (Set (Var "k")) "," (Set (Var "loc")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k5_compos_0 :::"IncAddr"::: )   "(" (Set  "("  ($#k11_scmfsa_2 :::"goto"::: )  (Set (Var "loc")) ")" ) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k11_scmfsa_2 :::"goto"::: )  (Set  "(" (Set (Var "loc"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "k")) ")" )))) ; 
 
theorem :: SCMFSA_4:2 (Bool  "for" (Set (Var "k")) "," (Set (Var "loc")) "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_compos_0 :::"IncAddr"::: )   "(" (Set  "(" (Set (Var "a"))  ($#k12_scmfsa_2 :::"=0_goto"::: )  (Set (Var "loc")) ")" ) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k12_scmfsa_2 :::"=0_goto"::: )  (Set  "(" (Set (Var "loc"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "k")) ")" ))))) ; 
 
theorem :: SCMFSA_4:3 (Bool  "for" (Set (Var "k")) "," (Set (Var "loc")) "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_compos_0 :::"IncAddr"::: )   "(" (Set  "(" (Set (Var "a"))  ($#k13_scmfsa_2 :::">0_goto"::: )  (Set (Var "loc")) ")" ) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k13_scmfsa_2 :::">0_goto"::: )  (Set  "(" (Set (Var "loc"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "k")) ")" ))))) ; 
 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" ")" ) ->   ($#v4_compos_0 :::"ins-loc-free"::: )   ; 

cluster (Set  "(" "f" "," "a" ")"   ($#k15_scmfsa_2 :::":="::: )  "b") ->   ($#v4_compos_0 :::"ins-loc-free"::: )   ; 
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_compos_0 :::"ins-loc-free"::: )   ; 

cluster (Set "f"  ($#k17_scmfsa_2 :::":=<0,...,0>"::: )  "a") ->   ($#v4_compos_0 :::"ins-loc-free"::: )   ; 
end; 


begin  registration
cluster (Set   ($#k1_scmfsa_2 :::"SCM+FSA"::: )  ) ->   ($#v2_amistd_5 :::"relocable"::: )   ; 
end; 
theorem :: SCMFSA_4:4 (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Bool  "not" (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "i")))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_enumset1 :::"{"::: ) (Num 6) "," (Num 7) "," (Num 8) ($#k1_enumset1 :::"}"::: ) )))) "holds"  (Bool (Set   ($#k5_compos_0 :::"IncAddr"::: )   "(" (Set (Var "i")) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "i"))))) ;