:: SFMASTR3  semantic presentation begin  































theorem :: SFMASTR3:1 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "aa")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of"   (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "I"))  ($#r5_scmfsa7b :::"is_closed_on"::: )  (Set   ($#k1_scmfsa_m :::"Initialized"::: )  (Set (Var "s"))) "," (Set (Var "p"))) & (Bool (Set (Var "I"))  ($#r6_scmfsa7b :::"is_halting_on"::: )  (Set   ($#k1_scmfsa_m :::"Initialized"::: )  (Set (Var "s"))) "," (Set (Var "p"))) & (Bool (Bool  "not" (Set (Var "I"))  ($#r4_scmfsa7b :::"destroys"::: )  (Set (Var "aa"))))) "holds"  (Bool (Set (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "aa")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_scmfsa_m :::"Initialized"::: )  (Set (Var "s")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "aa")))))))) ; 
 
theorem :: SFMASTR3:2 (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"::: ) )  "st" (Bool (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set  "("  ($#k4_compos_1 :::"Stop"::: )  (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set (Var "s")))))) ; 
 
theorem :: SFMASTR3:3 (Bool  "for" (Set (Var "aa")) "being"   ($#m1_subset_1 :::"Int-Location":::)  "holds" (Bool (Bool  "not" (Set   ($#k4_compos_1 :::"Stop"::: )  (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))  ($#r2_scmfsa7b :::"refers"::: )  (Set (Var "aa"))))) ; 
 
theorem :: SFMASTR3:4 (Bool  "for" (Set (Var "aa")) "," (Set (Var "bb")) "," (Set (Var "cc")) "being"   ($#m1_subset_1 :::"Int-Location":::)  "st" (Bool (Bool (Set (Var "aa"))  ($#r1_hidden :::"<>"::: )  (Set (Var "bb")))) "holds"  (Bool  "not" (Bool (Set (Set (Var "cc"))  ($#k6_scmfsa_2 :::":="::: )  (Set (Var "bb")))  ($#r1_scmfsa7b :::"refers"::: )  (Set (Var "aa"))))) ; 
 
theorem :: SFMASTR3:5 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "bb")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )   "holds"  (Bool (Set (Set  "("  ($#k2_extpro_1 :::"Exec"::: )   "(" (Set  "(" (Set (Var "a"))  ($#k14_scmfsa_2 :::":="::: )   "(" (Set (Var "f")) "," (Set (Var "bb")) ")"  ")" ) "," (Set (Var "s")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "s"))  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k1_int_2 :::"abs"::: )  (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "bb")) ")" ) ")" ))))))) ; 
 
theorem :: SFMASTR3:6 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "aa")) "," (Set (Var "bb")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )   "holds"  (Bool (Set (Set  "("  ($#k2_extpro_1 :::"Exec"::: )   "(" (Set  "("  "(" (Set (Var "f")) "," (Set (Var "aa")) ")"   ($#k15_scmfsa_2 :::":="::: )  (Set (Var "bb")) ")" ) "," (Set (Var "s")) ")"  ")" )  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "s"))  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")) ")" )  ($#k2_funct_7 :::"+*"::: )   "(" (Set  "("  ($#k1_int_2 :::"abs"::: )  (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "aa")) ")" ) ")" ) "," (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "bb")) ")" ) ")" ))))) ; 
 registrationlet "a" be   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::); let "b" be   ($#m1_subset_1 :::"Int-Location":::); let "I", "J" be   ($#v1_scmfsa7b :::"good"::: )    ($#m1_hidden :::"Program":::) "of" ; 
cluster (Set   ($#k5_scmfsa8b :::"if>0"::: )   "(" "a" "," "b" "," "I" "," "J" ")" ) ->   ($#v1_scmfsa7b :::"good"::: )   ; 
end; 
theorem :: SFMASTR3:7 (Bool  "for" (Set (Var "aa")) "," (Set (Var "bb")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "," (Set (Var "J")) "being"   ($#m1_hidden :::"Program":::) "of"  "holds"  (Bool (Set   ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set  "("  ($#k5_scmfsa8b :::"if>0"::: )   "(" (Set (Var "aa")) "," (Set (Var "bb")) "," (Set (Var "I")) "," (Set (Var "J")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k5_scmfsa_m :::"{"::: ) (Set (Var "aa")) "," (Set (Var "bb")) ($#k5_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "I")) ")" ) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "J")) ")" ))))) ; 
 
theorem :: SFMASTR3:8 (Bool  "for" (Set (Var "aa")) "," (Set (Var "bb")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of"   "st" (Bool (Bool (Bool  "not" (Set (Var "I"))  ($#r4_scmfsa7b :::"destroys"::: )  (Set (Var "aa"))))) "holds"  (Bool  "not" (Bool (Set   ($#k2_scmfsa_9 :::"while>0"::: )   "(" (Set (Var "bb")) "," (Set (Var "I")) ")" )  ($#r4_scmfsa7b :::"destroys"::: )  (Set (Var "aa")))))) ; 
 
theorem :: SFMASTR3:9 (Bool  "for" (Set (Var "cc")) "," (Set (Var "aa")) "," (Set (Var "bb")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "," (Set (Var "J")) "being"   ($#m1_hidden :::"Program":::) "of"   "st" (Bool (Bool (Set (Var "cc"))  ($#r1_hidden :::"<>"::: )  (Set (Var "aa"))) & (Bool (Bool  "not" (Set (Var "I"))  ($#r4_scmfsa7b :::"destroys"::: )  (Set (Var "cc")))) & (Bool (Bool  "not" (Set (Var "J"))  ($#r4_scmfsa7b :::"destroys"::: )  (Set (Var "cc"))))) "holds"  (Bool  "not" (Bool (Set   ($#k5_scmfsa8b :::"if>0"::: )   "(" (Set (Var "aa")) "," (Set (Var "bb")) "," (Set (Var "I")) "," (Set (Var "J")) ")" )  ($#r4_scmfsa7b :::"destroys"::: )  (Set (Var "cc")))))) ; 
 begin  definitionlet "p" be   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "a", "b", "c" be   ($#m1_subset_1 :::"Int-Location":::); let "I" be   ($#m1_hidden :::"Program":::) "of" ; let "s" be   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); func  :::"StepForUp":::  "(" "a" "," "b" "," "c" "," "I" "," "p" "," "s" ")"  ->   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  "("  ($#k4_card_3 :::"product"::: )  (Set  "("  ($#k2_memstr_0 :::"the_Values_of"::: )  (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ) equals :: SFMASTR3:def 1 (Set   ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) "a" "," "b" "," "c" ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  "I" ")" ) ")" ) ")" ) "," (Set  "(" (Set  "(" "I"  ($#k5_scmfsa6a :::"";""::: )  (Set  "("  ($#k7_scmfsa_2 :::"AddTo"::: )   "(" "a" "," (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")"  ")" ) ")" )  ($#k5_scmfsa6a :::"";""::: )  (Set  "("  ($#k8_scmfsa_2 :::"SubFrom"::: )   "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) "a" "," "b" "," "c" ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  "I" ")" ) ")" ) ")" ) "," (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")"  ")" ) ")" ) "," "p" "," (Set  "(" (Set  "(" "s"  ($#k2_funct_7 :::"+*"::: )   "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) "a" "," "b" "," "c" ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  "I" ")" ) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set  "(" "s"  ($#k1_funct_1 :::"."::: )  "c" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" "s"  ($#k1_funct_1 :::"."::: )  "b" ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) ")"  ")" )  ($#k2_funct_7 :::"+*"::: )   "(" "a" "," (Set  "(" "s"  ($#k1_funct_1 :::"."::: )  "b" ")" ) ")"  ")" ) ")" ); end; 










:: deftheorem    defines :::"StepForUp"::: SFMASTR3:def 1 :  (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")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of"   (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool (Set   ($#k1_sfmastr3 :::"StepForUp"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "I")) ")" ) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "I"))  ($#k5_scmfsa6a :::"";""::: )  (Set  "("  ($#k7_scmfsa_2 :::"AddTo"::: )   "(" (Set (Var "a")) "," (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")"  ")" ) ")" )  ($#k5_scmfsa6a :::"";""::: )  (Set  "("  ($#k8_scmfsa_2 :::"SubFrom"::: )   "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "I")) ")" ) ")" ) ")" ) "," (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")"  ")" ) ")" ) "," (Set (Var "p")) "," (Set  "(" (Set  "(" (Set (Var "s"))  ($#k2_funct_7 :::"+*"::: )   "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "I")) ")" ) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "b")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) ")"  ")" )  ($#k2_funct_7 :::"+*"::: )   "(" (Set (Var "a")) "," (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "b")) ")" ) ")"  ")" ) ")" )))))); 
 
theorem :: SFMASTR3:10 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "bb")) "," (Set (Var "cc")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of"   (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k1_sfmastr3 :::"StepForUp"::: )   "(" (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))))))) ; 
 
theorem :: SFMASTR3:11 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "bb")) "," (Set (Var "cc")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of"   (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k1_sfmastr3 :::"StepForUp"::: )   "(" (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "bb"))))))))) ; 
 
theorem :: SFMASTR3:12 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "bb")) "," (Set (Var "cc")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of"   (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "bb")))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k1_sfmastr3 :::"StepForUp"::: )   "(" (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "bb")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "bb"))))))))) ; 
 
theorem :: SFMASTR3:13 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "cc")) "," (Set (Var "bb")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of"   (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "cc")))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k1_sfmastr3 :::"StepForUp"::: )   "(" (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "cc")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "cc"))))))))) ; 
 
theorem :: SFMASTR3:14 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "dd")) "," (Set (Var "bb")) "," (Set (Var "cc")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of"   (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "dd"))) & (Bool (Set (Var "dd"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "I"))))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k1_sfmastr3 :::"StepForUp"::: )   "(" (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "dd")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "dd"))))))))) ; 
 
theorem :: SFMASTR3:15 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "bb")) "," (Set (Var "cc")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )    (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of"   (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k1_sfmastr3 :::"StepForUp"::: )   "(" (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")))))))))) ; 
 
theorem :: SFMASTR3:16 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "bb")) "," (Set (Var "cc")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of"   (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool  "for" (Set (Var "aux")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  "st" (Bool (Bool (Set (Var "aux"))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "I")) ")" ) ")" )))) "holds"  (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "aux"))  ($#k6_scmfsa_2 :::":="::: )  (Set (Var "cc")) ")" )  ($#k6_scmfsa6a :::"";""::: )  (Set  "("  ($#k8_scmfsa_2 :::"SubFrom"::: )   "(" (Set (Var "aux")) "," (Set (Var "bb")) ")"  ")" ) ")" )  ($#k5_scmfsa6a :::"";""::: )  (Set  "("  ($#k7_scmfsa_2 :::"AddTo"::: )   "(" (Set (Var "aux")) "," (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")"  ")" ) ")" )  ($#k5_scmfsa6a :::"";""::: )  (Set  "(" (Set (Var "a"))  ($#k6_scmfsa_2 :::":="::: )  (Set (Var "bb")) ")" ) ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "(" (Set  "(" (Set (Var "s"))  ($#k2_funct_7 :::"+*"::: )   "(" (Set (Var "aux")) "," (Set  "(" (Set  "(" (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "cc")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "bb")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) ")"  ")" )  ($#k2_funct_7 :::"+*"::: )   "(" (Set (Var "a")) "," (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "bb")) ")" ) ")"  ")" ))))))))) ; 
 definitionlet "p" be   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "a", "b", "c" be   ($#m1_subset_1 :::"Int-Location":::); let "I" be   ($#m1_hidden :::"Program":::) "of" ; let "s" be   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); pred  :::"ProperForUpBody"::: "a" "," "b" "," "c" "," "I" "," "s" "," "p" means :: SFMASTR3:def 2 (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" (Set  "(" "s"  ($#k1_funct_1 :::"."::: )  "c" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" "s"  ($#k1_funct_1 :::"."::: )  "b" ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1)))) "holds"  (Bool  "("  (Bool "I"  ($#r5_scmfsa7b :::"is_closed_on"::: )  (Set (Set  "("  ($#k1_sfmastr3 :::"StepForUp"::: )   "(" "a" "," "b" "," "c" "," "I" "," "p" "," "s" ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "i"))) "," (Set "p"  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k2_scmfsa_9 :::"while>0"::: )   "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) "a" "," "b" "," "c" ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  "I" ")" ) ")" ) ")" ) "," (Set  "(" (Set  "(" "I"  ($#k5_scmfsa6a :::"";""::: )  (Set  "("  ($#k7_scmfsa_2 :::"AddTo"::: )   "(" "a" "," (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")"  ")" ) ")" )  ($#k5_scmfsa6a :::"";""::: )  (Set  "("  ($#k8_scmfsa_2 :::"SubFrom"::: )   "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) "a" "," "b" "," "c" ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  "I" ")" ) ")" ) ")" ) "," (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")"  ")" ) ")" ) ")"  ")" ))) & (Bool "I"  ($#r6_scmfsa7b :::"is_halting_on"::: )  (Set (Set  "("  ($#k1_sfmastr3 :::"StepForUp"::: )   "(" "a" "," "b" "," "c" "," "I" "," "p" "," "s" ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "i"))) "," (Set "p"  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k2_scmfsa_9 :::"while>0"::: )   "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) "a" "," "b" "," "c" ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  "I" ")" ) ")" ) ")" ) "," (Set  "(" (Set  "(" "I"  ($#k5_scmfsa6a :::"";""::: )  (Set  "("  ($#k7_scmfsa_2 :::"AddTo"::: )   "(" "a" "," (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")"  ")" ) ")" )  ($#k5_scmfsa6a :::"";""::: )  (Set  "("  ($#k8_scmfsa_2 :::"SubFrom"::: )   "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) "a" "," "b" "," "c" ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  "I" ")" ) ")" ) ")" ) "," (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")"  ")" ) ")" ) ")"  ")" )))  ")" )); end; 









:: deftheorem    defines :::"ProperForUpBody"::: SFMASTR3:def 2 :  (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")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of"   (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"   (Bool  "("  (Bool   ($#r1_sfmastr3 :::"ProperForUpBody"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "I")) "," (Set (Var "s")) "," (Set (Var "p"))) "iff" (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "b")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1)))) "holds"  (Bool  "("  (Bool (Set (Var "I"))  ($#r5_scmfsa7b :::"is_closed_on"::: )  (Set (Set  "("  ($#k1_sfmastr3 :::"StepForUp"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "i"))) "," (Set (Set (Var "p"))  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k2_scmfsa_9 :::"while>0"::: )   "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "I")) ")" ) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "I"))  ($#k5_scmfsa6a :::"";""::: )  (Set  "("  ($#k7_scmfsa_2 :::"AddTo"::: )   "(" (Set (Var "a")) "," (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")"  ")" ) ")" )  ($#k5_scmfsa6a :::"";""::: )  (Set  "("  ($#k8_scmfsa_2 :::"SubFrom"::: )   "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "I")) ")" ) ")" ) ")" ) "," (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")"  ")" ) ")" ) ")"  ")" ))) & (Bool (Set (Var "I"))  ($#r6_scmfsa7b :::"is_halting_on"::: )  (Set (Set  "("  ($#k1_sfmastr3 :::"StepForUp"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "i"))) "," (Set (Set (Var "p"))  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k2_scmfsa_9 :::"while>0"::: )   "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "I")) ")" ) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "I"))  ($#k5_scmfsa6a :::"";""::: )  (Set  "("  ($#k7_scmfsa_2 :::"AddTo"::: )   "(" (Set (Var "a")) "," (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")"  ")" ) ")" )  ($#k5_scmfsa6a :::"";""::: )  (Set  "("  ($#k8_scmfsa_2 :::"SubFrom"::: )   "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "I")) ")" ) ")" ) ")" ) "," (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")"  ")" ) ")" ) ")"  ")" )))  ")" ))  ")" ))))); 
 
theorem :: SFMASTR3:17 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "aa")) "," (Set (Var "bb")) "," (Set (Var "cc")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "I")) "being"   ($#v7_amistd_1 :::"parahalting"::: )    ($#m1_hidden :::"Program":::) "of"  "holds"  (Bool   ($#r1_sfmastr3 :::"ProperForUpBody"::: )  (Set (Var "aa")) "," (Set (Var "bb")) "," (Set (Var "cc")) "," (Set (Var "I")) "," (Set (Var "s")) "," (Set (Var "p"))))))) ; 
 
theorem :: SFMASTR3:18 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "bb")) "," (Set (Var "cc")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "Ig")) "being"   ($#v1_scmfsa7b :::"good"::: )    ($#m1_hidden :::"Program":::) "of"   (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Set  "(" (Set  "("  ($#k1_sfmastr3 :::"StepForUp"::: )   "(" (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) "," (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "Ig"))  ($#r5_scmfsa7b :::"is_closed_on"::: )  (Set (Set  "("  ($#k1_sfmastr3 :::"StepForUp"::: )   "(" (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) "," (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k"))) "," (Set (Set (Var "p"))  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k2_scmfsa_9 :::"while>0"::: )   "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "Ig")) ")" ) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "Ig"))  ($#k5_scmfsa6a :::"";""::: )  (Set  "("  ($#k7_scmfsa_2 :::"AddTo"::: )   "(" (Set (Var "a")) "," (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")"  ")" ) ")" )  ($#k5_scmfsa6a :::"";""::: )  (Set  "("  ($#k8_scmfsa_2 :::"SubFrom"::: )   "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "Ig")) ")" ) ")" ) ")" ) "," (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")"  ")" ) ")" ) ")"  ")" ))) & (Bool (Set (Var "Ig"))  ($#r6_scmfsa7b :::"is_halting_on"::: )  (Set (Set  "("  ($#k1_sfmastr3 :::"StepForUp"::: )   "(" (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) "," (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k"))) "," (Set (Set (Var "p"))  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k2_scmfsa_9 :::"while>0"::: )   "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "Ig")) ")" ) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "Ig"))  ($#k5_scmfsa6a :::"";""::: )  (Set  "("  ($#k7_scmfsa_2 :::"AddTo"::: )   "(" (Set (Var "a")) "," (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")"  ")" ) ")" )  ($#k5_scmfsa6a :::"";""::: )  (Set  "("  ($#k8_scmfsa_2 :::"SubFrom"::: )   "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "Ig")) ")" ) ")" ) ")" ) "," (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")"  ")" ) ")" ) ")"  ")" )))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k1_sfmastr3 :::"StepForUp"::: )   "(" (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) "," (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1)))))))) ; 
 
theorem :: SFMASTR3:19 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "bb")) "," (Set (Var "cc")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "Ig")) "being"   ($#v1_scmfsa7b :::"good"::: )    ($#m1_hidden :::"Program":::) "of"   (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool   ($#r1_sfmastr3 :::"ProperForUpBody"::: )  (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) "," (Set (Var "Ig")) "," (Set (Var "s")) "," (Set (Var "p")))) "holds"  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "cc")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "bb")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1)))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set  "("  ($#k1_sfmastr3 :::"StepForUp"::: )   "(" (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) "," (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1)) &  "("  (Bool (Bool (Bool  "not" (Set (Var "Ig"))  ($#r4_scmfsa7b :::"destroys"::: )  (Set (Var "a"))))) "implies" (Bool  "("  (Bool (Set (Set  "(" (Set  "("  ($#k1_sfmastr3 :::"StepForUp"::: )   "(" (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) "," (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "bb")) ")" ))) & (Bool (Set (Set  "(" (Set  "("  ($#k1_sfmastr3 :::"StepForUp"::: )   "(" (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) "," (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "cc")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1)))  ")" )  ")"  & (Bool (Set (Set  "(" (Set  "(" (Set  "("  ($#k1_sfmastr3 :::"StepForUp"::: )   "(" (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) "," (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "Ig")) ")" ) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "cc")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "bb")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1)))  ")" ))))))) ; 
 
theorem :: SFMASTR3:20 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "bb")) "," (Set (Var "cc")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "Ig")) "being"   ($#v1_scmfsa7b :::"good"::: )    ($#m1_hidden :::"Program":::) "of"   (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool   ($#r1_sfmastr3 :::"ProperForUpBody"::: )  (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) "," (Set (Var "Ig")) "," (Set (Var "s")) "," (Set (Var "p")))) "holds"  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Set  "(" (Set  "("  ($#k1_sfmastr3 :::"StepForUp"::: )   "(" (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) "," (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "Ig")) ")" ) ")" ) ")" ))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "cc")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "bb")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1)))  ")" ))))))) ; 
 
theorem :: SFMASTR3:21 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "bb")) "," (Set (Var "cc")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "Ig")) "being"   ($#v1_scmfsa7b :::"good"::: )    ($#m1_hidden :::"Program":::) "of"   (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool   ($#r1_sfmastr3 :::"ProperForUpBody"::: )  (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) "," (Set (Var "Ig")) "," (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "cc")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "bb")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1)))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k1_sfmastr3 :::"StepForUp"::: )   "(" (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) "," (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "Ig")) ")" ) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set  "(" (Set (Var "Ig"))  ($#k5_scmfsa6a :::"";""::: )  (Set  "("  ($#k7_scmfsa_2 :::"AddTo"::: )   "(" (Set (Var "a")) "," (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")"  ")" ) ")" ) "," (Set  "(" (Set (Var "p"))  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k2_scmfsa_9 :::"while>0"::: )   "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "Ig")) ")" ) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "Ig"))  ($#k5_scmfsa6a :::"";""::: )  (Set  "("  ($#k7_scmfsa_2 :::"AddTo"::: )   "(" (Set (Var "a")) "," (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")"  ")" ) ")" )  ($#k5_scmfsa6a :::"";""::: )  (Set  "("  ($#k8_scmfsa_2 :::"SubFrom"::: )   "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "Ig")) ")" ) ")" ) ")" ) "," (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")"  ")" ) ")" ) ")"  ")" ) ")" ) "," (Set  "(" (Set  "("  ($#k1_sfmastr3 :::"StepForUp"::: )   "(" (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) "," (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" ) ")"  ")" )  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "Ig")) ")" ) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) ) ")" ))))))))) ; 
 definitionlet "a", "b", "c" be   ($#m1_subset_1 :::"Int-Location":::); let "I" be   ($#m1_hidden :::"Program":::) "of" ; func  :::"for-up":::  "(" "a" "," "b" "," "c" "," "I" ")"  ->   ($#m1_hidden :::"Program":::) "of"  equals :: SFMASTR3:def 3 (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) "a" "," "b" "," "c" ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  "I" ")" ) ")" ) ")" )  ($#k6_scmfsa_2 :::":="::: )  "c" ")" )  ($#k6_scmfsa6a :::"";""::: )  (Set  "("  ($#k8_scmfsa_2 :::"SubFrom"::: )   "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) "a" "," "b" "," "c" ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  "I" ")" ) ")" ) ")" ) "," "b" ")"  ")" ) ")" )  ($#k5_scmfsa6a :::"";""::: )  (Set  "("  ($#k7_scmfsa_2 :::"AddTo"::: )   "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) "a" "," "b" "," "c" ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  "I" ")" ) ")" ) ")" ) "," (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")"  ")" ) ")" )  ($#k5_scmfsa6a :::"";""::: )  (Set  "(" "a"  ($#k6_scmfsa_2 :::":="::: )  "b" ")" ) ")" )  ($#k3_scmfsa6a :::"";""::: )  (Set  "("  ($#k2_scmfsa_9 :::"while>0"::: )   "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) "a" "," "b" "," "c" ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  "I" ")" ) ")" ) ")" ) "," (Set  "(" (Set  "(" "I"  ($#k5_scmfsa6a :::"";""::: )  (Set  "("  ($#k7_scmfsa_2 :::"AddTo"::: )   "(" "a" "," (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")"  ")" ) ")" )  ($#k5_scmfsa6a :::"";""::: )  (Set  "("  ($#k8_scmfsa_2 :::"SubFrom"::: )   "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) "a" "," "b" "," "c" ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  "I" ")" ) ")" ) ")" ) "," (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")"  ")" ) ")" ) ")"  ")" )); end; 








:: deftheorem    defines :::"for-up"::: SFMASTR3:def 3 :  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of"  "holds"  (Bool (Set   ($#k2_sfmastr3 :::"for-up"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "I")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "I")) ")" ) ")" ) ")" )  ($#k6_scmfsa_2 :::":="::: )  (Set (Var "c")) ")" )  ($#k6_scmfsa6a :::"";""::: )  (Set  "("  ($#k8_scmfsa_2 :::"SubFrom"::: )   "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "I")) ")" ) ")" ) ")" ) "," (Set (Var "b")) ")"  ")" ) ")" )  ($#k5_scmfsa6a :::"";""::: )  (Set  "("  ($#k7_scmfsa_2 :::"AddTo"::: )   "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "I")) ")" ) ")" ) ")" ) "," (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")"  ")" ) ")" )  ($#k5_scmfsa6a :::"";""::: )  (Set  "(" (Set (Var "a"))  ($#k6_scmfsa_2 :::":="::: )  (Set (Var "b")) ")" ) ")" )  ($#k3_scmfsa6a :::"";""::: )  (Set  "("  ($#k2_scmfsa_9 :::"while>0"::: )   "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "I")) ")" ) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "I"))  ($#k5_scmfsa6a :::"";""::: )  (Set  "("  ($#k7_scmfsa_2 :::"AddTo"::: )   "(" (Set (Var "a")) "," (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")"  ")" ) ")" )  ($#k5_scmfsa6a :::"";""::: )  (Set  "("  ($#k8_scmfsa_2 :::"SubFrom"::: )   "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "I")) ")" ) ")" ) ")" ) "," (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")"  ")" ) ")" ) ")"  ")" ))))); 
 
theorem :: SFMASTR3:22 (Bool  "for" (Set (Var "aa")) "," (Set (Var "bb")) "," (Set (Var "cc")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of"  "holds"  (Bool (Set (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "aa")) "," (Set (Var "bb")) "," (Set (Var "cc")) ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "I")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set  "("  ($#k2_sfmastr3 :::"for-up"::: )   "(" (Set (Var "aa")) "," (Set (Var "bb")) "," (Set (Var "cc")) "," (Set (Var "I")) ")"  ")" ))))) ; 
 registrationlet "a" be   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::); let "b", "c" be   ($#m1_subset_1 :::"Int-Location":::); let "I" be   ($#v1_scmfsa7b :::"good"::: )    ($#m1_hidden :::"Program":::) "of" ; 
cluster (Set   ($#k2_sfmastr3 :::"for-up"::: )   "(" "a" "," "b" "," "c" "," "I" ")" ) ->   ($#v1_scmfsa7b :::"good"::: )   ; 
end; 
theorem :: SFMASTR3:23 (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "aa")) "," (Set (Var "bb")) "," (Set (Var "cc")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of"   "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "aa"))) & (Bool (Set (Var "aa"))  ($#r1_hidden :::"<>"::: )  (Set (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "(" (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) ($#k6_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "I")) ")" ) ")" ))) & (Bool (Bool  "not" (Set (Var "I"))  ($#r4_scmfsa7b :::"destroys"::: )  (Set (Var "aa"))))) "holds"  (Bool  "not" (Bool (Set   ($#k2_sfmastr3 :::"for-up"::: )   "(" (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) "," (Set (Var "I")) ")" )  ($#r4_scmfsa7b :::"destroys"::: )  (Set (Var "aa"))))))) ; 
 
theorem :: SFMASTR3:24 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "bb")) "," (Set (Var "cc")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of"   (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "bb")))  ($#r1_xxreal_0 :::">"::: )  (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "cc"))))) "holds"  (Bool  "("  (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Int-Location":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a"))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set  ($#k5_scmfsa_m :::"{"::: ) (Set (Var "bb")) "," (Set (Var "cc")) ($#k5_scmfsa_m :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "I")) ")" )))) "holds"  (Bool (Set (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set  "("  ($#k2_sfmastr3 :::"for-up"::: )   "(" (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) "," (Set (Var "I")) ")"  ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x"))))  ")" ) & (Bool  "("   "for" (Set (Var "f")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )   "holds"  (Bool (Set (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set  "("  ($#k2_sfmastr3 :::"for-up"::: )   "(" (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) "," (Set (Var "I")) ")"  ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f"))))  ")" )  ")" )))))) ; 
 
theorem :: SFMASTR3:25 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "cc")) "," (Set (Var "bb")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "Ig")) "being"   ($#v1_scmfsa7b :::"good"::: )    ($#m1_hidden :::"Program":::) "of"   (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "cc")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "bb")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1))) & (Bool  "("  (Bool   ($#r1_sfmastr3 :::"ProperForUpBody"::: )  (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) "," (Set (Var "Ig")) "," (Set (Var "s")) "," (Set (Var "p"))) "or" (Bool (Set (Var "Ig")) "is"   ($#v7_amistd_1 :::"parahalting"::: )  )  ")" )) "holds"  (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set  "("  ($#k2_sfmastr3 :::"for-up"::: )   "(" (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) "," (Set (Var "Ig")) ")"  ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "(" (Set  "("  ($#k1_sfmastr3 :::"StepForUp"::: )   "(" (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) "," (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" ))))))))) ; 
 
theorem :: SFMASTR3:26 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "bb")) "," (Set (Var "cc")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "Ig")) "being"   ($#v1_scmfsa7b :::"good"::: )    ($#m1_hidden :::"Program":::) "of"   (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool  "("  (Bool   ($#r1_sfmastr3 :::"ProperForUpBody"::: )  (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) "," (Set (Var "Ig")) "," (Set (Var "s")) "," (Set (Var "p"))) "or" (Bool (Set (Var "Ig")) "is"   ($#v7_amistd_1 :::"parahalting"::: )  )  ")" )) "holds"  (Bool  "("  (Bool (Set   ($#k2_sfmastr3 :::"for-up"::: )   "(" (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) "," (Set (Var "Ig")) ")" )  ($#r5_scmfsa7b :::"is_closed_on"::: )  (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set   ($#k2_sfmastr3 :::"for-up"::: )   "(" (Set (Var "a")) "," (Set (Var "bb")) "," (Set (Var "cc")) "," (Set (Var "Ig")) ")" )  ($#r6_scmfsa7b :::"is_halting_on"::: )  (Set (Var "s")) "," (Set (Var "p")))  ")" )))))) ; 
 begin  definitionlet "start", "finish", "minpos" be   ($#m1_subset_1 :::"Int-Location":::); let "f" be    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )  ; func  :::"FinSeqMin":::  "(" "f" "," "start" "," "finish" "," "minpos" ")"  ->   ($#m1_hidden :::"Program":::) "of"  equals :: SFMASTR3:def 4 (Set (Set  "(" "minpos"  ($#k6_scmfsa_2 :::":="::: )  "start" ")" )  ($#k4_scmfsa6a :::"";""::: )  (Set  "("  ($#k2_sfmastr3 :::"for-up"::: )   "(" (Set  "(" (Num 3)  ($#k9_scmfsa_m :::"-rdRWNotIn"::: )  (Set  ($#k6_scmfsa_m :::"{"::: ) "start" "," "finish" "," "minpos" ($#k6_scmfsa_m :::"}"::: ) ) ")" ) "," "start" "," "finish" "," (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  ($#k6_scmfsa_m :::"{"::: ) "start" "," "finish" "," "minpos" ($#k6_scmfsa_m :::"}"::: ) ) ")" )  ($#k14_scmfsa_2 :::":="::: )   "(" "f" "," (Set  "(" (Num 3)  ($#k9_scmfsa_m :::"-rdRWNotIn"::: )  (Set  ($#k6_scmfsa_m :::"{"::: ) "start" "," "finish" "," "minpos" ($#k6_scmfsa_m :::"}"::: ) ) ")" ) ")"  ")" )  ($#k6_scmfsa6a :::"";""::: )  (Set  "(" (Set  "(" (Num 2)  ($#k9_scmfsa_m :::"-ndRWNotIn"::: )  (Set  ($#k6_scmfsa_m :::"{"::: ) "start" "," "finish" "," "minpos" ($#k6_scmfsa_m :::"}"::: ) ) ")" )  ($#k14_scmfsa_2 :::":="::: )   "(" "f" "," "minpos" ")"  ")" ) ")" )  ($#k3_scmfsa6a :::"";""::: )  (Set  "("  ($#k5_scmfsa8b :::"if>0"::: )   "(" (Set  "(" (Num 2)  ($#k9_scmfsa_m :::"-ndRWNotIn"::: )  (Set  ($#k6_scmfsa_m :::"{"::: ) "start" "," "finish" "," "minpos" ($#k6_scmfsa_m :::"}"::: ) ) ")" ) "," (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  ($#k6_scmfsa_m :::"{"::: ) "start" "," "finish" "," "minpos" ($#k6_scmfsa_m :::"}"::: ) ) ")" ) "," (Set  "("  ($#k11_compos_1 :::"Macro"::: )  (Set  "(" "minpos"  ($#k6_scmfsa_2 :::":="::: )  (Set  "(" (Num 3)  ($#k9_scmfsa_m :::"-rdRWNotIn"::: )  (Set  ($#k6_scmfsa_m :::"{"::: ) "start" "," "finish" "," "minpos" ($#k6_scmfsa_m :::"}"::: ) ) ")" ) ")" ) ")" ) "," (Set  "("  ($#k4_compos_1 :::"Stop"::: )  (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")"  ")" ) ")" ) ")"  ")" )); end; 








:: deftheorem    defines :::"FinSeqMin"::: SFMASTR3:def 4 :  (Bool  "for" (Set (Var "start")) "," (Set (Var "finish")) "," (Set (Var "minpos")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )   "holds"  (Bool (Set   ($#k3_sfmastr3 :::"FinSeqMin"::: )   "(" (Set (Var "f")) "," (Set (Var "start")) "," (Set (Var "finish")) "," (Set (Var "minpos")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "minpos"))  ($#k6_scmfsa_2 :::":="::: )  (Set (Var "start")) ")" )  ($#k4_scmfsa6a :::"";""::: )  (Set  "("  ($#k2_sfmastr3 :::"for-up"::: )   "(" (Set  "(" (Num 3)  ($#k9_scmfsa_m :::"-rdRWNotIn"::: )  (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "start")) "," (Set (Var "finish")) "," (Set (Var "minpos")) ($#k6_scmfsa_m :::"}"::: ) ) ")" ) "," (Set (Var "start")) "," (Set (Var "finish")) "," (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "start")) "," (Set (Var "finish")) "," (Set (Var "minpos")) ($#k6_scmfsa_m :::"}"::: ) ) ")" )  ($#k14_scmfsa_2 :::":="::: )   "(" (Set (Var "f")) "," (Set  "(" (Num 3)  ($#k9_scmfsa_m :::"-rdRWNotIn"::: )  (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "start")) "," (Set (Var "finish")) "," (Set (Var "minpos")) ($#k6_scmfsa_m :::"}"::: ) ) ")" ) ")"  ")" )  ($#k6_scmfsa6a :::"";""::: )  (Set  "(" (Set  "(" (Num 2)  ($#k9_scmfsa_m :::"-ndRWNotIn"::: )  (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "start")) "," (Set (Var "finish")) "," (Set (Var "minpos")) ($#k6_scmfsa_m :::"}"::: ) ) ")" )  ($#k14_scmfsa_2 :::":="::: )   "(" (Set (Var "f")) "," (Set (Var "minpos")) ")"  ")" ) ")" )  ($#k3_scmfsa6a :::"";""::: )  (Set  "("  ($#k5_scmfsa8b :::"if>0"::: )   "(" (Set  "(" (Num 2)  ($#k9_scmfsa_m :::"-ndRWNotIn"::: )  (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "start")) "," (Set (Var "finish")) "," (Set (Var "minpos")) ($#k6_scmfsa_m :::"}"::: ) ) ")" ) "," (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "start")) "," (Set (Var "finish")) "," (Set (Var "minpos")) ($#k6_scmfsa_m :::"}"::: ) ) ")" ) "," (Set  "("  ($#k11_compos_1 :::"Macro"::: )  (Set  "(" (Set (Var "minpos"))  ($#k6_scmfsa_2 :::":="::: )  (Set  "(" (Num 3)  ($#k9_scmfsa_m :::"-rdRWNotIn"::: )  (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "start")) "," (Set (Var "finish")) "," (Set (Var "minpos")) ($#k6_scmfsa_m :::"}"::: ) ) ")" ) ")" ) ")" ) "," (Set  "("  ($#k4_compos_1 :::"Stop"::: )  (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")"  ")" ) ")" ) ")"  ")" ))))); 
 registrationlet "start", "finish" be   ($#m1_subset_1 :::"Int-Location":::); let "minpos" be   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::); let "f" be    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )  ; 
cluster (Set   ($#k3_sfmastr3 :::"FinSeqMin"::: )   "(" "f" "," "start" "," "finish" "," "minpos" ")" ) ->   ($#v1_scmfsa7b :::"good"::: )   ; 
end; 
theorem :: SFMASTR3:27 (Bool  "for" (Set (Var "c")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "aa")) "," (Set (Var "bb")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set (Var "aa")))) "holds"  (Bool  "not" (Bool (Set   ($#k3_sfmastr3 :::"FinSeqMin"::: )   "(" (Set (Var "f")) "," (Set (Var "aa")) "," (Set (Var "bb")) "," (Set (Var "c")) ")" )  ($#r4_scmfsa7b :::"destroys"::: )  (Set (Var "aa"))))))) ; 
 
theorem :: SFMASTR3:28 (Bool  "for" (Set (Var "c")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "aa")) "," (Set (Var "bb")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )   "holds"  (Bool (Set  ($#k6_scmfsa_m :::"{"::: ) (Set (Var "aa")) "," (Set (Var "bb")) "," (Set (Var "c")) ($#k6_scmfsa_m :::"}"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set  "("  ($#k3_sfmastr3 :::"FinSeqMin"::: )   "(" (Set (Var "f")) "," (Set (Var "aa")) "," (Set (Var "bb")) "," (Set (Var "c")) ")"  ")" )))))) ; 
 
theorem :: SFMASTR3:29 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "c")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "aa")) "," (Set (Var "bb")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool  "("  (Bool (Set   ($#k3_sfmastr3 :::"FinSeqMin"::: )   "(" (Set (Var "f")) "," (Set (Var "aa")) "," (Set (Var "bb")) "," (Set (Var "c")) ")" )  ($#r5_scmfsa7b :::"is_closed_on"::: )  (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set   ($#k3_sfmastr3 :::"FinSeqMin"::: )   "(" (Set (Var "f")) "," (Set (Var "aa")) "," (Set (Var "bb")) "," (Set (Var "c")) ")" )  ($#r6_scmfsa7b :::"is_halting_on"::: )  (Set (Var "s")) "," (Set (Var "p")))  ")" )))))) ; 
 
theorem :: SFMASTR3:30 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "c")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "aa")) "," (Set (Var "bb")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "aa"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Var "bb"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set  "("  ($#k3_sfmastr3 :::"FinSeqMin"::: )   "(" (Set (Var "f")) "," (Set (Var "aa")) "," (Set (Var "bb")) "," (Set (Var "c")) ")"  ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")))) & (Bool (Set (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set  "("  ($#k3_sfmastr3 :::"FinSeqMin"::: )   "(" (Set (Var "f")) "," (Set (Var "aa")) "," (Set (Var "bb")) "," (Set (Var "c")) ")"  ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "aa")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "aa")))) & (Bool (Set (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set  "("  ($#k3_sfmastr3 :::"FinSeqMin"::: )   "(" (Set (Var "f")) "," (Set (Var "aa")) "," (Set (Var "bb")) "," (Set (Var "c")) ")"  ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "bb")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "bb"))))  ")" )))))) ; 
 
theorem :: SFMASTR3:31 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "c")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "aa")) "," (Set (Var "bb")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "aa")))) & (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "aa")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "bb")))) & (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "bb")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set (Var "s"))  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Var "aa"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Var "bb"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set  "("  ($#k3_sfmastr3 :::"FinSeqMin"::: )   "(" (Set (Var "f")) "," (Set (Var "aa")) "," (Set (Var "bb")) "," (Set (Var "c")) ")"  ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_graph_2 :::"min_at"::: )   "(" (Set  "(" (Set (Var "s"))  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")) ")" ) "," (Set  "("  ($#k1_int_2 :::"abs"::: )  (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "aa")) ")" ) ")" ) "," (Set  "("  ($#k1_int_2 :::"abs"::: )  (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "bb")) ")" ) ")" ) ")" ))))))) ; 
 begin  definitionlet "f" be    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )  ; let "a", "b" be   ($#m1_subset_1 :::"Int-Location":::); func  :::"swap":::  "(" "f" "," "a" "," "b" ")"  ->   ($#m1_hidden :::"Program":::) "of"  equals :: SFMASTR3:def 5 (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  ($#k5_scmfsa_m :::"{"::: ) "a" "," "b" ($#k5_scmfsa_m :::"}"::: ) ) ")" )  ($#k14_scmfsa_2 :::":="::: )   "(" "f" "," "a" ")"  ")" )  ($#k6_scmfsa6a :::"";""::: )  (Set  "(" (Set  "(" (Num 2)  ($#k9_scmfsa_m :::"-ndRWNotIn"::: )  (Set  ($#k5_scmfsa_m :::"{"::: ) "a" "," "b" ($#k5_scmfsa_m :::"}"::: ) ) ")" )  ($#k14_scmfsa_2 :::":="::: )   "(" "f" "," "b" ")"  ")" ) ")" )  ($#k5_scmfsa6a :::"";""::: )  (Set  "("  "(" "f" "," "a" ")"   ($#k15_scmfsa_2 :::":="::: )  (Set  "(" (Num 2)  ($#k9_scmfsa_m :::"-ndRWNotIn"::: )  (Set  ($#k5_scmfsa_m :::"{"::: ) "a" "," "b" ($#k5_scmfsa_m :::"}"::: ) ) ")" ) ")" ) ")" )  ($#k5_scmfsa6a :::"";""::: )  (Set  "("  "(" "f" "," "b" ")"   ($#k15_scmfsa_2 :::":="::: )  (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  ($#k5_scmfsa_m :::"{"::: ) "a" "," "b" ($#k5_scmfsa_m :::"}"::: ) ) ")" ) ")" )); end; 







:: deftheorem    defines :::"swap"::: SFMASTR3:def 5 :  (Bool  "for" (Set (Var "f")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Int-Location":::) "holds"  (Bool (Set   ($#k4_sfmastr3 :::"swap"::: )   "(" (Set (Var "f")) "," (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  ($#k5_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k5_scmfsa_m :::"}"::: ) ) ")" )  ($#k14_scmfsa_2 :::":="::: )   "(" (Set (Var "f")) "," (Set (Var "a")) ")"  ")" )  ($#k6_scmfsa6a :::"";""::: )  (Set  "(" (Set  "(" (Num 2)  ($#k9_scmfsa_m :::"-ndRWNotIn"::: )  (Set  ($#k5_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k5_scmfsa_m :::"}"::: ) ) ")" )  ($#k14_scmfsa_2 :::":="::: )   "(" (Set (Var "f")) "," (Set (Var "b")) ")"  ")" ) ")" )  ($#k5_scmfsa6a :::"";""::: )  (Set  "("  "(" (Set (Var "f")) "," (Set (Var "a")) ")"   ($#k15_scmfsa_2 :::":="::: )  (Set  "(" (Num 2)  ($#k9_scmfsa_m :::"-ndRWNotIn"::: )  (Set  ($#k5_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k5_scmfsa_m :::"}"::: ) ) ")" ) ")" ) ")" )  ($#k5_scmfsa6a :::"";""::: )  (Set  "("  "(" (Set (Var "f")) "," (Set (Var "b")) ")"   ($#k15_scmfsa_2 :::":="::: )  (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  ($#k5_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k5_scmfsa_m :::"}"::: ) ) ")" ) ")" ))))); 
 registrationlet "f" be    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )  ; let "a", "b" be   ($#m1_subset_1 :::"Int-Location":::); 
cluster (Set   ($#k4_sfmastr3 :::"swap"::: )   "(" "f" "," "a" "," "b" ")" ) ->   ($#v1_scmfsa7b :::"good"::: )     ($#v7_amistd_1 :::"parahalting"::: )   ; 
end; 
theorem :: SFMASTR3:32 (Bool  "for" (Set (Var "cc")) "," (Set (Var "aa")) "," (Set (Var "bb")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )    "st" (Bool (Bool (Set (Var "cc"))  ($#r1_hidden :::"<>"::: )  (Set (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  ($#k5_scmfsa_m :::"{"::: ) (Set (Var "aa")) "," (Set (Var "bb")) ($#k5_scmfsa_m :::"}"::: ) ))) & (Bool (Set (Var "cc"))  ($#r1_hidden :::"<>"::: )  (Set (Num 2)  ($#k9_scmfsa_m :::"-ndRWNotIn"::: )  (Set  ($#k5_scmfsa_m :::"{"::: ) (Set (Var "aa")) "," (Set (Var "bb")) ($#k5_scmfsa_m :::"}"::: ) )))) "holds"  (Bool  "not" (Bool (Set   ($#k4_sfmastr3 :::"swap"::: )   "(" (Set (Var "f")) "," (Set (Var "aa")) "," (Set (Var "bb")) ")" )  ($#r4_scmfsa7b :::"destroys"::: )  (Set (Var "cc")))))) ; 
 
theorem :: SFMASTR3:33 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "aa")) "," (Set (Var "bb")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "aa")))) & (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "aa")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set (Var "s"))  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")) ")" ))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "bb")))) & (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "bb")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set (Var "s"))  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set  "("  ($#k4_sfmastr3 :::"swap"::: )   "(" (Set (Var "f")) "," (Set (Var "aa")) "," (Set (Var "bb")) ")"  ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "s"))  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")) ")" )  ($#k2_funct_7 :::"+*"::: )   "(" (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "aa")) ")" ) "," (Set  "(" (Set  "(" (Set (Var "s"))  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "bb")) ")" ) ")" ) ")"  ")" )  ($#k2_funct_7 :::"+*"::: )   "(" (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "bb")) ")" ) "," (Set  "(" (Set  "(" (Set (Var "s"))  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "aa")) ")" ) ")" ) ")" )))))) ; 
 
theorem :: SFMASTR3:34 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "aa")) "," (Set (Var "bb")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "aa")))) & (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "aa")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set (Var "s"))  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")) ")" ))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "bb")))) & (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "bb")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set (Var "s"))  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set  "("  ($#k4_sfmastr3 :::"swap"::: )   "(" (Set (Var "f")) "," (Set (Var "aa")) "," (Set (Var "bb")) ")"  ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "aa")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "s"))  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "bb")) ")" ))) & (Bool (Set (Set  "(" (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set  "("  ($#k4_sfmastr3 :::"swap"::: )   "(" (Set (Var "f")) "," (Set (Var "aa")) "," (Set (Var "bb")) ")"  ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "bb")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "s"))  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "aa")) ")" )))  ")" ))))) ; 
 
theorem :: SFMASTR3:35 (Bool  "for" (Set (Var "aa")) "," (Set (Var "bb")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )   "holds"  (Bool (Set  ($#k5_scmfsa_m :::"{"::: ) (Set (Var "aa")) "," (Set (Var "bb")) ($#k5_scmfsa_m :::"}"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set  "("  ($#k4_sfmastr3 :::"swap"::: )   "(" (Set (Var "f")) "," (Set (Var "aa")) "," (Set (Var "bb")) ")"  ")" ))))) ; 
 
theorem :: SFMASTR3:36 (Bool  "for" (Set (Var "aa")) "," (Set (Var "bb")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )   "holds"  (Bool (Set   ($#k4_sf_mastr :::"UsedInt*Loc"::: )  (Set  "("  ($#k4_sfmastr3 :::"swap"::: )   "(" (Set (Var "f")) "," (Set (Var "aa")) "," (Set (Var "bb")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) )))) ; 
 begin  definitionlet "f" be    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )  ; func  :::"Selection-sort"::: "f" ->   ($#m1_hidden :::"Program":::) "of"  equals :: SFMASTR3:def 6 (Set (Set  "(" (Set  "(" (Num 1)  ($#k1_sfmastr1 :::"-stNotUsed"::: )  (Set  "("  ($#k4_sfmastr3 :::"swap"::: )   "(" "f" "," (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "("  ($#k1_subset_1 :::"{}"::: )  (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) ")" ) ")" ) "," (Set  "(" (Num 2)  ($#k9_scmfsa_m :::"-ndRWNotIn"::: )  (Set  "("  ($#k1_subset_1 :::"{}"::: )  (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) ")" ) ")" ) ")"  ")" ) ")" )  ($#k16_scmfsa_2 :::":=len"::: )  "f" ")" )  ($#k4_scmfsa6a :::"";""::: )  (Set  "("  ($#k2_sfmastr3 :::"for-up"::: )   "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "("  ($#k1_subset_1 :::"{}"::: )  (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) ")" ) ")" ) "," (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set  "(" (Num 1)  ($#k1_sfmastr1 :::"-stNotUsed"::: )  (Set  "("  ($#k4_sfmastr3 :::"swap"::: )   "(" "f" "," (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "("  ($#k1_subset_1 :::"{}"::: )  (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) ")" ) ")" ) "," (Set  "(" (Num 2)  ($#k9_scmfsa_m :::"-ndRWNotIn"::: )  (Set  "("  ($#k1_subset_1 :::"{}"::: )  (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) ")" ) ")" ) ")"  ")" ) ")" ) "," (Set  "(" (Set  "("  ($#k3_sfmastr3 :::"FinSeqMin"::: )   "(" "f" "," (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "("  ($#k1_subset_1 :::"{}"::: )  (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) ")" ) ")" ) "," (Set  "(" (Num 1)  ($#k1_sfmastr1 :::"-stNotUsed"::: )  (Set  "("  ($#k4_sfmastr3 :::"swap"::: )   "(" "f" "," (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "("  ($#k1_subset_1 :::"{}"::: )  (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) ")" ) ")" ) "," (Set  "(" (Num 2)  ($#k9_scmfsa_m :::"-ndRWNotIn"::: )  (Set  "("  ($#k1_subset_1 :::"{}"::: )  (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) ")" ) ")" ) ")"  ")" ) ")" ) "," (Set  "(" (Num 2)  ($#k9_scmfsa_m :::"-ndRWNotIn"::: )  (Set  "("  ($#k1_subset_1 :::"{}"::: )  (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) ")" ) ")" ) ")"  ")" )  ($#k3_scmfsa6a :::"";""::: )  (Set  "("  ($#k4_sfmastr3 :::"swap"::: )   "(" "f" "," (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "("  ($#k1_subset_1 :::"{}"::: )  (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) ")" ) ")" ) "," (Set  "(" (Num 2)  ($#k9_scmfsa_m :::"-ndRWNotIn"::: )  (Set  "("  ($#k1_subset_1 :::"{}"::: )  (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) ")" ) ")" ) ")"  ")" ) ")" ) ")"  ")" )); end; 





:: deftheorem    defines :::"Selection-sort"::: SFMASTR3:def 6 :  (Bool  "for" (Set (Var "f")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )   "holds"  (Bool (Set   ($#k5_sfmastr3 :::"Selection-sort"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 1)  ($#k1_sfmastr1 :::"-stNotUsed"::: )  (Set  "("  ($#k4_sfmastr3 :::"swap"::: )   "(" (Set (Var "f")) "," (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "("  ($#k1_subset_1 :::"{}"::: )  (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) ")" ) ")" ) "," (Set  "(" (Num 2)  ($#k9_scmfsa_m :::"-ndRWNotIn"::: )  (Set  "("  ($#k1_subset_1 :::"{}"::: )  (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) ")" ) ")" ) ")"  ")" ) ")" )  ($#k16_scmfsa_2 :::":=len"::: )  (Set (Var "f")) ")" )  ($#k4_scmfsa6a :::"";""::: )  (Set  "("  ($#k2_sfmastr3 :::"for-up"::: )   "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "("  ($#k1_subset_1 :::"{}"::: )  (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) ")" ) ")" ) "," (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set  "(" (Num 1)  ($#k1_sfmastr1 :::"-stNotUsed"::: )  (Set  "("  ($#k4_sfmastr3 :::"swap"::: )   "(" (Set (Var "f")) "," (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "("  ($#k1_subset_1 :::"{}"::: )  (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) ")" ) ")" ) "," (Set  "(" (Num 2)  ($#k9_scmfsa_m :::"-ndRWNotIn"::: )  (Set  "("  ($#k1_subset_1 :::"{}"::: )  (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) ")" ) ")" ) ")"  ")" ) ")" ) "," (Set  "(" (Set  "("  ($#k3_sfmastr3 :::"FinSeqMin"::: )   "(" (Set (Var "f")) "," (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "("  ($#k1_subset_1 :::"{}"::: )  (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) ")" ) ")" ) "," (Set  "(" (Num 1)  ($#k1_sfmastr1 :::"-stNotUsed"::: )  (Set  "("  ($#k4_sfmastr3 :::"swap"::: )   "(" (Set (Var "f")) "," (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "("  ($#k1_subset_1 :::"{}"::: )  (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) ")" ) ")" ) "," (Set  "(" (Num 2)  ($#k9_scmfsa_m :::"-ndRWNotIn"::: )  (Set  "("  ($#k1_subset_1 :::"{}"::: )  (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) ")" ) ")" ) ")"  ")" ) ")" ) "," (Set  "(" (Num 2)  ($#k9_scmfsa_m :::"-ndRWNotIn"::: )  (Set  "("  ($#k1_subset_1 :::"{}"::: )  (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) ")" ) ")" ) ")"  ")" )  ($#k3_scmfsa6a :::"";""::: )  (Set  "("  ($#k4_sfmastr3 :::"swap"::: )   "(" (Set (Var "f")) "," (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  "("  ($#k1_subset_1 :::"{}"::: )  (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) ")" ) ")" ) "," (Set  "(" (Num 2)  ($#k9_scmfsa_m :::"-ndRWNotIn"::: )  (Set  "("  ($#k1_subset_1 :::"{}"::: )  (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) ")" ) ")" ) ")"  ")" ) ")" ) ")"  ")" )))); 
 
theorem :: SFMASTR3:37 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "f")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "S")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "S"))  ($#r6_pboole :::"="::: )  (Set   ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set  "("  ($#k5_sfmastr3 :::"Selection-sort"::: )  (Set (Var "f")) ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ))) "holds"  (Bool  "("  (Bool (Set (Set (Var "S"))  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")))  ($#r3_graph_2 :::"is_non_decreasing_on"::: )  (Num 1) "," (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set (Var "S"))  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")) ")" ))) & (Bool  "ex" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "("  ($#k4_finseq_1 :::"dom"::: )  (Set  "(" (Set (Var "s"))  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")) ")" ) ")" ) "st" (Bool (Set (Set (Var "S"))  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "s"))  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "p")))))  ")" ))))) ;