:: SCMFSA6C  semantic presentation begin  



























theorem :: SCMFSA6C:1 (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"::: ) )  (Bool  "for" (Set (Var "P")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "I")) "being"   ($#v1_scmfsa6b :::"keeping_0"::: )     ($#v7_amistd_1 :::"parahalting"::: )    ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "J")) "being"   ($#v7_amistd_1 :::"parahalting"::: )    ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool (Set (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set  "(" (Set (Var "I"))  ($#k3_scmfsa6a :::"";""::: )  (Set (Var "J")) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set (Var "J")) "," (Set (Var "P")) "," (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")"  ")" ) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a"))))))))) ; 
 
theorem :: SCMFSA6C:2 (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"::: ) )  (Bool  "for" (Set (Var "P")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "I")) "being"   ($#v1_scmfsa6b :::"keeping_0"::: )     ($#v7_amistd_1 :::"parahalting"::: )    ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "J")) "being"   ($#v7_amistd_1 :::"parahalting"::: )    ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool (Set (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set  "(" (Set (Var "I"))  ($#k3_scmfsa6a :::"";""::: )  (Set (Var "J")) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")"  ")" )  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set (Var "J")) "," (Set (Var "P")) "," (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")"  ")" ) ")"  ")" )  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f"))))))))) ; 
 begin  definitionlet "i" be   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); attr "i" is  :::"parahalting":::  means :: SCMFSA6C:def 1 (Bool (Set   ($#k11_compos_1 :::"Macro"::: )  "i") "is"   ($#v7_amistd_1 :::"parahalting"::: )  ); attr "i" is  :::"keeping_0":::  means :: SCMFSA6C:def 2 (Bool (Set   ($#k11_compos_1 :::"Macro"::: )  "i") "is"   ($#v1_scmfsa6b :::"keeping_0"::: )  ); end; 








:: deftheorem    defines :::"parahalting"::: SCMFSA6C:def 1 :  (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "i")) "is"   ($#v1_scmfsa6c :::"parahalting"::: )  ) "iff" (Bool (Set   ($#k11_compos_1 :::"Macro"::: )  (Set (Var "i"))) "is"   ($#v7_amistd_1 :::"parahalting"::: )  )  ")" )); 
 
:: deftheorem    defines :::"keeping_0"::: SCMFSA6C:def 2 :  (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "i")) "is"   ($#v2_scmfsa6c :::"keeping_0"::: )  ) "iff" (Bool (Set   ($#k11_compos_1 :::"Macro"::: )  (Set (Var "i"))) "is"   ($#v1_scmfsa6b :::"keeping_0"::: )  )  ")" )); 
 registration
cluster (Set   ($#k2_compos_1 :::"halt"::: )  (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )) ->   ($#v1_scmfsa6c :::"parahalting"::: )     ($#v2_scmfsa6c :::"keeping_0"::: )   ; 
end; registration
cluster   ($#v1_amistd_2 :::"with_explicit_jumps"::: )     ($#v3_amistd_2 :::"IC-relocable"::: )     ($#v1_scmfsa6c :::"parahalting"::: )     ($#v2_scmfsa6c :::"keeping_0"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )); 
end; registrationlet "i" be   ($#v1_scmfsa6c :::"parahalting"::: )    ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); 
cluster (Set   ($#k11_compos_1 :::"Macro"::: )  "i") ->   ($#v7_amistd_1 :::"parahalting"::: )   ; 
end; registrationlet "i" be   ($#v2_scmfsa6c :::"keeping_0"::: )    ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); 
cluster (Set   ($#k11_compos_1 :::"Macro"::: )  "i") ->   ($#v1_scmfsa6b :::"keeping_0"::: )   ; 
end; registrationlet "a", "b" be   ($#m1_subset_1 :::"Int-Location":::); 
cluster (Set "a"  ($#k6_scmfsa_2 :::":="::: )  "b") ->   ($#v1_scmfsa6c :::"parahalting"::: )   ; 

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

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

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

cluster (Set   ($#k10_scmfsa_2 :::"Divide"::: )   "(" "a" "," "b" ")" ) ->   ($#v1_scmfsa6c :::"parahalting"::: )   ; 
let "f" be    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )  ; 
cluster (Set "b"  ($#k14_scmfsa_2 :::":="::: )   "(" "f" "," "a" ")" ) ->   ($#v1_scmfsa6c :::"parahalting"::: )   ; 

cluster (Set  "(" "f" "," "a" ")"   ($#k15_scmfsa_2 :::":="::: )  "b") ->   ($#v1_scmfsa6c :::"parahalting"::: )     ($#v2_scmfsa6c :::"keeping_0"::: )   ; 
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") ->   ($#v1_scmfsa6c :::"parahalting"::: )   ; 

cluster (Set "f"  ($#k17_scmfsa_2 :::":=<0,...,0>"::: )  "a") ->   ($#v1_scmfsa6c :::"parahalting"::: )     ($#v2_scmfsa6c :::"keeping_0"::: )   ; 
end; registrationlet "a" be   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::); let "b" be   ($#m1_subset_1 :::"Int-Location":::); 
cluster (Set "a"  ($#k6_scmfsa_2 :::":="::: )  "b") ->   ($#v2_scmfsa6c :::"keeping_0"::: )   ; 

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

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

cluster (Set   ($#k9_scmfsa_2 :::"MultBy"::: )   "(" "a" "," "b" ")" ) ->   ($#v2_scmfsa6c :::"keeping_0"::: )   ; 
end; registrationlet "a", "b" be   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::); 
cluster (Set   ($#k10_scmfsa_2 :::"Divide"::: )   "(" "a" "," "b" ")" ) ->   ($#v2_scmfsa6c :::"keeping_0"::: )   ; 
end; registrationlet "a" be   ($#m1_subset_1 :::"Int-Location":::); let "f" be    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )  ; let "b" be   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::); 
cluster (Set "b"  ($#k14_scmfsa_2 :::":="::: )   "(" "f" "," "a" ")" ) ->   ($#v2_scmfsa6c :::"keeping_0"::: )   ; 
end; registrationlet "f" be    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )  ; let "b" be   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::); 
cluster (Set "b"  ($#k16_scmfsa_2 :::":=len"::: )  "f") ->   ($#v2_scmfsa6c :::"keeping_0"::: )   ; 
end; registrationlet "i" be   ($#v1_scmfsa6c :::"parahalting"::: )    ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "J" be   ($#v7_amistd_1 :::"parahalting"::: )    ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); 
cluster (Set "i"  ($#k4_scmfsa6a :::"";""::: )  "J") ->   ($#v7_amistd_1 :::"parahalting"::: )   ; 
end; registrationlet "I" be   ($#v7_amistd_1 :::"parahalting"::: )    ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "j" be   ($#v1_scmfsa6c :::"parahalting"::: )    ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); 
cluster (Set "I"  ($#k5_scmfsa6a :::"";""::: )  "j") ->   ($#v7_amistd_1 :::"parahalting"::: )   ; 
end; registrationlet "i", "j" be   ($#v1_scmfsa6c :::"parahalting"::: )    ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); 
cluster (Set "i"  ($#k6_scmfsa6a :::"";""::: )  "j") ->   ($#v7_amistd_1 :::"parahalting"::: )   ; 
end; registrationlet "i" be   ($#v2_scmfsa6c :::"keeping_0"::: )    ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "J" be   ($#v1_scmfsa6b :::"keeping_0"::: )    ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); 
cluster (Set "i"  ($#k4_scmfsa6a :::"";""::: )  "J") ->   ($#v1_scmfsa6b :::"keeping_0"::: )   ; 
end; registrationlet "I" be   ($#v1_scmfsa6b :::"keeping_0"::: )    ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "j" be   ($#v2_scmfsa6c :::"keeping_0"::: )    ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); 
cluster (Set "I"  ($#k5_scmfsa6a :::"";""::: )  "j") ->   ($#v1_scmfsa6b :::"keeping_0"::: )   ; 
end; registrationlet "i", "j" be   ($#v2_scmfsa6c :::"keeping_0"::: )    ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); 
cluster (Set "i"  ($#k6_scmfsa6a :::"";""::: )  "j") ->   ($#v1_scmfsa6b :::"keeping_0"::: )   ; 
end; begin  
theorem :: SCMFSA6C:3 canceled; 
 
theorem :: SCMFSA6C:4 (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set (Var "s1")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set (Var "s2"))))) "holds"  (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "("  ($#k2_extpro_1 :::"Exec"::: )   "(" (Set (Var "i")) "," (Set (Var "s1")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "("  ($#k2_extpro_1 :::"Exec"::: )   "(" (Set (Var "i")) "," (Set (Var "s2")) ")"  ")" ))))) ; 
 
theorem :: SCMFSA6C:5 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "P")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "i")) "being"   ($#v1_scmfsa6c :::"parahalting"::: )    ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool (Set   ($#k2_extpro_1 :::"Exec"::: )   "(" (Set (Var "i")) "," (Set  "("  ($#k1_scmfsa_m :::"Initialized"::: )  (Set (Var "s")) ")" ) ")" )  ($#r8_pboole :::"="::: )  (Set   ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set  "("  ($#k11_compos_1 :::"Macro"::: )  (Set (Var "i")) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ))))) ; 
 
theorem :: SCMFSA6C:6 (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"::: ) )  (Bool  "for" (Set (Var "P")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "I")) "being"   ($#v1_scmfsa6b :::"keeping_0"::: )     ($#v7_amistd_1 :::"parahalting"::: )    ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "j")) "being"   ($#v1_scmfsa6c :::"parahalting"::: )    ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool (Set (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set  "(" (Set (Var "I"))  ($#k5_scmfsa6a :::"";""::: )  (Set (Var "j")) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_extpro_1 :::"Exec"::: )   "(" (Set (Var "j")) "," (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")"  ")" ) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a"))))))))) ; 
 
theorem :: SCMFSA6C:7 (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"::: ) )  (Bool  "for" (Set (Var "P")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "I")) "being"   ($#v1_scmfsa6b :::"keeping_0"::: )     ($#v7_amistd_1 :::"parahalting"::: )    ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "j")) "being"   ($#v1_scmfsa6c :::"parahalting"::: )    ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool (Set (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set  "(" (Set (Var "I"))  ($#k5_scmfsa6a :::"";""::: )  (Set (Var "j")) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")"  ")" )  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_extpro_1 :::"Exec"::: )   "(" (Set (Var "j")) "," (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")"  ")" ) ")"  ")" )  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f"))))))))) ; 
 
theorem :: SCMFSA6C:8 (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"::: ) )  (Bool  "for" (Set (Var "P")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "i")) "being"   ($#v1_scmfsa6c :::"parahalting"::: )     ($#v2_scmfsa6c :::"keeping_0"::: )    ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "j")) "being"   ($#v1_scmfsa6c :::"parahalting"::: )    ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool (Set (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k6_scmfsa6a :::"";""::: )  (Set (Var "j")) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_extpro_1 :::"Exec"::: )   "(" (Set (Var "j")) "," (Set  "("  ($#k2_extpro_1 :::"Exec"::: )   "(" (Set (Var "i")) "," (Set  "("  ($#k1_scmfsa_m :::"Initialized"::: )  (Set (Var "s")) ")" ) ")"  ")" ) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a"))))))))) ; 
 
theorem :: SCMFSA6C:9 (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"::: ) )  (Bool  "for" (Set (Var "P")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "i")) "being"   ($#v1_scmfsa6c :::"parahalting"::: )     ($#v2_scmfsa6c :::"keeping_0"::: )    ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "j")) "being"   ($#v1_scmfsa6c :::"parahalting"::: )    ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool (Set (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k6_scmfsa6a :::"";""::: )  (Set (Var "j")) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")"  ")" )  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_extpro_1 :::"Exec"::: )   "(" (Set (Var "j")) "," (Set  "("  ($#k2_extpro_1 :::"Exec"::: )   "(" (Set (Var "i")) "," (Set  "("  ($#k1_scmfsa_m :::"Initialized"::: )  (Set (Var "s")) ")" ) ")"  ")" ) ")"  ")" )  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f"))))))))) ; 
 begin  definitionlet "a", "b" be   ($#m1_subset_1 :::"Int-Location":::); func  :::"swap":::  "(" "a" "," "b" ")"  ->   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) equals :: SCMFSA6C:def 3 (Set (Set  "(" (Set  "(" (Set  "("  ($#k5_sf_mastr :::"FirstNotUsed"::: )  (Set  "("  ($#k11_compos_1 :::"Macro"::: )  (Set  "(" "a"  ($#k6_scmfsa_2 :::":="::: )  "b" ")" ) ")" ) ")" )  ($#k6_scmfsa_2 :::":="::: )  "a" ")" )  ($#k6_scmfsa6a :::"";""::: )  (Set  "(" "a"  ($#k6_scmfsa_2 :::":="::: )  "b" ")" ) ")" )  ($#k5_scmfsa6a :::"";""::: )  (Set  "(" "b"  ($#k6_scmfsa_2 :::":="::: )  (Set  "("  ($#k5_sf_mastr :::"FirstNotUsed"::: )  (Set  "("  ($#k11_compos_1 :::"Macro"::: )  (Set  "(" "a"  ($#k6_scmfsa_2 :::":="::: )  "b" ")" ) ")" ) ")" ) ")" )); end; 






:: deftheorem    defines :::"swap"::: SCMFSA6C:def 3 :  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Int-Location":::) "holds"  (Bool (Set   ($#k1_scmfsa6c :::"swap"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k5_sf_mastr :::"FirstNotUsed"::: )  (Set  "("  ($#k11_compos_1 :::"Macro"::: )  (Set  "(" (Set (Var "a"))  ($#k6_scmfsa_2 :::":="::: )  (Set (Var "b")) ")" ) ")" ) ")" )  ($#k6_scmfsa_2 :::":="::: )  (Set (Var "a")) ")" )  ($#k6_scmfsa6a :::"";""::: )  (Set  "(" (Set (Var "a"))  ($#k6_scmfsa_2 :::":="::: )  (Set (Var "b")) ")" ) ")" )  ($#k5_scmfsa6a :::"";""::: )  (Set  "(" (Set (Var "b"))  ($#k6_scmfsa_2 :::":="::: )  (Set  "("  ($#k5_sf_mastr :::"FirstNotUsed"::: )  (Set  "("  ($#k11_compos_1 :::"Macro"::: )  (Set  "(" (Set (Var "a"))  ($#k6_scmfsa_2 :::":="::: )  (Set (Var "b")) ")" ) ")" ) ")" ) ")" )))); 
 registrationlet "a", "b" be   ($#m1_subset_1 :::"Int-Location":::); 
cluster (Set   ($#k1_scmfsa6c :::"swap"::: )   "(" "a" "," "b" ")" ) ->   ($#v7_amistd_1 :::"parahalting"::: )   ; 
end; registrationlet "a", "b" be   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::); 
cluster (Set   ($#k1_scmfsa6c :::"swap"::: )   "(" "a" "," "b" ")" ) ->   ($#v1_scmfsa6b :::"keeping_0"::: )   ; 
end; 
theorem :: SCMFSA6C:10 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "P")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set  "("  ($#k1_scmfsa6c :::"swap"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "b")))) & (Bool (Set (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set  "("  ($#k1_scmfsa6c :::"swap"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a"))))  ")" )))) ; 
 
theorem :: SCMFSA6C:11 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Int-Location":::) "holds"  (Bool (Set   ($#k4_sf_mastr :::"UsedInt*Loc"::: )  (Set  "("  ($#k1_scmfsa6c :::"swap"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ;