:: SFMASTR1 semantic presentation begin definitionlet "i" be ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); attr "i" is :::"good"::: means :: SFMASTR1:def 1 (Bool (Set ($#k11_compos_1 :::"Macro"::: ) "i") "is" ($#v1_scmfsa7b :::"good"::: ) ); end; :: deftheorem defines :::"good"::: SFMASTR1:def 1 : (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Var "i")) "is" ($#v1_sfmastr1 :::"good"::: ) ) "iff" (Bool (Set ($#k11_compos_1 :::"Macro"::: ) (Set (Var "i"))) "is" ($#v1_scmfsa7b :::"good"::: ) ) ")" )); registrationlet "a" be ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::); let "b" be ($#m1_subset_1 :::"Int-Location":::); cluster (Set "a" ($#k6_scmfsa_2 :::":="::: ) "b") -> ($#v1_sfmastr1 :::"good"::: ) ; cluster (Set ($#k7_scmfsa_2 :::"AddTo"::: ) "(" "a" "," "b" ")" ) -> ($#v1_sfmastr1 :::"good"::: ) ; cluster (Set ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" "a" "," "b" ")" ) -> ($#v1_sfmastr1 :::"good"::: ) ; cluster (Set ($#k9_scmfsa_2 :::"MultBy"::: ) "(" "a" "," "b" ")" ) -> ($#v1_sfmastr1 :::"good"::: ) ; end; registration cluster ($#v1_scmfsa6c :::"parahalting"::: ) ($#v1_amistd_2 :::"with_explicit_jumps"::: ) ($#v3_amistd_2 :::"IC-relocable"::: ) ($#v1_sfmastr1 :::"good"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )); end; registrationlet "a", "b" be ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::); cluster (Set ($#k10_scmfsa_2 :::"Divide"::: ) "(" "a" "," "b" ")" ) -> ($#v1_sfmastr1 :::"good"::: ) ; end; registrationlet "l" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k11_scmfsa_2 :::"goto"::: ) "l") -> ($#v1_sfmastr1 :::"good"::: ) ; end; registrationlet "a" be ($#m1_subset_1 :::"Int-Location":::); let "l" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set "a" ($#k12_scmfsa_2 :::"=0_goto"::: ) "l") -> ($#v1_sfmastr1 :::"good"::: ) ; cluster (Set "a" ($#k13_scmfsa_2 :::">0_goto"::: ) "l") -> ($#v1_sfmastr1 :::"good"::: ) ; end; registrationlet "a" be ($#m1_subset_1 :::"Int-Location":::); let "f" be ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) ; let "b" be ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::); cluster (Set "b" ($#k14_scmfsa_2 :::":="::: ) "(" "f" "," "a" ")" ) -> ($#v1_sfmastr1 :::"good"::: ) ; end; registrationlet "f" be ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) ; let "b" be ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::); cluster (Set "b" ($#k16_scmfsa_2 :::":=len"::: ) "f") -> ($#v1_sfmastr1 :::"good"::: ) ; end; registrationlet "f" be ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) ; let "a" be ($#m1_subset_1 :::"Int-Location":::); cluster (Set "f" ($#k17_scmfsa_2 :::":=<0,...,0>"::: ) "a") -> ($#v1_sfmastr1 :::"good"::: ) ; let "b" be ($#m1_subset_1 :::"Int-Location":::); cluster (Set "(" "f" "," "a" ")" ($#k15_scmfsa_2 :::":="::: ) "b") -> ($#v1_sfmastr1 :::"good"::: ) ; end; registrationlet "i" be ($#v1_sfmastr1 :::"good"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); cluster (Set ($#k11_compos_1 :::"Macro"::: ) "i") -> ($#v1_scmfsa7b :::"good"::: ) ; end; registrationlet "i", "j" be ($#v1_sfmastr1 :::"good"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); cluster (Set "i" ($#k6_scmfsa6a :::"";""::: ) "j") -> ($#v1_scmfsa7b :::"good"::: ) ; end; registrationlet "i" be ($#v1_sfmastr1 :::"good"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "I" be ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); cluster (Set "i" ($#k4_scmfsa6a :::"";""::: ) "I") -> ($#v1_scmfsa7b :::"good"::: ) ; cluster (Set "I" ($#k5_scmfsa6a :::"";""::: ) "i") -> ($#v1_scmfsa7b :::"good"::: ) ; end; registrationlet "a", "b" be ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::); cluster (Set ($#k1_scmfsa6c :::"swap"::: ) "(" "a" "," "b" ")" ) -> ($#v1_scmfsa7b :::"good"::: ) ; end; registrationlet "I" be ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "a" be ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::); cluster (Set ($#k2_scmfsa8c :::"Times"::: ) "(" "a" "," "I" ")" ) -> ($#v1_scmfsa7b :::"good"::: ) ; end; theorem :: SFMASTR1: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"::: ) ) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "I")))))) "holds" (Bool "not" (Bool (Set (Var "I")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a")))))) ; begin theorem :: SFMASTR1: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 "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "S"))) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "S"))) "," (Set (Var "P"))) & (Bool (Set (Var "J")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "S")) ")" ) "," (Set (Var "P")))) "holds" (Bool (Set (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J"))) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "S"))) "," (Set (Var "P")))))) ; theorem :: SFMASTR1: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")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "S"))) "," (Set (Var "P"))) & (Bool (Set (Var "J")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "S")) ")" ) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "S"))) "," (Set (Var "P"))) & (Bool (Set (Var "J")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "S")) ")" ) "," (Set (Var "P")))) "holds" (Bool (Set (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J"))) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "S"))) "," (Set (Var "P")))))) ; theorem :: SFMASTR1:4 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "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 (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "p"))) & (Bool (Set (Var "p")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s")))) "holds" (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) ")" ))) "holds" (Bool (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set (Var "m")) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) ")" ) "," (Set (Var "s")) "," (Set (Var "m")) ")" )))))) ; theorem :: SFMASTR1: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 "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "Ig")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "Ig")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "p"))) & (Bool (Set (Var "J")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ) "," (Set (Var "p"))) & (Bool (Set (Var "Ig")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "p"))) & (Bool (Set (Var "J")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ) "," (Set (Var "p")))) "holds" (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "Ig")) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "Ig")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "Ig")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "J")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "Ig")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ")" ) ")" ) ")" ")" ))))))) ; theorem :: SFMASTR1: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 "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "Ig")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "Ig")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "p"))) & (Bool (Set (Var "J")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ) "," (Set (Var "p"))) & (Bool (Set (Var "Ig")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "p"))) & (Bool (Set (Var "J")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ) "," (Set (Var "p")))) "holds" (Bool (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" (Set (Var "Ig")) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ) ($#r8_pboole :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "p")) "," (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "p")) "," (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ")" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "Ig")) ")" ) ")" ) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ")" ))))))) ; theorem :: SFMASTR1:7 (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 "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "Ig")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool "(" (Bool (Set (Var "Ig")) "is" ($#v7_amistd_1 :::"parahalting"::: ) ) "or" (Bool "(" (Bool (Set (Var "Ig")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "p"))) & (Bool (Set (Var "Ig")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "p"))) ")" ) ")" ) & (Bool "(" (Bool (Set (Var "J")) "is" ($#v7_amistd_1 :::"parahalting"::: ) ) "or" (Bool "(" (Bool (Set (Var "J")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ) "," (Set (Var "p"))) & (Bool (Set (Var "J")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ) "," (Set (Var "p"))) ")" ) ")" )) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" (Set (Var "Ig")) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "p")) "," (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))))))) ; theorem :: SFMASTR1:8 (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 "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "Ig")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "st" (Bool (Bool "(" (Bool (Set (Var "Ig")) "is" ($#v7_amistd_1 :::"parahalting"::: ) ) "or" (Bool "(" (Bool (Set (Var "Ig")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "p"))) & (Bool (Set (Var "Ig")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "p"))) ")" ) ")" ) & (Bool "(" (Bool (Set (Var "J")) "is" ($#v7_amistd_1 :::"parahalting"::: ) ) "or" (Bool "(" (Bool (Set (Var "J")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ) "," (Set (Var "p"))) & (Bool (Set (Var "J")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ) "," (Set (Var "p"))) ")" ) ")" )) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" (Set (Var "Ig")) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "p")) "," (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))))))))) ; theorem :: SFMASTR1:9 (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 "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "Ig")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool "(" (Bool (Set (Var "Ig")) "is" ($#v7_amistd_1 :::"parahalting"::: ) ) "or" (Bool "(" (Bool (Set (Var "Ig")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "p"))) & (Bool (Set (Var "Ig")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "p"))) ")" ) ")" ) & (Bool "(" (Bool (Set (Var "J")) "is" ($#v7_amistd_1 :::"parahalting"::: ) ) "or" (Bool "(" (Bool (Set (Var "J")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ) "," (Set (Var "p"))) & (Bool (Set (Var "J")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ) "," (Set (Var "p"))) ")" ) ")" )) "holds" (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" (Set (Var "Ig")) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "p")) "," (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ")" ")" ))))))) ; theorem :: SFMASTR1:10 (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 "Ig")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool "(" (Bool (Set (Var "Ig")) "is" ($#v7_amistd_1 :::"parahalting"::: ) ) "or" (Bool "(" (Bool (Set (Var "Ig")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "p"))) & (Bool (Set (Var "Ig")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "p"))) ")" ) ")" )) "holds" (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" )))))) ; theorem :: SFMASTR1:11 (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 "Ig")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "j")) "being" ($#v1_scmfsa6c :::"parahalting"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool "(" (Bool (Set (Var "Ig")) "is" ($#v7_amistd_1 :::"parahalting"::: ) ) "or" (Bool "(" (Bool (Set (Var "Ig")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "p"))) & (Bool (Set (Var "Ig")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "p"))) ")" ) ")" )) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" (Set (Var "Ig")) ($#k5_scmfsa6a :::"";""::: ) (Set (Var "j")) ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "j")) "," (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))))))) ; theorem :: SFMASTR1:12 (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 "Ig")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "j")) "being" ($#v1_scmfsa6c :::"parahalting"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "st" (Bool (Bool "(" (Bool (Set (Var "Ig")) "is" ($#v7_amistd_1 :::"parahalting"::: ) ) "or" (Bool "(" (Bool (Set (Var "Ig")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "p"))) & (Bool (Set (Var "Ig")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "p"))) ")" ) ")" )) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" (Set (Var "Ig")) ($#k5_scmfsa6a :::"";""::: ) (Set (Var "j")) ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "j")) "," (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))))))))) ; theorem :: SFMASTR1: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 "Ig")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "j")) "being" ($#v1_scmfsa6c :::"parahalting"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool "(" (Bool (Set (Var "Ig")) "is" ($#v7_amistd_1 :::"parahalting"::: ) ) "or" (Bool "(" (Bool (Set (Var "Ig")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "p"))) & (Bool (Set (Var "Ig")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "p"))) ")" ) ")" )) "holds" (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" (Set (Var "Ig")) ($#k5_scmfsa6a :::"";""::: ) (Set (Var "j")) ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "j")) "," (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "Ig")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ")" ")" ))))))) ; theorem :: SFMASTR1: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 "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#v1_scmfsa6c :::"parahalting"::: ) ($#v1_sfmastr1 :::"good"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool "(" (Bool (Set (Var "J")) "is" ($#v7_amistd_1 :::"parahalting"::: ) ) "or" (Bool "(" (Bool (Set (Var "J")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ) "," (Set (Var "p"))) & (Bool (Set (Var "J")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ) "," (Set (Var "p"))) ")" ) ")" )) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" (Set (Var "i")) ($#k4_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "p")) "," (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))))))) ; theorem :: SFMASTR1: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 "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#v1_scmfsa6c :::"parahalting"::: ) ($#v1_sfmastr1 :::"good"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "st" (Bool (Bool "(" (Bool (Set (Var "J")) "is" ($#v7_amistd_1 :::"parahalting"::: ) ) "or" (Bool "(" (Bool (Set (Var "J")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ) "," (Set (Var "p"))) & (Bool (Set (Var "J")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ) "," (Set (Var "p"))) ")" ) ")" )) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" (Set (Var "i")) ($#k4_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "p")) "," (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ")" ) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))))))))) ; theorem :: SFMASTR1:16 (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 "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#v1_scmfsa6c :::"parahalting"::: ) ($#v1_sfmastr1 :::"good"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool "(" (Bool (Set (Var "J")) "is" ($#v7_amistd_1 :::"parahalting"::: ) ) "or" (Bool "(" (Bool (Set (Var "J")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ) "," (Set (Var "p"))) & (Bool (Set (Var "J")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k2_extpro_1 :::"Exec"::: ) "(" (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 "(" (Set (Var "i")) ($#k4_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "p")) "," (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ")" ) ")" ")" ))))))) ; begin definitioncanceled; canceled; let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "p" be ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); func "n" :::"-thNotUsed"::: "p" -> ($#m1_subset_1 :::"Int-Location":::) equals :: SFMASTR1:def 4 (Set "n" ($#k9_scmfsa_m :::"-thRWNotIn"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) "p" ")" )); end; :: deftheorem SFMASTR1:def 2 : canceled; :: deftheorem SFMASTR1:def 3 : canceled; :: deftheorem defines :::"-thNotUsed"::: SFMASTR1:def 4 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set (Set (Var "n")) ($#k1_sfmastr1 :::"-thNotUsed"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k9_scmfsa_m :::"-thRWNotIn"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "p")) ")" ))))); notationlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "p" be ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); synonym "n" :::"-stNotUsed"::: "p" for "n" :::"-thNotUsed"::: "p"; synonym "n" :::"-ndNotUsed"::: "p" for "n" :::"-thNotUsed"::: "p"; synonym "n" :::"-rdNotUsed"::: "p" for "n" :::"-thNotUsed"::: "p"; end; registrationlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "p" be ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); cluster (Set "n" ($#k1_sfmastr1 :::"-thNotUsed"::: ) "p") -> ($#v1_scmfsa_m :::"read-write"::: ) ; end; begin theorem :: SFMASTR1:17 canceled; theorem :: SFMASTR1:18 canceled; theorem :: SFMASTR1:19 canceled; theorem :: SFMASTR1:20 canceled; theorem :: SFMASTR1:21 canceled; theorem :: SFMASTR1:22 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set "(" ($#k1_scmfsa6c :::"swap"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set "(" ($#k1_scmfsa6c :::"swap"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ))) ")" )) ; 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 :: SFMASTR1:def 5 (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Num 2) ($#k9_scmfsa_m :::"-ndRWNotIn"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (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"::: ) ) ")" ) ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set "(" ($#k1_scmfsa6c :::"swap"::: ) "(" "result" "," (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set ($#k5_scmfsa_m :::"{"::: ) "N" "," "result" ($#k5_scmfsa_m :::"}"::: ) ) ")" ) ")" ")" ) ")" ) ")" ) ($#k6_scmfsa_2 :::":="::: ) (Set "(" (Num 2) ($#k9_scmfsa_m :::"-ndRWNotIn"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set "(" ($#k1_scmfsa6c :::"swap"::: ) "(" "result" "," (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set ($#k5_scmfsa_m :::"{"::: ) "N" "," "result" ($#k5_scmfsa_m :::"}"::: ) ) ")" ) ")" ")" ) ")" ) ")" ) ")" ) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k2_scmfsa8c :::"Times"::: ) "(" (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set "(" ($#k1_scmfsa6c :::"swap"::: ) "(" "result" "," (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set ($#k5_scmfsa_m :::"{"::: ) "N" "," "result" ($#k5_scmfsa_m :::"}"::: ) ) ")" ) ")" ")" ) ")" ) ")" ) "," (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 2) ($#k9_scmfsa_m :::"-ndRWNotIn"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (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"::: SFMASTR1:def 5 : (Bool "for" (Set (Var "N")) "," (Set (Var "result")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set ($#k2_sfmastr1 :::"Fib_macro"::: ) "(" (Set (Var "N")) "," (Set (Var "result")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Num 2) ($#k9_scmfsa_m :::"-ndRWNotIn"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (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"::: ) ) ")" ) ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (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 "(" (Num 2) ($#k9_scmfsa_m :::"-ndRWNotIn"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (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 :::"}"::: ) ) ")" ) ")" ")" ) ")" ) ")" ) ")" ) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k2_scmfsa8c :::"Times"::: ) "(" (Set "(" (Num 1) ($#k9_scmfsa_m :::"-stRWNotIn"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (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 :::"}"::: ) ) ")" ) ")" ")" ) ")" ) ")" ) "," (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 2) ($#k9_scmfsa_m :::"-ndRWNotIn"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (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 :: SFMASTR1: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 "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 "(" ($#k2_sfmastr1 :::"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 "(" ($#k2_sfmastr1 :::"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")))) ")" ))))) ;