:: SCMFSA_9 semantic presentation begin theorem :: SCMFSA_9:1 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) "," (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 6))))) ; theorem :: SCMFSA_9:2 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) "," (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 6))))) ; definitionlet "a" be ($#m1_subset_1 :::"Int-Location":::); let "I" be ($#m1_hidden :::"Program":::) "of" ; func :::"while=0"::: "(" "a" "," "I" ")" -> ($#m1_hidden :::"Program":::) "of" equals :: SCMFSA_9:def 1 (Set (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" "a" "," (Set "(" "I" ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) "," (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) "I" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 4) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Set "(" ($#k11_scmfsa_2 :::"goto"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" )); func :::"while>0"::: "(" "a" "," "I" ")" -> ($#m1_hidden :::"Program":::) "of" equals :: SCMFSA_9:def 2 (Set (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" "a" "," (Set "(" "I" ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) "," (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) "I" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 4) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Set "(" ($#k11_scmfsa_2 :::"goto"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" )); end; :: deftheorem defines :::"while=0"::: SCMFSA_9:def 1 : (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" "holds" (Bool (Set ($#k1_scmfsa_9 :::"while=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) "," (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 4) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Set "(" ($#k11_scmfsa_2 :::"goto"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ))))); :: deftheorem defines :::"while>0"::: SCMFSA_9:def 2 : (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" "holds" (Bool (Set ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) "," (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 4) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Set "(" ($#k11_scmfsa_2 :::"goto"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ))))); theorem :: SCMFSA_9:3 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) "," (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) "," (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 11))))) ; definitionlet "a" be ($#m1_subset_1 :::"Int-Location":::); let "I" be ($#m1_hidden :::"Program":::) "of" ; func :::"while<0"::: "(" "a" "," "I" ")" -> ($#m1_hidden :::"Program":::) "of" equals :: SCMFSA_9:def 3 (Set (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" "a" "," (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) "," (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" "a" "," (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) "," (Set "(" "I" ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ")" ) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) "I" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 4) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Set "(" ($#k11_scmfsa_2 :::"goto"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" )); end; :: deftheorem defines :::"while<0"::: SCMFSA_9:def 3 : (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" "holds" (Bool (Set ($#k3_scmfsa_9 :::"while<0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) "," (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) "," (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ")" ) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 4) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Set "(" ($#k11_scmfsa_2 :::"goto"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ))))); theorem :: SCMFSA_9:4 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_scmfsa_9 :::"while=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 6))))) ; theorem :: SCMFSA_9:5 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 6))))) ; theorem :: SCMFSA_9:6 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k3_scmfsa_9 :::"while<0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 11))))) ; theorem :: SCMFSA_9:7 canceled; theorem :: SCMFSA_9:8 canceled; theorem :: SCMFSA_9:9 canceled; theorem :: SCMFSA_9:10 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k1_scmfsa_9 :::"while=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ))) & (Bool (Num 1) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k1_scmfsa_9 :::"while=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ))) & (Bool (Num 1) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ))) ")" ))) ; theorem :: SCMFSA_9:11 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_scmfsa_9 :::"while=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k12_scmfsa_2 :::"=0_goto"::: ) (Num 4))) & (Bool (Set (Set "(" ($#k1_scmfsa_9 :::"while=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_2 :::"goto"::: ) (Num 2))) & (Bool (Set (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k13_scmfsa_2 :::">0_goto"::: ) (Num 4))) & (Bool (Set (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_2 :::"goto"::: ) (Num 2))) ")" ))) ; theorem :: SCMFSA_9:12 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Num 6))) "holds" (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k1_scmfsa_9 :::"while=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" )))))) ; theorem :: SCMFSA_9:13 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Num 6))) "holds" (Bool (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k1_scmfsa_9 :::"while=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" )))))) ; theorem :: SCMFSA_9:14 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" "holds" (Bool (Set (Set "(" ($#k1_scmfsa_9 :::"while=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 5) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))))) ; theorem :: SCMFSA_9:15 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" "holds" (Bool (Set (Set "(" ($#k1_scmfsa_9 :::"while=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_2 :::"goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 5) ")" ))))) ; theorem :: SCMFSA_9:16 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" "holds" (Bool (Set (Set "(" ($#k1_scmfsa_9 :::"while=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_2 :::"goto"::: ) (Num 3))))) ; theorem :: SCMFSA_9:17 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (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 "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 6)))) "holds" (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k1_scmfsa_9 :::"while=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" )))))) ; theorem :: SCMFSA_9: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 "I")) "being" ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "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 :: SCMFSA_9:19 (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" (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "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 (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 (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" )) & (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (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 "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set (Var "k")) ")" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 4))) & (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 "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ) ")" ")" )) ($#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 (Var "k")) ")" ")" )))) "holds" (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (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 "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 4))) & (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 "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )) ($#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 "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ))) ")" )))))) ; theorem :: SCMFSA_9:20 (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" (Bool "for" (Set (Var "s")) "being" ($#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")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (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 "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_memstr_0 :::"IC"::: ) (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")) ")" ) ")" ")" ) ")" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 4)))) "holds" (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_scmfsa_9 :::"while=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ")" ) "," (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 "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_2 :::"goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 4) ")" ))))))) ; theorem :: SCMFSA_9:21 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" "holds" (Bool (Set (Set "(" ($#k1_scmfsa_9 :::"while=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 4) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_2 :::"goto"::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: SCMFSA_9: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 "I")) "being" ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "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 "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (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_numbers :::"0"::: ) )) & (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 "(" ($#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)))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (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 (Var "k")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k1_scmfsa_9 :::"while=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ))) ")" ) ")" ))))) ; definitionlet "s" be ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "I" be ($#m1_hidden :::"Program":::) "of" ; let "a" be ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::); let "P" be ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); func :::"StepWhile=0"::: "(" "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"::: ) ) ")" ) ")" ) means :: SCMFSA_9:def 4 (Bool "(" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r6_pboole :::"="::: ) "s") & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r6_pboole :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" "P" ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_scmfsa_9 :::"while=0"::: ) "(" "a" "," "I" ")" ")" ) ")" ) "," (Set "(" (Set "(" it ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ")" ) ")" ) "," (Set "(" (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set "(" "P" ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_scmfsa_9 :::"while=0"::: ) "(" "a" "," "I" ")" ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) "I" ")" ) "," (Set "(" (Set "(" it ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ")" ) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"StepWhile=0"::: SCMFSA_9:def 4 : (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" (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "b5")) "being" ($#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"::: ) ) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k4_scmfsa_9 :::"StepWhile=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" )) "iff" (Bool "(" (Bool (Set (Set (Var "b5")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r6_pboole :::"="::: ) (Set (Var "s"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b5")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r6_pboole :::"="::: ) (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 "(" (Set "(" (Set (Var "b5")) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ")" ) ")" ) "," (Set "(" (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_scmfsa_9 :::"while=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" (Set "(" (Set (Var "b5")) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ")" ) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" )) ")" ) ")" ) ")" )))))); theorem :: SCMFSA_9: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 "I")) "being" ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (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) ")" )) ($#r6_pboole :::"="::: ) (Set (Set "(" ($#k4_scmfsa_9 :::"StepWhile=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "P")) "," (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")) ")" ) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Num 1)))))))) ; theorem :: SCMFSA_9:24 canceled; theorem :: SCMFSA_9:25 (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" (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set (Set "(" ($#k4_scmfsa_9 :::"StepWhile=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r6_pboole :::"="::: ) (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 "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_scmfsa_9 :::"while=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" )))))) ; theorem :: SCMFSA_9:26 (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" (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (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")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (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"))) ($#r6_pboole :::"="::: ) (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 (Var "n")) ")" ))) "holds" (Bool "(" (Bool (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"))) ($#r6_pboole :::"="::: ) (Set ($#k8_memstr_0 :::"Initialize"::: ) (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")) ")" ))) & (Bool (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) ")" )) ($#r6_pboole :::"="::: ) (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 (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_scmfsa_9 :::"while=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (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")) ")" ) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ) ")" )) ")" )))))) ; theorem :: SCMFSA_9:27 (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" (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "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")) ")" ")" ))) ")" ) ")" ) & (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" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (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")) ($#k1_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 (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")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & "(" (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 (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (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 (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"::: ) ))) "implies" (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 (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )))) "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 :: SCMFSA_9:28 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v7_amistd_1 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (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" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (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")) ($#k1_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 (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")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & "(" (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 (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (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 (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"::: ) ))) "implies" (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 (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )))) "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 :: SCMFSA_9:29 (Bool "for" (Set (Var "I")) "being" ($#v7_amistd_1 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (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 "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"::: ) ) "holds" (Bool "(" (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 :::"."::: ) (Num 1) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) "or" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & "(" (Bool (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" ))))) "holds" (Bool (Set ($#k1_scmfsa_9 :::"while=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ) "is" ($#v7_amistd_1 :::"parahalting"::: ) ))) ; theorem :: SCMFSA_9:30 (Bool "for" (Set (Var "l1")) "," (Set (Var "l2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Bool "not" (Set (Set (Var "l1")) ($#k16_funcop_1 :::".-->"::: ) (Set "(" ($#k11_scmfsa_2 :::"goto"::: ) (Set (Var "l2")) ")" )) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a")))))) ; theorem :: SCMFSA_9:31 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Bool "not" (Set (Var "i")) ($#r3_scmfsa7b :::"destroys"::: ) (Set ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ))))) "holds" (Bool (Set ($#k11_compos_1 :::"Macro"::: ) (Set (Var "i"))) "is" ($#v1_scmfsa7b :::"good"::: ) )) ; registrationlet "I", "J" be ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" ; let "a" be ($#m1_subset_1 :::"Int-Location":::); cluster (Set ($#k1_scmfsa8b :::"if=0"::: ) "(" "a" "," "I" "," "J" ")" ) -> ($#v1_scmfsa7b :::"good"::: ) ; end; registrationlet "I" be ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" ; let "a" be ($#m1_subset_1 :::"Int-Location":::); cluster (Set ($#k1_scmfsa_9 :::"while=0"::: ) "(" "a" "," "I" ")" ) -> ($#v1_scmfsa7b :::"good"::: ) ; end; theorem :: SCMFSA_9:32 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Num 6))) "holds" (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" )))))) ; theorem :: SCMFSA_9:33 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Num 6))) "holds" (Bool (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" )))))) ; theorem :: SCMFSA_9:34 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" "holds" (Bool (Set (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 5) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))))) ; theorem :: SCMFSA_9:35 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" "holds" (Bool (Set (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_2 :::"goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 5) ")" ))))) ; theorem :: SCMFSA_9:36 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" "holds" (Bool (Set (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_2 :::"goto"::: ) (Num 3))))) ; theorem :: SCMFSA_9:37 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (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 "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 6)))) "holds" (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" )))))) ; theorem :: SCMFSA_9:38 (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" (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "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 :: SCMFSA_9:39 (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" (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "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 (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 (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" )) & (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (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 "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set (Var "k")) ")" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 4))) & (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 "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ) ")" ")" )) ($#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 (Var "k")) ")" ")" )))) "holds" (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (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 "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 4))) & (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 "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ")" ) ")" ) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ))) ")" )))))) ; theorem :: SCMFSA_9:40 (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" (Bool "for" (Set (Var "s")) "being" ($#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")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (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 "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_memstr_0 :::"IC"::: ) (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")) ")" ) ")" ")" ) ")" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 4)))) "holds" (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ")" ) "," (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 "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_2 :::"goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 4) ")" ))))))) ; theorem :: SCMFSA_9:41 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" "holds" (Bool (Set (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 4) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_2 :::"goto"::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: SCMFSA_9: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 "I")) "being" ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "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 "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (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_numbers :::"0"::: ) )) & (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 "(" ($#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)))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (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 (Var "k")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ))) ")" ) ")" ))))) ; definitionlet "s" be ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "I" be ($#m1_hidden :::"Program":::) "of" ; let "a" be ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::); let "P" be ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); func :::"StepWhile>0"::: "(" "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"::: ) ) ")" ) ")" ) means :: SCMFSA_9:def 5 (Bool "(" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r6_pboole :::"="::: ) "s") & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r6_pboole :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" "P" ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" "a" "," "I" ")" ")" ) ")" ) "," (Set "(" (Set "(" it ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ")" ) ")" ) "," (Set "(" (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set "(" "P" ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" "a" "," "I" ")" ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) "I" ")" ) "," (Set "(" (Set "(" it ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ")" ) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"StepWhile>0"::: SCMFSA_9:def 5 : (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" (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "b5")) "being" ($#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"::: ) ) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k5_scmfsa_9 :::"StepWhile>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" )) "iff" (Bool "(" (Bool (Set (Set (Var "b5")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r6_pboole :::"="::: ) (Set (Var "s"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b5")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r6_pboole :::"="::: ) (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 "(" (Set "(" (Set (Var "b5")) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ")" ) ")" ) "," (Set "(" (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" (Set "(" (Set (Var "b5")) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ")" ) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" )) ")" ) ")" ) ")" )))))); theorem :: SCMFSA_9:43 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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" (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (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) ")" )) ($#r6_pboole :::"="::: ) (Set (Set "(" ($#k5_scmfsa_9 :::"StepWhile>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "P")) "," (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")) ")" ) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Num 1)))))))) ; theorem :: SCMFSA_9:44 (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" (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set (Set "(" ($#k5_scmfsa_9 :::"StepWhile>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r6_pboole :::"="::: ) (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 "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" )))))) ; theorem :: SCMFSA_9:45 (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" (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (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")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (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"))) ($#r6_pboole :::"="::: ) (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 (Var "n")) ")" ))) "holds" (Bool "(" (Bool (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"))) ($#r6_pboole :::"="::: ) (Set ($#k8_memstr_0 :::"Initialize"::: ) (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")) ")" ))) & (Bool (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) ")" )) ($#r6_pboole :::"="::: ) (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 (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (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")) ")" ) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ) ")" )) ")" )))))) ; theorem :: SCMFSA_9:46 (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" (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "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")) ")" ")" ))) ")" ) ")" ) & (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" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (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")) ($#k1_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 (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")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & "(" (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 (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (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 (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"::: ) ))) "implies" (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 (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )))) "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 :: SCMFSA_9:47 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v7_amistd_1 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (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" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (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")) ($#k1_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 (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")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & "(" (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 (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (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 (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"::: ) ))) "implies" (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 (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )))) "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 :: SCMFSA_9:48 (Bool "for" (Set (Var "I")) "being" ($#v7_amistd_1 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (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 "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"::: ) ) "holds" (Bool "(" (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 :::"."::: ) (Num 1) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) "or" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & "(" (Bool (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" ))))) "holds" (Bool (Set ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ) "is" ($#v7_amistd_1 :::"parahalting"::: ) ))) ; registrationlet "I", "J" be ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" ; let "a" be ($#m1_subset_1 :::"Int-Location":::); cluster (Set ($#k2_scmfsa8b :::"if>0"::: ) "(" "a" "," "I" "," "J" ")" ) -> ($#v1_scmfsa7b :::"good"::: ) ; end; registrationlet "I" be ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" ; let "a" be ($#m1_subset_1 :::"Int-Location":::); cluster (Set ($#k2_scmfsa_9 :::"while>0"::: ) "(" "a" "," "I" ")" ) -> ($#v1_scmfsa7b :::"good"::: ) ; end;