:: SCMFSA8C semantic presentation begin theorem :: SCMFSA8C:1 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (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 "n")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set (Var "I")))) ")" )) "holds" (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k2_scmfsa8a :::"pseudo-LifeSpan"::: ) "(" (Set (Var "s")) "," (Set (Var "P")) "," (Set (Var "I")) ")" )))))) ; theorem :: SCMFSA8C:2 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "I"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" )))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "J")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ")" ))))) ; theorem :: SCMFSA8C:3 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ))))) ; theorem :: SCMFSA8C:4 canceled; theorem :: SCMFSA8C:5 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (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 (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "P")))) ")" )) "holds" (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Num 1) ")" )) "is" (Set (Var "I")) ($#v5_extpro_1 :::"-halted"::: ) )) ; theorem :: SCMFSA8C:6 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (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 (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "P")))) ")" )) "holds" (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Num 1) ")" )) "is" (Set (Var "I")) ($#v5_extpro_1 :::"-halted"::: ) )) ; theorem :: SCMFSA8C:7 canceled; theorem :: SCMFSA8C:8 canceled; theorem :: SCMFSA8C:9 canceled; theorem :: SCMFSA8C:10 canceled; theorem :: SCMFSA8C:11 canceled; theorem :: SCMFSA8C:12 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 6) "," (Num 7) "," (Num 8) ($#k2_enumset1 :::"}"::: ) ))) "holds" (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "i")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s")))))) ; theorem :: SCMFSA8C:13 canceled; theorem :: SCMFSA8C: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"::: ) ) "holds" (Bool (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")))))) ; theorem :: SCMFSA8C: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 "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set (Var "I"))))))) ; theorem :: SCMFSA8C:16 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s1")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Var "s1")) "," (Set (Var "P1"))) & (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "P1")))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "I")) "," (Set (Var "n")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P2"))) & (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s2"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s2"))))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ))) & (Bool (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set "(" ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P1")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ")" ")" ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P2")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ")" )) & (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ))) ")" ))))))) ; theorem :: SCMFSA8C:17 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Var "s1")) "," (Set (Var "P1"))) & (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "P2"))) & (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s2"))))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ))) & (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P1")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P2")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ")" )) & (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ))) ")" ))))) ; theorem :: SCMFSA8C:18 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Var "s1")) "," (Set (Var "P1"))) & (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set (Var "s1")) "," (Set (Var "P1"))) & (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "P2"))) & (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s2"))))) "holds" (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) ")" ))))) ; theorem :: SCMFSA8C:19 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Var "s1")) "," (Set (Var "P1"))) & (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set (Var "s1")) "," (Set (Var "P1"))) & (Bool "(" "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s2")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Set (Var "s1")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s2")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")))) ")" )) "holds" (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P1")) "," (Set (Var "s1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P2")) "," (Set (Var "s2")) ")" ")" )))))) ; theorem :: SCMFSA8C:20 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Var "s1")) "," (Set (Var "P1"))) & (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set (Var "s1")) "," (Set (Var "P1"))) & (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s2"))))) "holds" (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P1")) "," (Set (Var "s1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P2")) "," (Set (Var "s2")) ")" ")" )))))) ; theorem :: SCMFSA8C:21 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool "(" (Bool (Set (Var "I")) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s"))) "," (Set (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")))) & (Bool (Set ($#k2_scmfsa8a :::"pseudo-LifeSpan"::: ) "(" (Set (Var "s")) "," (Set (Var "P")) "," (Set (Var "I")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_scmfsa8a :::"pseudo-LifeSpan"::: ) "(" (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set (Var "I")) ")" )) ")" )))) ; theorem :: SCMFSA8C:22 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s1")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "I")) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set (Var "s1")) "," (Set (Var "P1")))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "I")) "," (Set (Var "n")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P2"))) & (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s2"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s2"))))) "holds" (Bool "(" (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k2_scmfsa8a :::"pseudo-LifeSpan"::: ) "(" (Set (Var "s1")) "," (Set (Var "P1")) "," (Set (Var "I")) ")" ))) "holds" (Bool (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set "(" ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P1")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ")" ")" ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P2")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ")" )) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_scmfsa8a :::"pseudo-LifeSpan"::: ) "(" (Set (Var "s1")) "," (Set (Var "P1")) "," (Set (Var "I")) ")" ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ))) & (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ))) ")" ) ")" ) ")" )))))) ; theorem :: SCMFSA8C:23 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s2")))) & (Bool (Set (Var "I")) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set (Var "s1")) "," (Set (Var "P1")))) "holds" (Bool (Set (Var "I")) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set (Var "s2")) "," (Set (Var "P2")))))) ; theorem :: SCMFSA8C:24 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Var "I")) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) "iff" (Bool (Set (Var "I")) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "P"))) ")" )))) ; theorem :: SCMFSA8C:25 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ))) & (Bool (Num 1) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ))) & (Bool (Num 1) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ))) ")" ))) ; theorem :: SCMFSA8C:26 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k12_scmfsa_2 :::"=0_goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ))) & (Bool (Set (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_2 :::"goto"::: ) (Num 2))) & (Bool (Set (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k13_scmfsa_2 :::">0_goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ))) & (Bool (Set (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_2 :::"goto"::: ) (Num 2))) ")" ))) ; theorem :: SCMFSA8C:27 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3)))) "holds" (Bool "(" (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ))) & (Bool (Set (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"<>"::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))) ")" )))) ; theorem :: SCMFSA8C:28 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3)))) "holds" (Bool "(" (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ))) & (Bool (Set (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"<>"::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))) ")" )))) ; theorem :: SCMFSA8C:29 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "I"))) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool "(" (Bool (Set (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" )) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" )) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_scmfsa8a :::"pseudo-LifeSpan"::: ) "(" (Set (Var "s")) "," (Set (Var "P")) "," (Set "(" ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "I")) ")" ) ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k2_scmfsa8a :::"pseudo-LifeSpan"::: ) "(" (Set (Var "s")) "," (Set (Var "P")) "," (Set "(" ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "I")) ")" ) ")" ))) "holds" (Bool (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 "n")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set (Var "n")) ")" ")" ))) ")" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_scmfsa8a :::"pseudo-LifeSpan"::: ) "(" (Set (Var "s")) "," (Set (Var "P")) "," (Set "(" ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "I")) ")" ) ")" ))) "holds" (Bool (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 "n")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set (Var "n")) ")" ")" ))) ")" ) ")" )))) ; theorem :: SCMFSA8C:30 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "I"))) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" )) ($#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 "(" ($#k2_scmfsa8a :::"pseudo-LifeSpan"::: ) "(" (Set (Var "s")) "," (Set (Var "P")) "," (Set "(" ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "I")) ")" ) ")" ")" ) ")" ")" )))))) ; theorem :: SCMFSA8C:31 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "I"))) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set "(" ($#k2_scmfsa8a :::"pseudo-LifeSpan"::: ) "(" (Set (Var "s")) "," (Set (Var "P")) "," (Set "(" ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "I")) ")" ) ")" ")" ) ")" ")" )))))) ; theorem :: SCMFSA8C:32 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))))) ; theorem :: SCMFSA8C:33 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))))) ; theorem :: SCMFSA8C:34 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_2 :::"goto"::: ) (Set "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ))))) ; theorem :: SCMFSA8C:35 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_2 :::"goto"::: ) (Set "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ))))) ; theorem :: SCMFSA8C:36 (Bool "for" (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Num 2) ")" ) "," (Set (Var "J")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_2 :::"goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 5) ")" ))))) ; theorem :: SCMFSA8C:37 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (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"::: ) )) & (Bool (Set ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "I"))) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool "(" (Bool (Set ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) ")" ))))) ; theorem :: SCMFSA8C: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")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (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 "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "I"))) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ))))))) ; theorem :: SCMFSA8C:39 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (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"::: ) )) & (Bool (Set ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "I"))) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool "(" (Bool (Set ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) ")" ))))) ; theorem :: SCMFSA8C:40 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (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 "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "I"))) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ))))))) ; theorem :: SCMFSA8C:41 (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"::: ) ) (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"::: ) )) & (Bool (Set ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "J"))) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool "(" (Bool (Set ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "J")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3))) ")" ))))) ; theorem :: SCMFSA8C: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")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (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 "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "J"))) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" (Set (Var "J")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ))))))) ; theorem :: SCMFSA8C:43 (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"::: ) ) (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"::: ) )) & (Bool (Set ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "J"))) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool "(" (Bool (Set ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "J")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3))) ")" ))))) ; theorem :: SCMFSA8C:44 (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"::: ) ) (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 "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "J"))) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" (Set (Var "J")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ))))))) ; theorem :: SCMFSA8C:45 (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"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "I"))) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "J"))) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool "(" (Bool (Set ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" ))))) ; theorem :: SCMFSA8C:46 (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"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "I"))) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "J"))) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool "(" (Bool (Set ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" ))))) ; theorem :: SCMFSA8C:47 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Bool "not" (Set (Var "I")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a"))))) "holds" (Bool "not" (Bool (Set ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "I"))) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a")))))) ; theorem :: SCMFSA8C:48 (Bool "for" (Set (Var "i")) "being" ($#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 "not" (Set (Var "i")) ($#r3_scmfsa7b :::"destroys"::: ) (Set (Var "a"))))) "holds" (Bool "not" (Bool (Set ($#k11_compos_1 :::"Macro"::: ) (Set (Var "i"))) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a")))))) ; theorem :: SCMFSA8C:49 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Bool "not" (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )) ($#r1_scmfsa7b :::"refers"::: ) (Set (Var "a"))))) ; theorem :: SCMFSA8C:50 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool "not" (Bool (Set ($#k7_scmfsa_2 :::"AddTo"::: ) "(" (Set (Var "c")) "," (Set (Var "b")) ")" ) ($#r1_scmfsa7b :::"refers"::: ) (Set (Var "a"))))) ; theorem :: SCMFSA8C:51 (Bool "for" (Set (Var "i")) "being" ($#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 "not" (Set (Var "i")) ($#r1_scmfsa7b :::"refers"::: ) (Set (Var "a"))))) "holds" (Bool "not" (Bool (Set ($#k11_compos_1 :::"Macro"::: ) (Set (Var "i"))) ($#r2_scmfsa7b :::"refers"::: ) (Set (Var "a")))))) ; theorem :: SCMFSA8C:52 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Bool "not" (Set (Var "I")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a")))) & (Bool (Bool "not" (Set (Var "J")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a"))))) "holds" (Bool "not" (Bool (Set (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J"))) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a")))))) ; theorem :: SCMFSA8C:53 (Bool "for" (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#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 "not" (Set (Var "i")) ($#r3_scmfsa7b :::"destroys"::: ) (Set (Var "a")))) & (Bool (Bool "not" (Set (Var "J")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a"))))) "holds" (Bool "not" (Bool (Set (Set (Var "i")) ($#k4_scmfsa6a :::"";""::: ) (Set (Var "J"))) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a"))))))) ; theorem :: SCMFSA8C:54 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "j")) "being" ($#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 "not" (Set (Var "I")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a")))) & (Bool (Bool "not" (Set (Var "j")) ($#r3_scmfsa7b :::"destroys"::: ) (Set (Var "a"))))) "holds" (Bool "not" (Bool (Set (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set (Var "j"))) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a"))))))) ; theorem :: SCMFSA8C:55 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#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 "not" (Set (Var "i")) ($#r3_scmfsa7b :::"destroys"::: ) (Set (Var "a")))) & (Bool (Bool "not" (Set (Var "j")) ($#r3_scmfsa7b :::"destroys"::: ) (Set (Var "a"))))) "holds" (Bool "not" (Bool (Set (Set (Var "i")) ($#k6_scmfsa6a :::"";""::: ) (Set (Var "j"))) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a")))))) ; theorem :: SCMFSA8C:56 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Bool "not" (Set ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a"))))) ; theorem :: SCMFSA8C:57 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "l")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Bool "not" (Set ($#k1_scmfsa8a :::"Goto"::: ) (Set (Var "l"))) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a")))))) ; theorem :: SCMFSA8C:58 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "P")))) "holds" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ) "," (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ) ")" ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ) "," (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ) ")" ")" ) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")))) ")" ) ")" )))) ; theorem :: SCMFSA8C:59 (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" ($#v7_amistd_1 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ) "," (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ) ")" ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))))))) ; theorem :: SCMFSA8C:60 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (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 ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "P"))) & (Bool (Bool "not" (Set (Var "I")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a"))))) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))))))) ; theorem :: SCMFSA8C:61 (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" ($#v7_amistd_1 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Bool "not" (Set (Var "I")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a"))))) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))))))) ; theorem :: SCMFSA8C:62 (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" ($#v7_amistd_1 :::"parahalting"::: ) ($#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 "not" (Set (Var "I")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a"))))) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))))))) ; theorem :: SCMFSA8C:63 (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" ($#v1_scmfsa6b :::"keeping_0"::: ) ($#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")))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ")" )))) ; theorem :: SCMFSA8C:64 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Bool "not" (Set (Var "I")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a"))))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (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")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set (Var "I"))))) "holds" (Bool (Set (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) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (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")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))))))) ; theorem :: SCMFSA8C:65 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Bool "not" (Set (Var "I")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a"))))) "holds" (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool (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 "n")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set (Var "I")))) ")" )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set (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 "n")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))))))))) ; theorem :: SCMFSA8C:66 (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" ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool (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 "n")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set (Var "I")))) ")" )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set (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 "n")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )))))))) ; theorem :: SCMFSA8C:67 (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" ($#v1_scmfsa7b :::"good"::: ) ($#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")))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ")" )))) ; theorem :: SCMFSA8C:68 (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" ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (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")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))))))) ; theorem :: SCMFSA8C:69 (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" ($#v1_scmfsa6b :::"keeping_0"::: ) ($#v7_amistd_1 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Bool "not" (Set (Var "I")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a"))))) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ) "," (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ) ")" ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))))))) ; theorem :: SCMFSA8C:70 (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"::: ) )) ; theorem :: SCMFSA8C:71 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Var "s1")) "," (Set (Var "P1"))) & (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set (Var "s1")) "," (Set (Var "P1"))) & (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s2"))))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P1")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s1")) ")" ) "," (Set (Var "k")) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P2")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s2")) ")" ) "," (Set (Var "k")) ")" )) & (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set "(" (Set (Var "P1")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P1")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s1")) ")" ) "," (Set (Var "k")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set "(" (Set (Var "P2")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P2")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s2")) ")" ) "," (Set (Var "k")) ")" ")" ) ")" )) ")" ))))) ; theorem :: SCMFSA8C:72 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Var "s1")) "," (Set (Var "P1"))) & (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set (Var "s1")) "," (Set (Var "P1"))) & (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s2"))))) "holds" (Bool "(" (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P1")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s1")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P2")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s2")) ")" ) ")" )) & (Bool (Set ($#k6_extpro_1 :::"Result"::: ) "(" (Set "(" (Set (Var "P1")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s1")) ")" ) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k6_extpro_1 :::"Result"::: ) "(" (Set "(" (Set (Var "P2")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s2")) ")" ) ")" )) ")" )))) ; theorem :: SCMFSA8C:73 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Var "s1")) "," (Set (Var "P1"))) & (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set (Var "s1")) "," (Set (Var "P1"))) & (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "P2"))) & (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "k")) ")" ) ($#r8_pboole :::"="::: ) (Set (Var "s2"))))) "holds" (Bool (Set ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) ")" ))))) ; begin definitionlet "I" be ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); func :::"loop"::: "I" -> ($#v2_compos_1 :::"halt-free"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) equals :: SCMFSA8C:def 1 (Set ($#k1_scmfsa6a :::"Directed"::: ) "(" "I" "," (Set ($#k6_numbers :::"0"::: ) ) ")" ); end; :: deftheorem defines :::"loop"::: SCMFSA8C:def 1 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set ($#k1_scmfsa8c :::"loop"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set ($#k1_scmfsa6a :::"Directed"::: ) "(" (Set (Var "I")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ))); theorem :: SCMFSA8C:74 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set ($#k1_scmfsa8c :::"loop"::: ) (Set (Var "I"))) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a")))) "holds" (Bool (Set (Var "I")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a"))))) ; registrationlet "I" be ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); cluster (Set ($#k1_scmfsa8c :::"loop"::: ) "I") -> ($#v2_compos_1 :::"halt-free"::: ) ($#v1_scmfsa7b :::"good"::: ) ; end; theorem :: SCMFSA8C:75 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Bool "not" (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_scmfsa8c :::"loop"::: ) (Set (Var "I")) ")" ))))) ; theorem :: SCMFSA8C:76 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "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")))) "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 "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ))) "holds" (Bool (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 "m")) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_scmfsa8c :::"loop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set (Var "m")) ")" )))))) ; theorem :: SCMFSA8C:77 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "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")))) "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 "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ))) "holds" (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (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 "m")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_scmfsa8c :::"loop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_scmfsa8c :::"loop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set (Var "m")) ")" ")" ) ")" )))))) ; theorem :: SCMFSA8C:78 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "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")))) "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 "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ))) "holds" (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_scmfsa8c :::"loop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_scmfsa8c :::"loop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set (Var "m")) ")" ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))))))) ; theorem :: SCMFSA8C:79 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "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")))) "holds" (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_scmfsa8c :::"loop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_scmfsa8c :::"loop"::: ) (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")) ")" ) ")" ")" ) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_2 :::"goto"::: ) (Set ($#k6_numbers :::"0"::: ) )))))) ; theorem :: SCMFSA8C:80 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "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"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v6_amistd_1 :::"paraclosed"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (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 "(" ($#k1_scmfsa8c :::"loop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set (Var "s")) "," (Set (Var "m")) ")" )))))) ; theorem :: SCMFSA8C:81 (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" ($#v7_amistd_1 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "s"))) & (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) ")" ))) "holds" (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_scmfsa8c :::"loop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_scmfsa8c :::"loop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))))))) ; begin definitionlet "a" be ($#m1_subset_1 :::"Int-Location":::); let "I" be ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); func :::"Times"::: "(" "a" "," "I" ")" -> ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) equals :: SCMFSA8C:def 2 (Set ($#k2_scmfsa8b :::"if>0"::: ) "(" "a" "," (Set "(" ($#k1_scmfsa8c :::"loop"::: ) (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" "a" "," (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Num 2) ")" ) "," (Set "(" "I" ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" "a" "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ) "," (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ); end; :: deftheorem defines :::"Times"::: SCMFSA8C:def 2 : (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set ($#k2_scmfsa8c :::"Times"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k1_scmfsa8c :::"loop"::: ) (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Num 2) ")" ) "," (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ) "," (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" )))); registrationlet "a" be ($#m1_subset_1 :::"Int-Location":::); let "I" be ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); cluster (Set ($#k2_scmfsa8c :::"Times"::: ) "(" "a" "," "I" ")" ) -> ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ; end; theorem :: SCMFSA8C:82 (Bool "for" (Set (Var "I")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Num 2) ")" ) "," (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ")" ) "is" ($#v1_scmfsa7b :::"good"::: ) ))) ; theorem :: SCMFSA8C:83 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Num 2) ")" ) "," (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_2 :::"goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 5) ")" ))))) ; theorem :: SCMFSA8C:84 (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" ($#v1_scmfsa7b :::"good"::: ) ($#v7_amistd_1 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Bool "not" (Set (Var "I")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a")))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_scmfsa8c :::"loop"::: ) (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Num 2) ")" ) "," (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ")" ")" )) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))))))) ; theorem :: SCMFSA8C:85 (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" ($#v1_scmfsa7b :::"good"::: ) ($#v7_amistd_1 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Bool "not" (Set (Var "I")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a")))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_scmfsa8c :::"loop"::: ) (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Num 2) ")" ) "," (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ")" ")" )) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "P"))))))) ; theorem :: SCMFSA8C:86 (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" ($#v1_scmfsa7b :::"good"::: ) ($#v7_amistd_1 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Bool "not" (Set (Var "I")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a")))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool "(" (Bool (Set ($#k2_scmfsa8c :::"Times"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k2_scmfsa8c :::"Times"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" ))))) ; theorem :: SCMFSA8C:87 (Bool "for" (Set (Var "I")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#v7_amistd_1 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Bool "not" (Set (Var "I")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a"))))) "holds" (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Num 1) ")" )) "is" (Set ($#k2_scmfsa8c :::"Times"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ) ($#v5_extpro_1 :::"-halted"::: ) ))) ; theorem :: SCMFSA8C:88 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Bool "not" (Set (Var "I")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "c")))) & (Bool (Bool "not" (Set (Var "J")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "c"))))) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "c")))) & (Bool (Bool "not" (Set ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "c")))) ")" ))) ; theorem :: SCMFSA8C:89 (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" ($#v1_scmfsa7b :::"good"::: ) ($#v7_amistd_1 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Bool "not" (Set (Var "I")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a")))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )(Bool "ex" (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )(Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "s2")) ($#r8_pboole :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ")" ))) & (Bool (Set (Var "P2")) ($#r8_pboole :::"="::: ) (Set (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_scmfsa8c :::"loop"::: ) (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Num 2) ")" ) "," (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ))) & (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Num 2) ")" ) "," (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ")" ) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) & (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "b")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "k")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")))) ")" ) & (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "k")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "n")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k1_scmfsa8c :::"loop"::: ) (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Num 2) ")" ) "," (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ))) ")" ) ")" )))))))) ; theorem :: SCMFSA8C:90 (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" ($#v1_scmfsa7b :::"good"::: ) ($#v7_amistd_1 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (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 "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa8c :::"Times"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s")))))))) ; theorem :: SCMFSA8C:91 (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" ($#v1_scmfsa7b :::"good"::: ) ($#v7_amistd_1 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Bool "not" (Set (Var "I")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a")))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) & (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa8c :::"Times"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa8c :::"Times"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ")" ")" ))) ")" ))))) ; begin theorem :: SCMFSA8C:92 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa8c :::"Times"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k11_compos_1 :::"Macro"::: ) (Set "(" ($#k7_scmfsa_2 :::"AddTo"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ")" )))))) ;