:: SFMASTR2 semantic presentation begin theorem :: SFMASTR2:1 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "b")) "being" ($#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 ($#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 "b")) ($#r2_hidden :::"in"::: ) (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "I")))))) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))))))) ; theorem :: SFMASTR2: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"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-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 ($#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 "f")) ($#r2_hidden :::"in"::: ) (Set ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "I")))))) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")))))))) ; theorem :: SFMASTR2:3 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#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 "(" (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"))) ")" ) "or" (Bool (Set (Var "I")) "is" ($#v7_amistd_1 :::"parahalting"::: ) ) ")" ) & (Bool "(" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) "or" (Bool (Set (Var "a")) "is" ($#v1_scmfsa_m :::"read-write"::: ) ) ")" ) & (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "I")))))) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))))))) ; theorem :: SFMASTR2:4 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#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))) "holds" (Bool "(" (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "p"))) "iff" (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "p"))) ")" )))) ; theorem :: SFMASTR2:5 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#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))) "holds" (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"))) "iff" (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"))) ")" ) ")" )))) ; begin definitionlet "a" be ($#m1_subset_1 :::"Int-Location":::); let "I" be ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); func :::"times*"::: "(" "a" "," "I" ")" -> ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) equals :: SFMASTR2:def 1 (Set ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set "(" (Set ($#k4_scmfsa_m :::"{"::: ) "a" ($#k4_scmfsa_m :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) "I" ")" ) ")" ) ")" ) "," (Set "(" "I" ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set "(" (Set ($#k4_scmfsa_m :::"{"::: ) "a" ($#k4_scmfsa_m :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) "I" ")" ) ")" ) ")" ) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ")" ); end; :: deftheorem defines :::"times*"::: SFMASTR2:def 1 : (Bool "for" (Set (Var "a")) "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 ($#k1_sfmastr2 :::"times*"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set "(" (Set ($#k4_scmfsa_m :::"{"::: ) (Set (Var "a")) ($#k4_scmfsa_m :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "I")) ")" ) ")" ) ")" ) "," (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set "(" (Set ($#k4_scmfsa_m :::"{"::: ) (Set (Var "a")) ($#k4_scmfsa_m :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "I")) ")" ) ")" ) ")" ) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ")" )))); definitionlet "a" be ($#m1_subset_1 :::"Int-Location":::); let "I" be ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); func :::"times"::: "(" "a" "," "I" ")" -> ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) equals :: SFMASTR2:def 2 (Set (Set "(" (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set "(" (Set ($#k4_scmfsa_m :::"{"::: ) "a" ($#k4_scmfsa_m :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) "I" ")" ) ")" ) ")" ) ($#k6_scmfsa_2 :::":="::: ) "a" ")" ) ($#k4_scmfsa6a :::"";""::: ) (Set "(" ($#k1_sfmastr2 :::"times*"::: ) "(" "a" "," "I" ")" ")" )); end; :: deftheorem defines :::"times"::: SFMASTR2:def 2 : (Bool "for" (Set (Var "a")) "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_sfmastr2 :::"times"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set "(" (Set ($#k4_scmfsa_m :::"{"::: ) (Set (Var "a")) ($#k4_scmfsa_m :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "I")) ")" ) ")" ) ")" ) ($#k6_scmfsa_2 :::":="::: ) (Set (Var "a")) ")" ) ($#k4_scmfsa6a :::"";""::: ) (Set "(" ($#k1_sfmastr2 :::"times*"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ))))); notationlet "a" be ($#m1_subset_1 :::"Int-Location":::); let "I" be ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); synonym "a" :::"times"::: "I" for :::"times"::: "(" "a" "," "I" ")" ; end; theorem :: SFMASTR2:6 canceled; theorem :: SFMASTR2:7 canceled; theorem :: SFMASTR2:8 (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 (Set ($#k4_scmfsa_m :::"{"::: ) (Set (Var "b")) ($#k4_scmfsa_m :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "I")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set "(" ($#k2_sfmastr2 :::"times"::: ) "(" (Set (Var "b")) "," (Set (Var "I")) ")" ")" ))))) ; theorem :: SFMASTR2:9 (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_sfmastr2 :::"times"::: ) "(" (Set (Var "b")) "," (Set (Var "I")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "I")))))) ; registrationlet "I" be ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "a" be ($#m1_subset_1 :::"Int-Location":::); cluster (Set ($#k2_sfmastr2 :::"times"::: ) "(" "a" "," "I" ")" ) -> ($#v1_scmfsa7b :::"good"::: ) ; end; 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 "I" be ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "a" be ($#m1_subset_1 :::"Int-Location":::); func :::"StepTimes"::: "(" "a" "," "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 :: SFMASTR2:def 3 (Set ($#k5_scmfsa_9 :::"StepWhile>0"::: ) "(" (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set "(" (Set ($#k4_scmfsa_m :::"{"::: ) "a" ($#k4_scmfsa_m :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) "I" ")" ) ")" ) ")" ) "," (Set "(" "I" ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set "(" (Set ($#k4_scmfsa_m :::"{"::: ) "a" ($#k4_scmfsa_m :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) "I" ")" ) ")" ) ")" ) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) "," "p" "," (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set "(" (Set ($#k4_scmfsa_m :::"{"::: ) "a" ($#k4_scmfsa_m :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) "I" ")" ) ")" ) ")" ) ($#k6_scmfsa_2 :::":="::: ) "a" ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) "s" ")" ) ")" ")" ) ")" ); end; :: deftheorem defines :::"StepTimes"::: SFMASTR2: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 "I")) "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 ($#k3_sfmastr2 :::"StepTimes"::: ) "(" (Set (Var "a")) "," (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 ($#k4_scmfsa_m :::"{"::: ) (Set (Var "a")) ($#k4_scmfsa_m :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "I")) ")" ) ")" ) ")" ) "," (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set "(" (Set ($#k4_scmfsa_m :::"{"::: ) (Set (Var "a")) ($#k4_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 "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set "(" (Set ($#k4_scmfsa_m :::"{"::: ) (Set (Var "a")) ($#k4_scmfsa_m :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "I")) ")" ) ")" ) ")" ) ($#k6_scmfsa_2 :::":="::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ")" ) ")" )))))); theorem :: SFMASTR2:10 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "J")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k3_sfmastr2 :::"StepTimes"::: ) "(" (Set (Var "a")) "," (Set (Var "J")) "," (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 :: SFMASTR2:11 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "J")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool "(" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) "or" (Bool (Set (Var "a")) "is" ($#v1_scmfsa_m :::"read-write"::: ) ) ")" )) "holds" (Bool (Set (Set "(" (Set "(" ($#k3_sfmastr2 :::"StepTimes"::: ) "(" (Set (Var "a")) "," (Set (Var "J")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set "(" (Set ($#k4_scmfsa_m :::"{"::: ) (Set (Var "a")) ($#k4_scmfsa_m :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "J")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))))))) ; theorem :: SFMASTR2:12 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "J")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#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 "(" ($#k3_sfmastr2 :::"StepTimes"::: ) "(" (Set (Var "a")) "," (Set (Var "J")) "," (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 "J")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Set "(" ($#k3_sfmastr2 :::"StepTimes"::: ) "(" (Set (Var "a")) "," (Set (Var "J")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) "," (Set (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_sfmastr2 :::"times*"::: ) "(" (Set (Var "a")) "," (Set (Var "J")) ")" ")" ))) & (Bool (Set (Var "J")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set (Set "(" ($#k3_sfmastr2 :::"StepTimes"::: ) "(" (Set (Var "a")) "," (Set (Var "J")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) "," (Set (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_sfmastr2 :::"times*"::: ) "(" (Set (Var "a")) "," (Set (Var "J")) ")" ")" )))) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k3_sfmastr2 :::"StepTimes"::: ) "(" (Set (Var "a")) "," (Set (Var "J")) "," (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)) & "(" (Bool (Bool (Set (Set "(" (Set "(" ($#k3_sfmastr2 :::"StepTimes"::: ) "(" (Set (Var "a")) "," (Set (Var "J")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set "(" (Set ($#k4_scmfsa_m :::"{"::: ) (Set (Var "a")) ($#k4_scmfsa_m :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "J")) ")" ) ")" ) ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set "(" (Set "(" ($#k3_sfmastr2 :::"StepTimes"::: ) "(" (Set (Var "a")) "," (Set (Var "J")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set "(" (Set ($#k4_scmfsa_m :::"{"::: ) (Set (Var "a")) ($#k4_scmfsa_m :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "J")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k3_sfmastr2 :::"StepTimes"::: ) "(" (Set (Var "a")) "," (Set (Var "J")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set "(" (Set ($#k4_scmfsa_m :::"{"::: ) (Set (Var "a")) ($#k4_scmfsa_m :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "J")) ")" ) ")" ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) ")" ")" )))))) ; theorem :: SFMASTR2:13 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#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 (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) "or" (Bool (Set (Var "a")) "is" ($#v1_scmfsa_m :::"read-write"::: ) ) ")" )) "holds" (Bool (Set (Set "(" (Set "(" ($#k3_sfmastr2 :::"StepTimes"::: ) "(" (Set (Var "a")) "," (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 "a")))))))) ; theorem :: SFMASTR2:14 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "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" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k3_sfmastr2 :::"StepTimes"::: ) "(" (Set (Var "a")) "," (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"))))))))) ; 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 ($#m1_subset_1 :::"Int-Location":::); let "I" be ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); pred :::"ProperTimesBody"::: "a" "," "I" "," "s" "," "p" means :: SFMASTR2:def 4 (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 "s" ($#k1_funct_1 :::"."::: ) "a"))) "holds" (Bool "(" (Bool "I" ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Set "(" ($#k3_sfmastr2 :::"StepTimes"::: ) "(" "a" "," "I" "," "p" "," "s" ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) "," (Set "p" ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_sfmastr2 :::"times*"::: ) "(" "a" "," "I" ")" ")" ))) & (Bool "I" ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set (Set "(" ($#k3_sfmastr2 :::"StepTimes"::: ) "(" "a" "," "I" "," "p" "," "s" ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) "," (Set "p" ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_sfmastr2 :::"times*"::: ) "(" "a" "," "I" ")" ")" ))) ")" )); end; :: deftheorem defines :::"ProperTimesBody"::: SFMASTR2: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" ($#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_sfmastr2 :::"ProperTimesBody"::: ) (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 (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))) "holds" (Bool "(" (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Set "(" ($#k3_sfmastr2 :::"StepTimes"::: ) "(" (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_sfmastr2 :::"times*"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ))) & (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set (Set "(" ($#k3_sfmastr2 :::"StepTimes"::: ) "(" (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_sfmastr2 :::"times*"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ))) ")" )) ")" ))))); theorem :: SFMASTR2:15 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#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")) "is" ($#v7_amistd_1 :::"parahalting"::: ) )) "holds" (Bool ($#r1_sfmastr2 :::"ProperTimesBody"::: ) (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "s")) "," (Set (Var "p"))))))) ; theorem :: SFMASTR2:16 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "J")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool ($#r1_sfmastr2 :::"ProperTimesBody"::: ) (Set (Var "a")) "," (Set (Var "J")) "," (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 (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))) "holds" (Bool (Set (Set "(" (Set "(" ($#k3_sfmastr2 :::"StepTimes"::: ) "(" (Set (Var "a")) "," (Set (Var "J")) "," (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 :: SFMASTR2:17 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "J")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool "(" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) "or" (Bool (Set (Var "a")) "is" ($#v1_scmfsa_m :::"read-write"::: ) ) ")" ) & (Bool ($#r1_sfmastr2 :::"ProperTimesBody"::: ) (Set (Var "a")) "," (Set (Var "J")) "," (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 (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" ($#k3_sfmastr2 :::"StepTimes"::: ) "(" (Set (Var "a")) "," (Set (Var "J")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set "(" (Set ($#k4_scmfsa_m :::"{"::: ) (Set (Var "a")) ($#k4_scmfsa_m :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "J")) ")" ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))))))) ; theorem :: SFMASTR2:18 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "J")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool ($#r1_sfmastr2 :::"ProperTimesBody"::: ) (Set (Var "a")) "," (Set (Var "J")) "," (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool "(" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) "or" (Bool (Set (Var "a")) "is" ($#v1_scmfsa_m :::"read-write"::: ) ) ")" )) "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 (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k3_sfmastr2 :::"StepTimes"::: ) "(" (Set (Var "a")) "," (Set (Var "J")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set "(" (Set ($#k4_scmfsa_m :::"{"::: ) (Set (Var "a")) ($#k4_scmfsa_m :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "J")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set "(" ($#k3_sfmastr2 :::"StepTimes"::: ) "(" (Set (Var "a")) "," (Set (Var "J")) "," (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 :: SFMASTR2:19 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#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))) "holds" (Bool (Set (Set "(" (Set "(" ($#k3_sfmastr2 :::"StepTimes"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k11_card_3 :::"|"::: ) (Set "(" (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "I")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "I")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) ) ")" ))))))) ; theorem :: SFMASTR2:20 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "J")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#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 "(" ($#k3_sfmastr2 :::"StepTimes"::: ) "(" (Set (Var "a")) "," (Set (Var "J")) "," (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 "J")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set "(" (Set "(" ($#k3_sfmastr2 :::"StepTimes"::: ) "(" (Set (Var "a")) "," (Set (Var "J")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" )) "," (Set (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_sfmastr2 :::"times*"::: ) "(" (Set (Var "a")) "," (Set (Var "J")) ")" ")" ))) & (Bool (Set (Var "J")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set "(" (Set "(" ($#k3_sfmastr2 :::"StepTimes"::: ) "(" (Set (Var "a")) "," (Set (Var "J")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" )) "," (Set (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_sfmastr2 :::"times*"::: ) "(" (Set (Var "a")) "," (Set (Var "J")) ")" ")" ))) & (Bool (Set (Set "(" (Set "(" ($#k3_sfmastr2 :::"StepTimes"::: ) "(" (Set (Var "a")) "," (Set (Var "J")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set "(" (Set ($#k4_scmfsa_m :::"{"::: ) (Set (Var "a")) ($#k4_scmfsa_m :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "J")) ")" ) ")" ) ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" ($#k3_sfmastr2 :::"StepTimes"::: ) "(" (Set (Var "a")) "," (Set (Var "J")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k11_card_3 :::"|"::: ) (Set "(" (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "J")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "J")) "," (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_sfmastr2 :::"times*"::: ) "(" (Set (Var "a")) "," (Set (Var "J")) ")" ")" ) ")" ) "," (Set "(" (Set "(" ($#k3_sfmastr2 :::"StepTimes"::: ) "(" (Set (Var "a")) "," (Set (Var "J")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "J")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) ) ")" )))))))) ; theorem :: SFMASTR2:21 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "J")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#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 ($#r1_sfmastr2 :::"ProperTimesBody"::: ) (Set (Var "a")) "," (Set (Var "J")) "," (Set (Var "s")) "," (Set (Var "p"))) "or" (Bool (Set (Var "J")) "is" ($#v7_amistd_1 :::"parahalting"::: ) ) ")" ) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool "(" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) "or" (Bool (Set (Var "a")) "is" ($#v1_scmfsa_m :::"read-write"::: ) ) ")" )) "holds" (Bool (Set (Set "(" (Set "(" ($#k3_sfmastr2 :::"StepTimes"::: ) "(" (Set (Var "a")) "," (Set (Var "J")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k11_card_3 :::"|"::: ) (Set "(" (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "J")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "J")) "," (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_sfmastr2 :::"times*"::: ) "(" (Set (Var "a")) "," (Set (Var "J")) ")" ")" ) ")" ) "," (Set "(" (Set "(" ($#k3_sfmastr2 :::"StepTimes"::: ) "(" (Set (Var "a")) "," (Set (Var "J")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "J")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) ) ")" )))))))) ; theorem :: SFMASTR2:22 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#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 (Var "a"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (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 "(" ($#k2_sfmastr2 :::"times"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "I")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "I")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) ) ")" ))))))) ; theorem :: SFMASTR2:23 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "J")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#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 (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "k"))) & (Bool "(" (Bool ($#r1_sfmastr2 :::"ProperTimesBody"::: ) (Set (Var "a")) "," (Set (Var "J")) "," (Set (Var "s")) "," (Set (Var "p"))) "or" (Bool (Set (Var "J")) "is" ($#v7_amistd_1 :::"parahalting"::: ) ) ")" ) & (Bool "(" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) "or" (Bool (Set (Var "a")) "is" ($#v1_scmfsa_m :::"read-write"::: ) ) ")" )) "holds" (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_sfmastr2 :::"times"::: ) "(" (Set (Var "a")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" (Set "(" ($#k3_sfmastr2 :::"StepTimes"::: ) "(" (Set (Var "a")) "," (Set (Var "J")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" )))))))) ; theorem :: SFMASTR2:24 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "J")) "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 "(" (Bool ($#r1_sfmastr2 :::"ProperTimesBody"::: ) (Set (Var "a")) "," (Set (Var "J")) "," (Set (Var "s")) "," (Set (Var "p"))) "or" (Bool (Set (Var "J")) "is" ($#v7_amistd_1 :::"parahalting"::: ) ) ")" )) "holds" (Bool "(" (Bool (Set ($#k2_sfmastr2 :::"times"::: ) "(" (Set (Var "a")) "," (Set (Var "J")) ")" ) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set ($#k2_sfmastr2 :::"times"::: ) "(" (Set (Var "a")) "," (Set (Var "J")) ")" ) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "p"))) ")" ))))) ; begin definitionlet "d" be ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::); func :::"triv-times"::: "d" -> ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) equals :: SFMASTR2:def 5 (Set ($#k2_sfmastr2 :::"times"::: ) "(" "d" "," (Set "(" (Set "(" ($#k1_scmfsa_9 :::"while=0"::: ) "(" "d" "," (Set "(" ($#k11_compos_1 :::"Macro"::: ) (Set "(" "d" ($#k6_scmfsa_2 :::":="::: ) "d" ")" ) ")" ) ")" ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" "d" "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ")" ); end; :: deftheorem defines :::"triv-times"::: SFMASTR2:def 5 : (Bool "for" (Set (Var "d")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set ($#k4_sfmastr2 :::"triv-times"::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set ($#k2_sfmastr2 :::"times"::: ) "(" (Set (Var "d")) "," (Set "(" (Set "(" ($#k1_scmfsa_9 :::"while=0"::: ) "(" (Set (Var "d")) "," (Set "(" ($#k11_compos_1 :::"Macro"::: ) (Set "(" (Set (Var "d")) ($#k6_scmfsa_2 :::":="::: ) (Set (Var "d")) ")" ) ")" ) ")" ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "d")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ")" ))); theorem :: SFMASTR2:25 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k4_sfmastr2 :::"triv-times"::: ) (Set (Var "d")) ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))))))) ; theorem :: SFMASTR2:26 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))))) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k4_sfmastr2 :::"triv-times"::: ) (Set (Var "d")) ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; begin definitionlet "N", "result" be ($#m1_subset_1 :::"Int-Location":::); func :::"Fib-macro"::: "(" "N" "," "result" ")" -> ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) equals :: SFMASTR2:def 6 (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k1_sfmastr1 :::"-stNotUsed"::: ) (Set "(" ($#k2_sfmastr2 :::"times"::: ) "(" "N" "," (Set "(" (Set "(" ($#k7_scmfsa_2 :::"AddTo"::: ) "(" "result" "," (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set ($#k5_scmfsa_m :::"{"::: ) "N" "," "result" ($#k5_scmfsa_m :::"}"::: ) ) ")" ) ")" ")" ) ($#k4_scmfsa6a :::"";""::: ) (Set "(" ($#k1_scmfsa6c :::"swap"::: ) "(" "result" "," (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set ($#k5_scmfsa_m :::"{"::: ) "N" "," "result" ($#k5_scmfsa_m :::"}"::: ) ) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ) ($#k6_scmfsa_2 :::":="::: ) "N" ")" ) ($#k6_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" "result" "," "result" ")" ")" ) ")" ) ($#k5_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"::: ) ) ")" ) ")" ) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k2_sfmastr2 :::"times"::: ) "(" "N" "," (Set "(" (Set "(" ($#k7_scmfsa_2 :::"AddTo"::: ) "(" "result" "," (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set ($#k5_scmfsa_m :::"{"::: ) "N" "," "result" ($#k5_scmfsa_m :::"}"::: ) ) ")" ) ")" ")" ) ($#k4_scmfsa6a :::"";""::: ) (Set "(" ($#k1_scmfsa6c :::"swap"::: ) "(" "result" "," (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set ($#k5_scmfsa_m :::"{"::: ) "N" "," "result" ($#k5_scmfsa_m :::"}"::: ) ) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" "N" ($#k6_scmfsa_2 :::":="::: ) (Set "(" (Num 1) ($#k1_sfmastr1 :::"-stNotUsed"::: ) (Set "(" ($#k2_sfmastr2 :::"times"::: ) "(" "N" "," (Set "(" (Set "(" ($#k7_scmfsa_2 :::"AddTo"::: ) "(" "result" "," (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set ($#k5_scmfsa_m :::"{"::: ) "N" "," "result" ($#k5_scmfsa_m :::"}"::: ) ) ")" ) ")" ")" ) ($#k4_scmfsa6a :::"";""::: ) (Set "(" ($#k1_scmfsa6c :::"swap"::: ) "(" "result" "," (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set ($#k5_scmfsa_m :::"{"::: ) "N" "," "result" ($#k5_scmfsa_m :::"}"::: ) ) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ) ")" )); end; :: deftheorem defines :::"Fib-macro"::: SFMASTR2:def 6 : (Bool "for" (Set (Var "N")) "," (Set (Var "result")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set ($#k5_sfmastr2 :::"Fib-macro"::: ) "(" (Set (Var "N")) "," (Set (Var "result")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k1_sfmastr1 :::"-stNotUsed"::: ) (Set "(" ($#k2_sfmastr2 :::"times"::: ) "(" (Set (Var "N")) "," (Set "(" (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 :::"}"::: ) ) ")" ) ")" ")" ) ($#k4_scmfsa6a :::"";""::: ) (Set "(" ($#k1_scmfsa6c :::"swap"::: ) "(" (Set (Var "result")) "," (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set ($#k5_scmfsa_m :::"{"::: ) (Set (Var "N")) "," (Set (Var "result")) ($#k5_scmfsa_m :::"}"::: ) ) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ) ($#k6_scmfsa_2 :::":="::: ) (Set (Var "N")) ")" ) ($#k6_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "result")) "," (Set (Var "result")) ")" ")" ) ")" ) ($#k5_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"::: ) ) ")" ) ")" ) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k2_sfmastr2 :::"times"::: ) "(" (Set (Var "N")) "," (Set "(" (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 :::"}"::: ) ) ")" ) ")" ")" ) ($#k4_scmfsa6a :::"";""::: ) (Set "(" ($#k1_scmfsa6c :::"swap"::: ) "(" (Set (Var "result")) "," (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set ($#k5_scmfsa_m :::"{"::: ) (Set (Var "N")) "," (Set (Var "result")) ($#k5_scmfsa_m :::"}"::: ) ) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" (Set (Var "N")) ($#k6_scmfsa_2 :::":="::: ) (Set "(" (Num 1) ($#k1_sfmastr1 :::"-stNotUsed"::: ) (Set "(" ($#k2_sfmastr2 :::"times"::: ) "(" (Set (Var "N")) "," (Set "(" (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 :::"}"::: ) ) ")" ) ")" ")" ) ($#k4_scmfsa6a :::"";""::: ) (Set "(" ($#k1_scmfsa6c :::"swap"::: ) "(" (Set (Var "result")) "," (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set ($#k5_scmfsa_m :::"{"::: ) (Set (Var "N")) "," (Set (Var "result")) ($#k5_scmfsa_m :::"}"::: ) ) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ) ")" )))); theorem :: SFMASTR2:27 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "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 "(" ($#k5_sfmastr2 :::"Fib-macro"::: ) "(" (Set (Var "N")) "," (Set (Var "result")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "result"))) ($#r1_hidden :::"="::: ) (Set ($#k1_pre_ff :::"Fib"::: ) (Set (Var "n")))) & (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k5_sfmastr2 :::"Fib-macro"::: ) "(" (Set (Var "N")) "," (Set (Var "result")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "N")))) ")" ))))) ;