:: SCMFSA9A  semantic presentation begin  

















theorem :: SCMFSA9A:1 (Bool  "for" (Set (Var "l")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool (Set   ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set  "(" (Set (Var "l"))  ($#k16_funcop_1 :::".-->"::: )  (Set (Var "i")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "i")))))) ; 
 
theorem :: SCMFSA9A:2 (Bool  "for" (Set (Var "l")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool (Set   ($#k4_sf_mastr :::"UsedInt*Loc"::: )  (Set  "(" (Set (Var "l"))  ($#k16_funcop_1 :::".-->"::: )  (Set (Var "i")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_sf_mastr :::"UsedInt*Loc"::: )  (Set (Var "i")))))) ; 
 
theorem :: SCMFSA9A:3 (Bool (Set   ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set  "("  ($#k4_compos_1 :::"Stop"::: )  (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) ; 
 
theorem :: SCMFSA9A:4 (Bool (Set   ($#k4_sf_mastr :::"UsedInt*Loc"::: )  (Set  "("  ($#k4_compos_1 :::"Stop"::: )  (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) ; 
 
theorem :: SCMFSA9A:5 (Bool  "for" (Set (Var "l")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set  "("  ($#k1_scmfsa8a :::"Goto"::: )  (Set (Var "l")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: SCMFSA9A:6 (Bool  "for" (Set (Var "l")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k4_sf_mastr :::"UsedInt*Loc"::: )  (Set  "("  ($#k1_scmfsa8a :::"Goto"::: )  (Set (Var "l")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 

























theorem :: SCMFSA9A:7 (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "," (Set (Var "J")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool (Set   ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set  "("  ($#k1_scmfsa8b :::"if=0"::: )   "(" (Set (Var "b")) "," (Set (Var "I")) "," (Set (Var "J")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k4_scmfsa_m :::"{"::: ) (Set (Var "b")) ($#k4_scmfsa_m :::"}"::: ) )  ($#k1_finsub_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "I")) ")" ) ")" )  ($#k1_finsub_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "J")) ")" ))))) ; 
 
theorem :: SCMFSA9A:8 (Bool  "for" (Set (Var "I")) "," (Set (Var "J")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Int-Location":::) "holds"  (Bool (Set   ($#k4_sf_mastr :::"UsedInt*Loc"::: )  (Set  "("  ($#k1_scmfsa8b :::"if=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_sf_mastr :::"UsedInt*Loc"::: )  (Set (Var "I")) ")" )  ($#k1_finsub_1 :::"\/"::: )  (Set  "("  ($#k4_sf_mastr :::"UsedInt*Loc"::: )  (Set (Var "J")) ")" ))))) ; 
 
theorem :: SCMFSA9A:9 (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "," (Set (Var "J")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool (Set   ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set  "("  ($#k2_scmfsa8b :::"if>0"::: )   "(" (Set (Var "b")) "," (Set (Var "I")) "," (Set (Var "J")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k4_scmfsa_m :::"{"::: ) (Set (Var "b")) ($#k4_scmfsa_m :::"}"::: ) )  ($#k1_finsub_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "I")) ")" ) ")" )  ($#k1_finsub_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "J")) ")" ))))) ; 
 
theorem :: SCMFSA9A:10 (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "," (Set (Var "J")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool (Set   ($#k4_sf_mastr :::"UsedInt*Loc"::: )  (Set  "("  ($#k2_scmfsa8b :::"if>0"::: )   "(" (Set (Var "b")) "," (Set (Var "I")) "," (Set (Var "J")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_sf_mastr :::"UsedInt*Loc"::: )  (Set (Var "I")) ")" )  ($#k1_finsub_1 :::"\/"::: )  (Set  "("  ($#k4_sf_mastr :::"UsedInt*Loc"::: )  (Set (Var "J")) ")" ))))) ; 
 begin  
theorem :: SCMFSA9A:11 (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool (Set   ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set  "("  ($#k1_scmfsa_9 :::"while=0"::: )   "(" (Set (Var "b")) "," (Set (Var "I")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k4_scmfsa_m :::"{"::: ) (Set (Var "b")) ($#k4_scmfsa_m :::"}"::: ) )  ($#k1_finsub_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "I")) ")" ))))) ; 
 
theorem :: SCMFSA9A:12 (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool (Set   ($#k4_sf_mastr :::"UsedInt*Loc"::: )  (Set  "("  ($#k1_scmfsa_9 :::"while=0"::: )   "(" (Set (Var "b")) "," (Set (Var "I")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_sf_mastr :::"UsedInt*Loc"::: )  (Set (Var "I")))))) ; 
 definitionlet "p" be   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "s" be   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "a" be   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::); let "I" be   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); pred  :::"ProperBodyWhile=0"::: "a" "," "I" "," "s" "," "p" means :: SCMFSA9A:def 1 (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Set  "(" (Set  "("  ($#k4_scmfsa_9 :::"StepWhile=0"::: )   "(" "a" "," "I" "," "p" "," "s" ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k1_funct_1 :::"."::: )  "a")  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool "I"  ($#r5_scmfsa7b :::"is_closed_on"::: )  (Set (Set  "("  ($#k4_scmfsa_9 :::"StepWhile=0"::: )   "(" "a" "," "I" "," "p" "," "s" ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k"))) "," (Set "p"  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k1_scmfsa_9 :::"while=0"::: )   "(" "a" "," "I" ")"  ")" ))) & (Bool "I"  ($#r6_scmfsa7b :::"is_halting_on"::: )  (Set (Set  "("  ($#k4_scmfsa_9 :::"StepWhile=0"::: )   "(" "a" "," "I" "," "p" "," "s" ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k"))) "," (Set "p"  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k1_scmfsa_9 :::"while=0"::: )   "(" "a" "," "I" ")"  ")" )))  ")" )); pred  :::"WithVariantWhile=0"::: "a" "," "I" "," "s" "," "p" means :: SCMFSA9A:def 2 (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k4_card_3 :::"product"::: )  (Set  "("  ($#k2_memstr_0 :::"the_Values_of"::: )  (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ) "," (Set  ($#k5_numbers :::"NAT"::: ) ) "st"  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set  "("  ($#k4_scmfsa_9 :::"StepWhile=0"::: )   "(" "a" "," "I" "," "p" "," "s" ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set  "("  ($#k4_scmfsa_9 :::"StepWhile=0"::: )   "(" "a" "," "I" "," "p" "," "s" ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" ))) "or" (Bool (Set (Set  "(" (Set  "("  ($#k4_scmfsa_9 :::"StepWhile=0"::: )   "(" "a" "," "I" "," "p" "," "s" ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k1_funct_1 :::"."::: )  "a")  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ))); end; 














:: deftheorem    defines :::"ProperBodyWhile=0"::: SCMFSA9A:def 1 :  (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"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"   (Bool  "("  (Bool   ($#r1_scmfsa9a :::"ProperBodyWhile=0"::: )  (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "s")) "," (Set (Var "p"))) "iff" (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Set  "(" (Set  "("  ($#k4_scmfsa_9 :::"StepWhile=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Var "I"))  ($#r5_scmfsa7b :::"is_closed_on"::: )  (Set (Set  "("  ($#k4_scmfsa_9 :::"StepWhile=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k"))) "," (Set (Set (Var "p"))  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k1_scmfsa_9 :::"while=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) ")"  ")" ))) & (Bool (Set (Var "I"))  ($#r6_scmfsa7b :::"is_halting_on"::: )  (Set (Set  "("  ($#k4_scmfsa_9 :::"StepWhile=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k"))) "," (Set (Set (Var "p"))  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k1_scmfsa_9 :::"while=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) ")"  ")" )))  ")" ))  ")" ))))); 
 
:: deftheorem    defines :::"WithVariantWhile=0"::: SCMFSA9A:def 2 :  (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"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"   (Bool  "("  (Bool   ($#r2_scmfsa9a :::"WithVariantWhile=0"::: )  (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "s")) "," (Set (Var "p"))) "iff" (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k4_card_3 :::"product"::: )  (Set  "("  ($#k2_memstr_0 :::"the_Values_of"::: )  (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ) "," (Set  ($#k5_numbers :::"NAT"::: ) ) "st"  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set  "("  ($#k4_scmfsa_9 :::"StepWhile=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set  "("  ($#k4_scmfsa_9 :::"StepWhile=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" ))) "or" (Bool (Set (Set  "(" (Set  "("  ($#k4_scmfsa_9 :::"StepWhile=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )))  ")" ))))); 
 
theorem :: SCMFSA9A:13 (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"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#v7_amistd_1 :::"parahalting"::: )    ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool   ($#r1_scmfsa9a :::"ProperBodyWhile=0"::: )  (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "s")) "," (Set (Var "p"))))))) ; 
 
theorem :: SCMFSA9A:14 (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"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool   ($#r1_scmfsa9a :::"ProperBodyWhile=0"::: )  (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "s")) "," (Set (Var "p"))) & (Bool   ($#r2_scmfsa9a :::"WithVariantWhile=0"::: )  (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "s")) "," (Set (Var "p")))) "holds"  (Bool  "("  (Bool (Set   ($#k1_scmfsa_9 :::"while=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) ")" )  ($#r6_scmfsa7b :::"is_halting_on"::: )  (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set   ($#k1_scmfsa_9 :::"while=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) ")" )  ($#r5_scmfsa7b :::"is_closed_on"::: )  (Set (Var "s")) "," (Set (Var "p")))  ")" ))))) ; 
 
theorem :: SCMFSA9A:15 (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"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#v7_amistd_1 :::"parahalting"::: )    ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool   ($#r2_scmfsa9a :::"WithVariantWhile=0"::: )  (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "s")) "," (Set (Var "p")))) "holds"  (Bool  "("  (Bool (Set   ($#k1_scmfsa_9 :::"while=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) ")" )  ($#r6_scmfsa7b :::"is_halting_on"::: )  (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set   ($#k1_scmfsa_9 :::"while=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) ")" )  ($#r5_scmfsa7b :::"is_closed_on"::: )  (Set (Var "s")) "," (Set (Var "p")))  ")" ))))) ; 
 
theorem :: SCMFSA9A:16 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "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 "I")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "s")) "being" (Set   ($#k6_numbers :::"0"::: )  )  ($#v5_memstr_0 :::"-started"::: )    ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set   ($#k1_scmfsa_9 :::"while=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Var "p"))) & (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set   ($#k8_extpro_1 :::"LifeSpan"::: )   "(" (Set (Var "p")) "," (Set (Var "s")) ")" )  ($#r1_hidden :::"="::: )  (Num 4)) & (Bool  "("   "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set (Var "k")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set (Var "s"))))  ")" )  ")" ))))) ; 
 
theorem :: SCMFSA9A:17 (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"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "I"))  ($#r5_scmfsa7b :::"is_closed_on"::: )  (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set (Var "I"))  ($#r6_scmfsa7b :::"is_halting_on"::: )  (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set  "(" (Set (Var "p"))  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k1_scmfsa_9 :::"while=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) ")"  ")" ) ")" ) "," (Set  "("  ($#k8_memstr_0 :::"Initialize"::: )  (Set (Var "s")) ")" ) "," (Set  "(" (Set  "("  ($#k8_extpro_1 :::"LifeSpan"::: )   "(" (Set  "(" (Set (Var "p"))  ($#k1_funct_4 :::"+*"::: )  (Set (Var "I")) ")" ) "," (Set  "("  ($#k8_memstr_0 :::"Initialize"::: )  (Set (Var "s")) ")" ) ")"  ")" )  ($#k2_nat_1 :::"+"::: )  (Num 3) ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set  "(" (Set (Var "p"))  ($#k1_funct_4 :::"+*"::: )  (Set (Var "I")) ")" ) "," (Set  "("  ($#k8_memstr_0 :::"Initialize"::: )  (Set (Var "s")) ")" ) "," (Set  "("  ($#k8_extpro_1 :::"LifeSpan"::: )   "(" (Set  "(" (Set (Var "p"))  ($#k1_funct_4 :::"+*"::: )  (Set (Var "I")) ")" ) "," (Set  "("  ($#k8_memstr_0 :::"Initialize"::: )  (Set (Var "s")) ")" ) ")"  ")" ) ")"  ")" ))))))) ; 
 
theorem :: SCMFSA9A:18 (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"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Set  "(" (Set  "("  ($#k4_scmfsa_9 :::"StepWhile=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "(" (Set  "("  ($#k4_scmfsa_9 :::"StepWhile=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "(" (Set  "("  ($#k4_scmfsa_9 :::"StepWhile=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )))))))) ; 
 
theorem :: SCMFSA9A:19 (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"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool  "("  (Bool  "("  (Bool (Set (Var "I"))  ($#r6_scmfsa7b :::"is_halting_on"::: )  (Set   ($#k1_scmfsa_m :::"Initialized"::: )  (Set  "(" (Set  "("  ($#k4_scmfsa_9 :::"StepWhile=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )) "," (Set (Set (Var "p"))  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k1_scmfsa_9 :::"while=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) ")"  ")" ))) & (Bool (Set (Var "I"))  ($#r5_scmfsa7b :::"is_closed_on"::: )  (Set   ($#k1_scmfsa_m :::"Initialized"::: )  (Set  "(" (Set  "("  ($#k4_scmfsa_9 :::"StepWhile=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )) "," (Set (Set (Var "p"))  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k1_scmfsa_9 :::"while=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) ")"  ")" )))  ")" ) "or" (Bool (Set (Var "I")) "is"   ($#v7_amistd_1 :::"parahalting"::: )  )  ")" ) & (Bool (Set (Set  "(" (Set  "("  ($#k4_scmfsa_9 :::"StepWhile=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set  "(" (Set  "("  ($#k4_scmfsa_9 :::"StepWhile=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (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))) "holds"  (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "(" (Set  "("  ($#k4_scmfsa_9 :::"StepWhile=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set (Var "I")) "," (Set  "(" (Set (Var "p"))  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k1_scmfsa_9 :::"while=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) ")"  ")" ) ")" ) "," (Set  "(" (Set  "("  ($#k4_scmfsa_9 :::"StepWhile=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" ) ")"  ")" )))))))) ; 
 
theorem :: SCMFSA9A:20 (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"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "Ig")) "being"   ($#v1_scmfsa7b :::"good"::: )    ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool  "("  (Bool   ($#r1_scmfsa9a :::"ProperBodyWhile=0"::: )  (Set (Var "a")) "," (Set (Var "Ig")) "," (Set (Var "s")) "," (Set (Var "p"))) "or" (Bool (Set (Var "Ig")) "is"   ($#v7_amistd_1 :::"parahalting"::: )  )  ")" ) & (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 "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k4_scmfsa_9 :::"StepWhile=0"::: )   "(" (Set (Var "a")) "," (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))))))) ; 
 
theorem :: SCMFSA9A:21 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "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"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool   ($#r1_scmfsa9a :::"ProperBodyWhile=0"::: )  (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "s1")) "," (Set (Var "p1"))) & (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set (Var "s1")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set (Var "s2"))))) "holds"  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "(" (Set  "("  ($#k4_scmfsa_9 :::"StepWhile=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p1")) "," (Set (Var "s1")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "(" (Set  "("  ($#k4_scmfsa_9 :::"StepWhile=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p2")) "," (Set (Var "s2")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )))))))) ; 
 definitionlet "p" be   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "s" be   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "a" be   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::); let "I" be   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); assume that  
(Bool  "("  (Bool   ($#r1_scmfsa9a :::"ProperBodyWhile=0"::: )  (Set (Const "a")) "," (Set (Const "I")) "," (Set (Const "s")) "," (Set (Const "p"))) "or" (Bool (Set (Const "I")) "is"   ($#v7_amistd_1 :::"parahalting"::: )  )  ")" )
 and  
(Bool   ($#r2_scmfsa9a :::"WithVariantWhile=0"::: )  (Set (Const "a")) "," (Set (Const "I")) "," (Set (Const "s")) "," (Set (Const "p")))
 ; func  :::"ExitsAtWhile=0":::  "(" "a" "," "I" "," "p" "," "s" ")"  ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) means :: SCMFSA9A:def 3 (Bool  "ex" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool it  ($#r1_hidden :::"="::: )  (Set (Var "k"))) & (Bool (Set (Set  "(" (Set  "("  ($#k4_scmfsa_9 :::"StepWhile=0"::: )   "(" "a" "," "I" "," "p" "," "s" ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k1_funct_1 :::"."::: )  "a")  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Set  "(" (Set  "("  ($#k4_scmfsa_9 :::"StepWhile=0"::: )   "(" "a" "," "I" "," "p" "," "s" ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k1_funct_1 :::"."::: )  "a")  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i")))  ")" ) & (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set  "(" "p"  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k1_scmfsa_9 :::"while=0"::: )   "(" "a" "," "I" ")"  ")" ) ")" ) "," (Set  "("  ($#k8_memstr_0 :::"Initialize"::: )  "s" ")" ) "," (Set  "("  ($#k8_extpro_1 :::"LifeSpan"::: )   "(" (Set  "(" "p"  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k1_scmfsa_9 :::"while=0"::: )   "(" "a" "," "I" ")"  ")" ) ")" ) "," (Set  "("  ($#k8_memstr_0 :::"Initialize"::: )  "s" ")" ) ")"  ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "(" (Set  "("  ($#k4_scmfsa_9 :::"StepWhile=0"::: )   "(" "a" "," "I" "," "p" "," "s" ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )))  ")" )); end; 









:: deftheorem    defines :::"ExitsAtWhile=0"::: SCMFSA9A:def 3 :  (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"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool  "("  (Bool   ($#r1_scmfsa9a :::"ProperBodyWhile=0"::: )  (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "s")) "," (Set (Var "p"))) "or" (Bool (Set (Var "I")) "is"   ($#v7_amistd_1 :::"parahalting"::: )  )  ")" ) & (Bool   ($#r2_scmfsa9a :::"WithVariantWhile=0"::: )  (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "s")) "," (Set (Var "p")))) "holds"  (Bool  "for" (Set (Var "b5")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_scmfsa9a :::"ExitsAtWhile=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" )) "iff" (Bool  "ex" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set (Var "k"))) & (Bool (Set (Set  "(" (Set  "("  ($#k4_scmfsa_9 :::"StepWhile=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Set  "(" (Set  "("  ($#k4_scmfsa_9 :::"StepWhile=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i")))  ")" ) & (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set  "(" (Set (Var "p"))  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k1_scmfsa_9 :::"while=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) ")"  ")" ) ")" ) "," (Set  "("  ($#k8_memstr_0 :::"Initialize"::: )  (Set (Var "s")) ")" ) "," (Set  "("  ($#k8_extpro_1 :::"LifeSpan"::: )   "(" (Set  "(" (Set (Var "p"))  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k1_scmfsa_9 :::"while=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) ")"  ")" ) ")" ) "," (Set  "("  ($#k8_memstr_0 :::"Initialize"::: )  (Set (Var "s")) ")" ) ")"  ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "(" (Set  "("  ($#k4_scmfsa_9 :::"StepWhile=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )))  ")" ))  ")" )))))); 
 
theorem :: SCMFSA9A:22 (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"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "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 "a")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set  "("  ($#k1_scmfsa_9 :::"while=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) ")"  ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set (Var "s")))))))) ; 
 
theorem :: SCMFSA9A:23 (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"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool  "("  (Bool   ($#r1_scmfsa9a :::"ProperBodyWhile=0"::: )  (Set (Var "a")) "," (Set (Var "I")) "," (Set   ($#k1_scmfsa_m :::"Initialized"::: )  (Set (Var "s"))) "," (Set (Var "p"))) "or" (Bool (Set (Var "I")) "is"   ($#v7_amistd_1 :::"parahalting"::: )  )  ")" ) & (Bool   ($#r2_scmfsa9a :::"WithVariantWhile=0"::: )  (Set (Var "a")) "," (Set (Var "I")) "," (Set   ($#k1_scmfsa_m :::"Initialized"::: )  (Set (Var "s"))) "," (Set (Var "p")))) "holds"  (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set  "("  ($#k1_scmfsa_9 :::"while=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) ")"  ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "(" (Set  "("  ($#k4_scmfsa_9 :::"StepWhile=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set  "("  ($#k1_scmfsa_m :::"Initialized"::: )  (Set (Var "s")) ")" ) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set  "("  ($#k1_scmfsa9a :::"ExitsAtWhile=0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set  "("  ($#k1_scmfsa_m :::"Initialized"::: )  (Set (Var "s")) ")" ) ")"  ")" ) ")" ))))))) ; 
 begin  
theorem :: SCMFSA9A:24 (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool (Set   ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set  "("  ($#k2_scmfsa_9 :::"while>0"::: )   "(" (Set (Var "b")) "," (Set (Var "I")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k4_scmfsa_m :::"{"::: ) (Set (Var "b")) ($#k4_scmfsa_m :::"}"::: ) )  ($#k1_finsub_1 :::"\/"::: )  (Set  "("  ($#k2_sf_mastr :::"UsedIntLoc"::: )  (Set (Var "I")) ")" ))))) ; 
 
theorem :: SCMFSA9A:25 (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool (Set   ($#k4_sf_mastr :::"UsedInt*Loc"::: )  (Set  "("  ($#k2_scmfsa_9 :::"while>0"::: )   "(" (Set (Var "b")) "," (Set (Var "I")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_sf_mastr :::"UsedInt*Loc"::: )  (Set (Var "I")))))) ; 
 definitionlet "p" be   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "s" be   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "a" be   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::); let "I" be   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); pred  :::"ProperBodyWhile>0"::: "a" "," "I" "," "s" "," "p" means :: SCMFSA9A:def 4 (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" "a" "," "I" "," "p" "," "s" ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k1_funct_1 :::"."::: )  "a")  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool "I"  ($#r5_scmfsa7b :::"is_closed_on"::: )  (Set (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" "a" "," "I" "," "p" "," "s" ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k"))) "," (Set "p"  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k2_scmfsa_9 :::"while>0"::: )   "(" "a" "," "I" ")"  ")" ))) & (Bool "I"  ($#r6_scmfsa7b :::"is_halting_on"::: )  (Set (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" "a" "," "I" "," "p" "," "s" ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k"))) "," (Set "p"  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k2_scmfsa_9 :::"while>0"::: )   "(" "a" "," "I" ")"  ")" )))  ")" )); pred  :::"WithVariantWhile>0"::: "a" "," "I" "," "s" "," "p" means :: SCMFSA9A:def 5 (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k4_card_3 :::"product"::: )  (Set  "("  ($#k2_memstr_0 :::"the_Values_of"::: )  (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ) "," (Set  ($#k5_numbers :::"NAT"::: ) ) "st"  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" "a" "," "I" "," "p" "," "s" ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" "a" "," "I" "," "p" "," "s" ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" ))) "or" (Bool (Set (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" "a" "," "I" "," "p" "," "s" ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k1_funct_1 :::"."::: )  "a")  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ))); end; 














:: deftheorem    defines :::"ProperBodyWhile>0"::: SCMFSA9A:def 4 :  (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"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"   (Bool  "("  (Bool   ($#r3_scmfsa9a :::"ProperBodyWhile>0"::: )  (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "s")) "," (Set (Var "p"))) "iff" (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Var "I"))  ($#r5_scmfsa7b :::"is_closed_on"::: )  (Set (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (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 (Var "a")) "," (Set (Var "I")) ")"  ")" ))) & (Bool (Set (Var "I"))  ($#r6_scmfsa7b :::"is_halting_on"::: )  (Set (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (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 (Var "a")) "," (Set (Var "I")) ")"  ")" )))  ")" ))  ")" ))))); 
 
:: deftheorem    defines :::"WithVariantWhile>0"::: SCMFSA9A:def 5 :  (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"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"   (Bool  "("  (Bool   ($#r4_scmfsa9a :::"WithVariantWhile>0"::: )  (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "s")) "," (Set (Var "p"))) "iff" (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k4_card_3 :::"product"::: )  (Set  "("  ($#k2_memstr_0 :::"the_Values_of"::: )  (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ) "," (Set  ($#k5_numbers :::"NAT"::: ) ) "st"  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" ))) "or" (Bool (Set (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )))  ")" ))))); 
 
theorem :: SCMFSA9A:26 (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"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#v7_amistd_1 :::"parahalting"::: )    ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool   ($#r3_scmfsa9a :::"ProperBodyWhile>0"::: )  (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "s")) "," (Set (Var "p"))))))) ; 
 
theorem :: SCMFSA9A:27 (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"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool   ($#r3_scmfsa9a :::"ProperBodyWhile>0"::: )  (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "s")) "," (Set (Var "p"))) & (Bool   ($#r4_scmfsa9a :::"WithVariantWhile>0"::: )  (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "s")) "," (Set (Var "p")))) "holds"  (Bool  "("  (Bool (Set   ($#k2_scmfsa_9 :::"while>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) ")" )  ($#r6_scmfsa7b :::"is_halting_on"::: )  (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set   ($#k2_scmfsa_9 :::"while>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) ")" )  ($#r5_scmfsa7b :::"is_closed_on"::: )  (Set (Var "s")) "," (Set (Var "p")))  ")" ))))) ; 
 
theorem :: SCMFSA9A:28 (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"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#v7_amistd_1 :::"parahalting"::: )    ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool   ($#r4_scmfsa9a :::"WithVariantWhile>0"::: )  (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "s")) "," (Set (Var "p")))) "holds"  (Bool  "("  (Bool (Set   ($#k2_scmfsa_9 :::"while>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) ")" )  ($#r6_scmfsa7b :::"is_halting_on"::: )  (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set   ($#k2_scmfsa_9 :::"while>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) ")" )  ($#r5_scmfsa7b :::"is_closed_on"::: )  (Set (Var "s")) "," (Set (Var "p")))  ")" ))))) ; 
 
theorem :: SCMFSA9A:29 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "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 "I")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "s")) "being" (Set   ($#k6_numbers :::"0"::: )  )  ($#v5_memstr_0 :::"-started"::: )    ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set   ($#k2_scmfsa_9 :::"while>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Var "p"))) & (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set   ($#k8_extpro_1 :::"LifeSpan"::: )   "(" (Set (Var "p")) "," (Set (Var "s")) ")" )  ($#r1_hidden :::"="::: )  (Num 4)) & (Bool  "("   "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set (Var "k")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set (Var "s"))))  ")" )  ")" ))))) ; 
 
theorem :: SCMFSA9A:30 (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"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "I"))  ($#r5_scmfsa7b :::"is_closed_on"::: )  (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set (Var "I"))  ($#r6_scmfsa7b :::"is_halting_on"::: )  (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set  "(" (Set (Var "p"))  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k2_scmfsa_9 :::"while>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) ")"  ")" ) ")" ) "," (Set  "("  ($#k8_memstr_0 :::"Initialize"::: )  (Set (Var "s")) ")" ) "," (Set  "(" (Set  "("  ($#k8_extpro_1 :::"LifeSpan"::: )   "(" (Set  "(" (Set (Var "p"))  ($#k1_funct_4 :::"+*"::: )  (Set (Var "I")) ")" ) "," (Set  "("  ($#k8_memstr_0 :::"Initialize"::: )  (Set (Var "s")) ")" ) ")"  ")" )  ($#k2_nat_1 :::"+"::: )  (Num 3) ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set  "(" (Set (Var "p"))  ($#k1_funct_4 :::"+*"::: )  (Set (Var "I")) ")" ) "," (Set  "("  ($#k8_memstr_0 :::"Initialize"::: )  (Set (Var "s")) ")" ) "," (Set  "("  ($#k8_extpro_1 :::"LifeSpan"::: )   "(" (Set  "(" (Set (Var "p"))  ($#k1_funct_4 :::"+*"::: )  (Set (Var "I")) ")" ) "," (Set  "("  ($#k8_memstr_0 :::"Initialize"::: )  (Set (Var "s")) ")" ) ")"  ")" ) ")"  ")" ))))))) ; 
 
theorem :: SCMFSA9A:31 (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"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )))))))) ; 
 
theorem :: SCMFSA9A:32 (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"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool  "("  (Bool  "("  (Bool (Set (Var "I"))  ($#r6_scmfsa7b :::"is_halting_on"::: )  (Set   ($#k1_scmfsa_m :::"Initialized"::: )  (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (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 (Var "a")) "," (Set (Var "I")) ")"  ")" ))) & (Bool (Set (Var "I"))  ($#r5_scmfsa7b :::"is_closed_on"::: )  (Set   ($#k1_scmfsa_m :::"Initialized"::: )  (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (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 (Var "a")) "," (Set (Var "I")) ")"  ")" )))  ")" ) "or" (Bool (Set (Var "I")) "is"   ($#v7_amistd_1 :::"parahalting"::: )  )  ")" ) & (Bool (Set (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (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))) "holds"  (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set (Var "I")) "," (Set  "(" (Set (Var "p"))  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k2_scmfsa_9 :::"while>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) ")"  ")" ) ")" ) "," (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" ) ")"  ")" )))))))) ; 
 
theorem :: SCMFSA9A:33 (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"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "Ig")) "being"   ($#v1_scmfsa7b :::"good"::: )    ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool  "("  (Bool   ($#r3_scmfsa9a :::"ProperBodyWhile>0"::: )  (Set (Var "a")) "," (Set (Var "Ig")) "," (Set (Var "s")) "," (Set (Var "p"))) "or" (Bool (Set (Var "Ig")) "is"   ($#v7_amistd_1 :::"parahalting"::: )  )  ")" ) & (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 "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set (Var "a")) "," (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))))))) ; 
 
theorem :: SCMFSA9A:34 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "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"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool   ($#r3_scmfsa9a :::"ProperBodyWhile>0"::: )  (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "s1")) "," (Set (Var "p1"))) & (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set (Var "s1")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set (Var "s2"))))) "holds"  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p1")) "," (Set (Var "s1")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p2")) "," (Set (Var "s2")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )))))))) ; 
 definitionlet "p" be   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "s" be   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "a" be   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::); let "I" be   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); assume that  
(Bool  "("  (Bool   ($#r3_scmfsa9a :::"ProperBodyWhile>0"::: )  (Set (Const "a")) "," (Set (Const "I")) "," (Set (Const "s")) "," (Set (Const "p"))) "or" (Bool (Set (Const "I")) "is"   ($#v7_amistd_1 :::"parahalting"::: )  )  ")" )
 and  
(Bool   ($#r4_scmfsa9a :::"WithVariantWhile>0"::: )  (Set (Const "a")) "," (Set (Const "I")) "," (Set (Const "s")) "," (Set (Const "p")))
 ; func  :::"ExitsAtWhile>0":::  "(" "a" "," "I" "," "p" "," "s" ")"  ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) means :: SCMFSA9A:def 6 (Bool  "ex" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool it  ($#r1_hidden :::"="::: )  (Set (Var "k"))) & (Bool (Set (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" "a" "," "I" "," "p" "," "s" ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k1_funct_1 :::"."::: )  "a")  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" "a" "," "I" "," "p" "," "s" ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k1_funct_1 :::"."::: )  "a")  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i")))  ")" ) & (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set  "(" "p"  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k2_scmfsa_9 :::"while>0"::: )   "(" "a" "," "I" ")"  ")" ) ")" ) "," (Set  "("  ($#k8_memstr_0 :::"Initialize"::: )  "s" ")" ) "," (Set  "("  ($#k8_extpro_1 :::"LifeSpan"::: )   "(" (Set  "(" "p"  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k2_scmfsa_9 :::"while>0"::: )   "(" "a" "," "I" ")"  ")" ) ")" ) "," (Set  "("  ($#k8_memstr_0 :::"Initialize"::: )  "s" ")" ) ")"  ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" "a" "," "I" "," "p" "," "s" ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )))  ")" )); end; 









:: deftheorem    defines :::"ExitsAtWhile>0"::: SCMFSA9A:def 6 :  (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"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool  "("  (Bool   ($#r3_scmfsa9a :::"ProperBodyWhile>0"::: )  (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "s")) "," (Set (Var "p"))) "or" (Bool (Set (Var "I")) "is"   ($#v7_amistd_1 :::"parahalting"::: )  )  ")" ) & (Bool   ($#r4_scmfsa9a :::"WithVariantWhile>0"::: )  (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "s")) "," (Set (Var "p")))) "holds"  (Bool  "for" (Set (Var "b5")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_scmfsa9a :::"ExitsAtWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" )) "iff" (Bool  "ex" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set (Var "k"))) & (Bool (Set (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i")))  ")" ) & (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set  "(" (Set (Var "p"))  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k2_scmfsa_9 :::"while>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) ")"  ")" ) ")" ) "," (Set  "("  ($#k8_memstr_0 :::"Initialize"::: )  (Set (Var "s")) ")" ) "," (Set  "("  ($#k8_extpro_1 :::"LifeSpan"::: )   "(" (Set  "(" (Set (Var "p"))  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k2_scmfsa_9 :::"while>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) ")"  ")" ) ")" ) "," (Set  "("  ($#k8_memstr_0 :::"Initialize"::: )  (Set (Var "s")) ")" ) ")"  ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )))  ")" ))  ")" )))))); 
 
theorem :: SCMFSA9A:35 (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"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "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 "a")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set  "("  ($#k2_scmfsa_9 :::"while>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) ")"  ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set (Var "s")))))))) ; 
 
theorem :: SCMFSA9A:36 (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"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool  "("  (Bool   ($#r3_scmfsa9a :::"ProperBodyWhile>0"::: )  (Set (Var "a")) "," (Set (Var "I")) "," (Set   ($#k1_scmfsa_m :::"Initialized"::: )  (Set (Var "s"))) "," (Set (Var "p"))) "or" (Bool (Set (Var "I")) "is"   ($#v7_amistd_1 :::"parahalting"::: )  )  ")" ) & (Bool   ($#r4_scmfsa9a :::"WithVariantWhile>0"::: )  (Set (Var "a")) "," (Set (Var "I")) "," (Set   ($#k1_scmfsa_m :::"Initialized"::: )  (Set (Var "s"))) "," (Set (Var "p")))) "holds"  (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set  "("  ($#k2_scmfsa_9 :::"while>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) ")"  ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set  "("  ($#k1_scmfsa_m :::"Initialized"::: )  (Set (Var "s")) ")" ) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set  "("  ($#k2_scmfsa9a :::"ExitsAtWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set  "("  ($#k1_scmfsa_m :::"Initialized"::: )  (Set (Var "s")) ")" ) ")"  ")" ) ")" ))))))) ; 
 
theorem :: SCMFSA9A:37 (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"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" ))))))))) ; 
 
theorem :: SCMFSA9A:38 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "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"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "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")))) & (Bool   ($#r3_scmfsa9a :::"ProperBodyWhile>0"::: )  (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "s1")) "," (Set (Var "p1")))) "holds"  (Bool   ($#r3_scmfsa9a :::"ProperBodyWhile>0"::: )  (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "s2")) "," (Set (Var "p2"))))))) ; 
 
theorem :: SCMFSA9A:39 (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"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "Ig")) "being"   ($#v1_scmfsa7b :::"good"::: )    ($#m1_hidden :::"Program":::) "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   ($#r3_scmfsa9a :::"ProperBodyWhile>0"::: )  (Set (Var "a")) "," (Set (Var "Ig")) "," (Set (Var "s")) "," (Set (Var "p"))) & (Bool   ($#r4_scmfsa9a :::"WithVariantWhile>0"::: )  (Set (Var "a")) "," (Set (Var "Ig")) "," (Set (Var "s")) "," (Set (Var "p")))) "holds"  (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r1_hidden :::"<>"::: )  (Set (Var "j"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k2_scmfsa9a :::"ExitsAtWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")" )) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k2_scmfsa9a :::"ExitsAtWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"<>"::: )  (Set (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "j")))) & (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "i")) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "j")) ")" )))  ")" )))))) ; 
 definitioncanceled; end; 
:: deftheorem   SCMFSA9A:def 7 :  canceled;  
 
theorem :: SCMFSA9A:40 (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"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "Ig")) "being"   ($#v1_scmfsa7b :::"good"::: )    ($#m1_hidden :::"Program":::) "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   ($#r3_scmfsa9a :::"ProperBodyWhile>0"::: )  (Set (Var "a")) "," (Set (Var "Ig")) "," (Set (Var "s")) "," (Set (Var "p"))) & (Bool   ($#r4_scmfsa9a :::"WithVariantWhile>0"::: )  (Set (Var "a")) "," (Set (Var "Ig")) "," (Set (Var "s")) "," (Set (Var "p")))) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k4_card_3 :::"product"::: )  (Set  "("  ($#k2_memstr_0 :::"the_Values_of"::: )  (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ) "," (Set  ($#k5_numbers :::"NAT"::: ) ) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v7_memstr_0 :::"on_data_only"::: )  ) & (Bool  "("   "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set (Var "a")) "," (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" ))) "or" (Bool (Set (Set  "(" (Set  "("  ($#k5_scmfsa_9 :::"StepWhile>0"::: )   "(" (Set (Var "a")) "," (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   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )  ")" )))))) ; 
 
theorem :: SCMFSA9A:41 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "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"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "Ig")) "being"   ($#v1_scmfsa7b :::"good"::: )    ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Set (Var "s1"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set (Var "s1")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set (Var "s2")))) & (Bool   ($#r3_scmfsa9a :::"ProperBodyWhile>0"::: )  (Set (Var "a")) "," (Set (Var "Ig")) "," (Set (Var "s1")) "," (Set (Var "p1"))) & (Bool   ($#r4_scmfsa9a :::"WithVariantWhile>0"::: )  (Set (Var "a")) "," (Set (Var "Ig")) "," (Set (Var "s1")) "," (Set (Var "p1")))) "holds"  (Bool   ($#r4_scmfsa9a :::"WithVariantWhile>0"::: )  (Set (Var "a")) "," (Set (Var "Ig")) "," (Set (Var "s2")) "," (Set (Var "p2"))))))) ; 
 begin  definitionlet "N", "result" be   ($#m1_subset_1 :::"Int-Location":::); func  :::"Fusc_macro":::  "(" "N" "," "result" ")"  ->   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) equals :: SCMFSA9A:def 8 (Set (Set  "(" (Set  "(" (Set  "("  ($#k8_scmfsa_2 :::"SubFrom"::: )   "(" "result" "," "result" ")"  ")" )  ($#k6_scmfsa6a :::"";""::: )  (Set  "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  ($#k5_scmfsa_m :::"{"::: ) "N" "," "result" ($#k5_scmfsa_m :::"}"::: ) ) ")" )  ($#k6_scmfsa_2 :::":="::: )  (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" )  ($#k5_scmfsa6a :::"";""::: )  (Set  "(" (Set  "(" (Num 2)  ($#k9_scmfsa_m :::"-ndRWNotIn"::: )  (Set  ($#k5_scmfsa_m :::"{"::: ) "N" "," "result" ($#k5_scmfsa_m :::"}"::: ) ) ")" )  ($#k6_scmfsa_2 :::":="::: )  "N" ")" ) ")" )  ($#k3_scmfsa6a :::"";""::: )  (Set  "("  ($#k2_scmfsa_9 :::"while>0"::: )   "(" (Set  "(" (Num 2)  ($#k9_scmfsa_m :::"-ndRWNotIn"::: )  (Set  ($#k5_scmfsa_m :::"{"::: ) "N" "," "result" ($#k5_scmfsa_m :::"}"::: ) ) ")" ) "," (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 3)  ($#k9_scmfsa_m :::"-rdRWNotIn"::: )  (Set  ($#k5_scmfsa_m :::"{"::: ) "N" "," "result" ($#k5_scmfsa_m :::"}"::: ) ) ")" )  ($#k1_scmfsa_7 :::":="::: )  (Num 2) ")" )  ($#k5_scmfsa6a :::"";""::: )  (Set  "("  ($#k10_scmfsa_2 :::"Divide"::: )   "(" (Set  "(" (Num 2)  ($#k9_scmfsa_m :::"-ndRWNotIn"::: )  (Set  ($#k5_scmfsa_m :::"{"::: ) "N" "," "result" ($#k5_scmfsa_m :::"}"::: ) ) ")" ) "," (Set  "(" (Num 3)  ($#k9_scmfsa_m :::"-rdRWNotIn"::: )  (Set  ($#k5_scmfsa_m :::"{"::: ) "N" "," "result" ($#k5_scmfsa_m :::"}"::: ) ) ")" ) ")"  ")" ) ")" )  ($#k3_scmfsa6a :::"";""::: )  (Set  "("  ($#k1_scmfsa8b :::"if=0"::: )   "(" (Set  "(" (Num 3)  ($#k9_scmfsa_m :::"-rdRWNotIn"::: )  (Set  ($#k5_scmfsa_m :::"{"::: ) "N" "," "result" ($#k5_scmfsa_m :::"}"::: ) ) ")" ) "," (Set  "("  ($#k11_compos_1 :::"Macro"::: )  (Set  "("  ($#k7_scmfsa_2 :::"AddTo"::: )   "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  ($#k5_scmfsa_m :::"{"::: ) "N" "," "result" ($#k5_scmfsa_m :::"}"::: ) ) ")" ) "," "result" ")"  ")" ) ")" ) "," (Set  "("  ($#k11_compos_1 :::"Macro"::: )  (Set  "("  ($#k7_scmfsa_2 :::"AddTo"::: )   "(" "result" "," (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  ($#k5_scmfsa_m :::"{"::: ) "N" "," "result" ($#k5_scmfsa_m :::"}"::: ) ) ")" ) ")"  ")" ) ")" ) ")"  ")" ) ")" ) ")"  ")" )); end; 






:: deftheorem    defines :::"Fusc_macro"::: SCMFSA9A:def 8 :  (Bool  "for" (Set (Var "N")) "," (Set (Var "result")) "being"   ($#m1_subset_1 :::"Int-Location":::) "holds"  (Bool (Set   ($#k3_scmfsa9a :::"Fusc_macro"::: )   "(" (Set (Var "N")) "," (Set (Var "result")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k8_scmfsa_2 :::"SubFrom"::: )   "(" (Set (Var "result")) "," (Set (Var "result")) ")"  ")" )  ($#k6_scmfsa6a :::"";""::: )  (Set  "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  ($#k5_scmfsa_m :::"{"::: ) (Set (Var "N")) "," (Set (Var "result")) ($#k5_scmfsa_m :::"}"::: ) ) ")" )  ($#k6_scmfsa_2 :::":="::: )  (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" )  ($#k5_scmfsa6a :::"";""::: )  (Set  "(" (Set  "(" (Num 2)  ($#k9_scmfsa_m :::"-ndRWNotIn"::: )  (Set  ($#k5_scmfsa_m :::"{"::: ) (Set (Var "N")) "," (Set (Var "result")) ($#k5_scmfsa_m :::"}"::: ) ) ")" )  ($#k6_scmfsa_2 :::":="::: )  (Set (Var "N")) ")" ) ")" )  ($#k3_scmfsa6a :::"";""::: )  (Set  "("  ($#k2_scmfsa_9 :::"while>0"::: )   "(" (Set  "(" (Num 2)  ($#k9_scmfsa_m :::"-ndRWNotIn"::: )  (Set  ($#k5_scmfsa_m :::"{"::: ) (Set (Var "N")) "," (Set (Var "result")) ($#k5_scmfsa_m :::"}"::: ) ) ")" ) "," (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 3)  ($#k9_scmfsa_m :::"-rdRWNotIn"::: )  (Set  ($#k5_scmfsa_m :::"{"::: ) (Set (Var "N")) "," (Set (Var "result")) ($#k5_scmfsa_m :::"}"::: ) ) ")" )  ($#k1_scmfsa_7 :::":="::: )  (Num 2) ")" )  ($#k5_scmfsa6a :::"";""::: )  (Set  "("  ($#k10_scmfsa_2 :::"Divide"::: )   "(" (Set  "(" (Num 2)  ($#k9_scmfsa_m :::"-ndRWNotIn"::: )  (Set  ($#k5_scmfsa_m :::"{"::: ) (Set (Var "N")) "," (Set (Var "result")) ($#k5_scmfsa_m :::"}"::: ) ) ")" ) "," (Set  "(" (Num 3)  ($#k9_scmfsa_m :::"-rdRWNotIn"::: )  (Set  ($#k5_scmfsa_m :::"{"::: ) (Set (Var "N")) "," (Set (Var "result")) ($#k5_scmfsa_m :::"}"::: ) ) ")" ) ")"  ")" ) ")" )  ($#k3_scmfsa6a :::"";""::: )  (Set  "("  ($#k1_scmfsa8b :::"if=0"::: )   "(" (Set  "(" (Num 3)  ($#k9_scmfsa_m :::"-rdRWNotIn"::: )  (Set  ($#k5_scmfsa_m :::"{"::: ) (Set (Var "N")) "," (Set (Var "result")) ($#k5_scmfsa_m :::"}"::: ) ) ")" ) "," (Set  "("  ($#k11_compos_1 :::"Macro"::: )  (Set  "("  ($#k7_scmfsa_2 :::"AddTo"::: )   "(" (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  ($#k5_scmfsa_m :::"{"::: ) (Set (Var "N")) "," (Set (Var "result")) ($#k5_scmfsa_m :::"}"::: ) ) ")" ) "," (Set (Var "result")) ")"  ")" ) ")" ) "," (Set  "("  ($#k11_compos_1 :::"Macro"::: )  (Set  "("  ($#k7_scmfsa_2 :::"AddTo"::: )   "(" (Set (Var "result")) "," (Set  "(" (Num 1)  ($#k9_scmfsa_m :::"-stRWNotIn"::: )  (Set  ($#k5_scmfsa_m :::"{"::: ) (Set (Var "N")) "," (Set (Var "result")) ($#k5_scmfsa_m :::"}"::: ) ) ")" ) ")"  ")" ) ")" ) ")"  ")" ) ")" ) ")"  ")" )))); 
 
theorem :: SCMFSA9A:42 (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"::: ) )  (Bool  "for" (Set (Var "N")) "," (Set (Var "result")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::)  "st" (Bool (Bool (Set (Var "N"))  ($#r1_hidden :::"<>"::: )  (Set (Var "result")))) "holds"  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "N"))))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set  "("  ($#k3_scmfsa9a :::"Fusc_macro"::: )   "(" (Set (Var "N")) "," (Set (Var "result")) ")"  ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "result")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_pre_ff :::"Fusc"::: )  (Set (Var "n")))) & (Bool (Set (Set  "("  ($#k1_scmfsa6b :::"IExec"::: )   "(" (Set  "("  ($#k3_scmfsa9a :::"Fusc_macro"::: )   "(" (Set (Var "N")) "," (Set (Var "result")) ")"  ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "N")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))  ")" ))))) ;