:: SCMPDS_7 semantic presentation begin theorem :: SCMPDS_7:1 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k17_scmpds_2 :::"ICplusConst"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "n")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "m")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "n"))))) ; theorem :: SCMPDS_7:2 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "i")) ($#k2_scmpds_4 :::"';'"::: ) (Set (Var "I")) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set (Var "j")) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k2_scmpds_4 :::"';'"::: ) (Set "(" (Set "(" (Set (Var "I")) ($#k3_scmpds_4 :::"';'"::: ) (Set (Var "j")) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set (Var "k")) ")" ))))) ; theorem :: SCMPDS_7:3 (Bool "for" (Set (Var "J")) "," (Set (Var "I")) "," (Set (Var "K")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k61_valued_1 :::"Shift"::: ) "(" (Set (Var "J")) "," (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J")) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "K"))))) ; theorem :: SCMPDS_7:4 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set ($#k10_compos_1 :::"stop"::: ) (Set "(" (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J")) ")" )))) ; theorem :: SCMPDS_7:5 canceled; theorem :: SCMPDS_7:6 canceled; theorem :: SCMPDS_7:7 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 4) "," (Num 5) "," (Num 6) "," (Num 14) ($#k3_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 :: SCMPDS_7:8 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_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 "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s1")) ")" ) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P2")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (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 "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P1")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (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 "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P2")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s2")) ")" ) "," (Set (Var "k")) ")" ")" ) ")" )) ")" ))))) ; theorem :: SCMPDS_7:9 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P1"))) & (Bool (Set ($#k10_compos_1 :::"stop"::: ) (Set (Var "I"))) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set ($#k10_compos_1 :::"stop"::: ) (Set (Var "I"))) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "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 (Var "P1")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s")) "," (Set (Var "k")) ")" )) & (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P1")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P2")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" )) ")" ))))) ; theorem :: SCMPDS_7:10 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P1"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P1"))) & (Bool (Set ($#k10_compos_1 :::"stop"::: ) (Set (Var "I"))) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set ($#k10_compos_1 :::"stop"::: ) (Set (Var "I"))) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "holds" (Bool "(" (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "P1")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "P2")) "," (Set (Var "s")) ")" )) & (Bool (Set ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "P1")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "P2")) "," (Set (Var "s")) ")" )) ")" )))) ; theorem :: SCMPDS_7:11 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s1")) "," (Set (Var "P1"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"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 "(" ($#k10_compos_1 :::"stop"::: ) (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 "(" ($#k10_compos_1 :::"stop"::: ) (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 "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s1")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_extpro_1 :::"Result"::: ) "(" (Set "(" (Set (Var "P2")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s2")) ")" ) ")" )) ")" )))) ; theorem :: SCMPDS_7:12 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s1")) "," (Set (Var "P1"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s1")) "," (Set (Var "P1"))) & (Bool (Set ($#k10_compos_1 :::"stop"::: ) (Set (Var "I"))) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set ($#k10_compos_1 :::"stop"::: ) (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")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "s2"))))) "holds" (Bool (Set ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) ")" ))))) ; theorem :: SCMPDS_7:13 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (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 "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))))))) ; theorem :: SCMPDS_7:14 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scmpds_4 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (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 "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))))))) ; theorem :: SCMPDS_7:15 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k10_compos_1 :::"stop"::: ) (Set (Var "I"))) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) ")" ))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "i")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set (Var "I")))))))) ; theorem :: SCMPDS_7:16 (Bool "for" (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s1")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set ($#k10_compos_1 :::"stop"::: ) (Set (Var "I"))) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s1")) "," (Set (Var "P1"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_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 ($#k61_valued_1 :::"Shift"::: ) "(" (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"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) ")" ))) "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 ($#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 :: SCMPDS_7:17 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set ($#k10_compos_1 :::"stop"::: ) (Set (Var "I"))) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) ")" ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: SCMPDS_7:18 (Bool "for" (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s1")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set ($#k10_compos_1 :::"stop"::: ) (Set (Var "I"))) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s1")) "," (Set (Var "P1"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_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 ($#k61_valued_1 :::"Shift"::: ) "(" (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 (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) ")" ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")))) & (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) ")" ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) ")" ")" ) ")" ")" ))) ")" )))))) ; theorem :: SCMPDS_7:19 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (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 "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set (Var "k")) ")" )))))) ; theorem :: SCMPDS_7:20 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "J"))) & (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (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 "J")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set (Var "k")) ")" )))))) ; theorem :: SCMPDS_7:21 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (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 "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" )) & (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "J"))) & (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "J")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set (Var "k")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ))))))) ; theorem :: SCMPDS_7:22 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "J"))) & (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Bool "not" (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "J")) ")" ) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "J")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ))))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "J")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "I"))))))) ; theorem :: SCMPDS_7:23 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "J")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ) "," (Set (Var "P"))) & (Bool (Set (Var "J")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ) "," (Set (Var "P")))) "holds" (Bool "(" (Bool (Set (Var "J")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ")" ) "," (Set (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ))) & (Bool (Set (Var "J")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ")" ) "," (Set (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ))) ")" )))) ; theorem :: SCMPDS_7:24 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "J")) "being" ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "J")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ) "," (Set (Var "P"))) & (Bool (Set (Var "J")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ) "," (Set (Var "P")))) "holds" (Bool "(" (Bool (Set (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J"))) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J"))) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" ))))) ; theorem :: SCMPDS_7:25 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "J"))) & (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "J")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "I")))))))) ; theorem :: SCMPDS_7:26 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (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 "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set (Var "k")) ")" ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ))))))) ; theorem :: SCMPDS_7:27 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set (Var "s")) ")" ))) "holds" (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set "(" (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J")) ")" ) ")" ) ")" ) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set "(" (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J")) ")" ) ")" ) ")" ) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ))))))) ; theorem :: SCMPDS_7:28 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "J")) "being" ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "J")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) "," (Set (Var "P"))) & (Bool (Set (Var "J")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) "," (Set (Var "P")))) "holds" (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set "(" (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J")) ")" ) ")" ) ")" ) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "J")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set (Var "s")) ")" ")" ) ")" ) ")" ")" ))))))) ; theorem :: SCMPDS_7:29 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "J")) "being" ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "J")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) "," (Set (Var "P"))) & (Bool (Set (Var "J")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) "," (Set (Var "P")))) "holds" (Bool (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J")) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ")" )))))) ; theorem :: SCMPDS_7:30 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "J")) "being" ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "J")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) "," (Set (Var "P"))) & (Bool (Set (Var "J")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) "," (Set (Var "P")))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J")) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))))))) ; theorem :: SCMPDS_7:31 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "j")) "being" ($#v4_scmpds_4 :::"shiftable"::: ) ($#v1_scmpds_5 :::"parahalting"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" (Set (Var "I")) ($#k3_scmpds_4 :::"';'"::: ) (Set (Var "j")) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "j")) "," (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))))))) ; begin definitionlet "a" be ($#m1_subset_1 :::"Int_position":::); let "i" be ($#m1_hidden :::"Integer":::); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "I" be ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); func :::"for-up"::: "(" "a" "," "i" "," "n" "," "I" ")" -> ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_7:def 1 (Set (Set "(" (Set "(" (Set "(" "(" "a" "," "i" ")" ($#k9_scmpds_2 :::">=0_goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) "I" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ) ($#k2_scmpds_4 :::"';'"::: ) "I" ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" "a" "," "i" "," "n" ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k3_scmpds_2 :::"goto"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) "I" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ")" )); end; :: deftheorem defines :::"for-up"::: SCMPDS_7:def 1 : (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k1_scmpds_7 :::"for-up"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" "(" (Set (Var "a")) "," (Set (Var "i")) ")" ($#k9_scmpds_2 :::">=0_goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ) ($#k2_scmpds_4 :::"';'"::: ) (Set (Var "I")) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k3_scmpds_2 :::"goto"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ")" ))))))); begin theorem :: SCMPDS_7:32 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_scmpds_7 :::"for-up"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3))))))) ; theorem :: SCMPDS_7:33 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool "(" (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3))) "iff" (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k1_scmpds_7 :::"for-up"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ")" ))) ")" ))))) ; theorem :: SCMPDS_7:34 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_scmpds_7 :::"for-up"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "i")) ")" ($#k9_scmpds_2 :::">=0_goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ))) & (Bool (Set (Set "(" ($#k1_scmpds_7 :::"for-up"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set "(" ($#k1_scmpds_7 :::"for-up"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_scmpds_2 :::"goto"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ))) ")" ))))) ; theorem :: SCMPDS_7:35 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k1_scmpds_7 :::"for-up"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k1_scmpds_7 :::"for-up"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" ))))))) ; theorem :: SCMPDS_7:36 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k1_scmpds_7 :::"for-up"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) "," (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" ")" ))))))))) ; theorem :: SCMPDS_7:37 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k1_scmpds_7 :::"for-up"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3))))))))) ; theorem :: SCMPDS_7:38 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k1_scmpds_7 :::"for-up"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))))))))) ; theorem :: SCMPDS_7:39 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" )) & (Bool "(" "for" (Set (Var "t")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "Q")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "t")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "t")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" ))) & (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "t")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) ")" ) ")" )) ")" )) "holds" (Bool "(" (Bool (Set ($#k1_scmpds_7 :::"for-up"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k1_scmpds_7 :::"for-up"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" )))))))) ; theorem :: SCMPDS_7:40 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" )) & (Bool "(" "for" (Set (Var "t")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "Q")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "t")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "t")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" ))) & (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "t")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) ")" ) ")" )) ")" )) "holds" (Bool (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k1_scmpds_7 :::"for-up"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k1_scmpds_7 :::"for-up"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" (Set (Var "I")) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) ")" ")" ) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ")" ) ")" ))))))))) ; registrationlet "I" be ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "a" be ($#m1_subset_1 :::"Int_position":::); let "i" be ($#m1_hidden :::"Integer":::); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k1_scmpds_7 :::"for-up"::: ) "(" "a" "," "i" "," "n" "," "I" ")" ) -> ($#v3_scmpds_4 :::"shiftable"::: ) ; end; registrationlet "I" be ($#v2_compos_1 :::"halt-free"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "a" be ($#m1_subset_1 :::"Int_position":::); let "i" be ($#m1_hidden :::"Integer":::); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k1_scmpds_7 :::"for-up"::: ) "(" "a" "," "i" "," "n" "," "I" ")" ) -> ($#v2_compos_1 :::"halt-free"::: ) ; end; begin definitionlet "a" be ($#m1_subset_1 :::"Int_position":::); let "i" be ($#m1_hidden :::"Integer":::); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "I" be ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); func :::"for-down"::: "(" "a" "," "i" "," "n" "," "I" ")" -> ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_7:def 2 (Set (Set "(" (Set "(" (Set "(" "(" "a" "," "i" ")" ($#k8_scmpds_2 :::"<=0_goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) "I" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ) ($#k2_scmpds_4 :::"';'"::: ) "I" ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" "a" "," "i" "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) "n" ")" ) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k3_scmpds_2 :::"goto"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) "I" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ")" )); end; :: deftheorem defines :::"for-down"::: SCMPDS_7:def 2 : (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" "(" (Set (Var "a")) "," (Set (Var "i")) ")" ($#k8_scmpds_2 :::"<=0_goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ) ($#k2_scmpds_4 :::"';'"::: ) (Set (Var "I")) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "n")) ")" ) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k3_scmpds_2 :::"goto"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ")" ))))))); begin theorem :: SCMPDS_7:41 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3))))))) ; theorem :: SCMPDS_7:42 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool "(" (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3))) "iff" (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ")" ))) ")" ))))) ; theorem :: SCMPDS_7:43 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "i")) ")" ($#k8_scmpds_2 :::"<=0_goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ))) & (Bool (Set (Set "(" ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "n")) ")" ) ")" )) & (Bool (Set (Set "(" ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_scmpds_2 :::"goto"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ))) ")" ))))) ; theorem :: SCMPDS_7:44 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" ))))))) ; theorem :: SCMPDS_7:45 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) "," (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" ")" ))))))))) ; theorem :: SCMPDS_7:46 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3))))))))) ; theorem :: SCMPDS_7:47 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))))))))) ; theorem :: SCMPDS_7:48 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" )) & (Bool "(" "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "Q")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" ))) & (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) ")" ) ")" )) ")" )) "holds" (Bool "(" (Bool (Set ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" )))))))) ; theorem :: SCMPDS_7:49 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" )) & (Bool "(" "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "Q")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" ))) & (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) ")" ) ")" )) ")" )) "holds" (Bool (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" (Set (Var "I")) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "n")) ")" ) ")" ")" ) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ")" ) ")" ))))))))) ; registrationlet "I" be ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "a" be ($#m1_subset_1 :::"Int_position":::); let "i" be ($#m1_hidden :::"Integer":::); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k2_scmpds_7 :::"for-down"::: ) "(" "a" "," "i" "," "n" "," "I" ")" ) -> ($#v3_scmpds_4 :::"shiftable"::: ) ; end; registrationlet "I" be ($#v2_compos_1 :::"halt-free"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "a" be ($#m1_subset_1 :::"Int_position":::); let "i" be ($#m1_hidden :::"Integer":::); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k2_scmpds_7 :::"for-down"::: ) "(" "a" "," "i" "," "n" "," "I" ")" ) -> ($#v2_compos_1 :::"halt-free"::: ) ; end; begin definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"sum"::: "n" -> ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_7:def 3 (Set (Set "(" (Set "(" (Set "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) ($#k5_scmpds_2 :::":="::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) ")" ($#k10_scmpds_2 :::":="::: ) "n" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) ")" ($#k10_scmpds_2 :::":="::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) "," (Num 1) "," (Set "(" ($#k9_compos_1 :::"Load"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) "," (Num 1) ")" ")" ) ")" ) ")" ")" )); end; :: deftheorem defines :::"sum"::: SCMPDS_7:def 3 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_scmpds_7 :::"sum"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) ($#k5_scmpds_2 :::":="::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) ")" ($#k10_scmpds_2 :::":="::: ) (Set (Var "n")) ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) ")" ($#k10_scmpds_2 :::":="::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) "," (Num 1) "," (Set "(" ($#k9_compos_1 :::"Load"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) "," (Num 1) ")" ")" ) ")" ) ")" ")" )))); theorem :: SCMPDS_7:50 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set ($#k2_scmp_gcd :::"GBP"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) "," (Num 1) "," (Set "(" ($#k9_compos_1 :::"Load"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) "," (Num 1) ")" ")" ) ")" ) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) "," (Num 1) "," (Set "(" ($#k9_compos_1 :::"Load"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) "," (Num 1) ")" ")" ) ")" ) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" ))) ; theorem :: SCMPDS_7:51 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set ($#k2_scmp_gcd :::"GBP"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 3) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) "," (Num 1) "," (Set "(" ($#k9_compos_1 :::"Load"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) "," (Num 1) ")" ")" ) ")" ) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 3) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n")))))) ; theorem :: SCMPDS_7:52 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k3_scmpds_7 :::"sum"::: ) (Set (Var "n")) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 3) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n")))))) ; definitionlet "sp", "control", "result", "pp", "pData" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"sum"::: "(" "sp" "," "control" "," "result" "," "pp" "," "pData" ")" -> ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_7:def 4 (Set (Set "(" (Set "(" "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) "sp" ")" ) "," "result" ")" ($#k10_scmpds_2 :::":="::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) "pp" ")" ) ($#k5_scmpds_2 :::":="::: ) "pData" ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) "sp" ")" ) "," "control" "," (Num 1) "," (Set "(" (Set "(" ($#k12_scmpds_2 :::"AddTo"::: ) "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) "sp" ")" ) "," "result" "," (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) "pData" ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) "pp" ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ) ")" ) ")" ")" )); end; :: deftheorem defines :::"sum"::: SCMPDS_7:def 4 : (Bool "for" (Set (Var "sp")) "," (Set (Var "control")) "," (Set (Var "result")) "," (Set (Var "pp")) "," (Set (Var "pData")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k4_scmpds_7 :::"sum"::: ) "(" (Set (Var "sp")) "," (Set (Var "control")) "," (Set (Var "result")) "," (Set (Var "pp")) "," (Set (Var "pData")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "sp")) ")" ) "," (Set (Var "result")) ")" ($#k10_scmpds_2 :::":="::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "pp")) ")" ) ($#k5_scmpds_2 :::":="::: ) (Set (Var "pData")) ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "sp")) ")" ) "," (Set (Var "control")) "," (Num 1) "," (Set "(" (Set "(" ($#k12_scmpds_2 :::"AddTo"::: ) "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "sp")) ")" ) "," (Set (Var "result")) "," (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "pData")) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "pp")) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ) ")" ) ")" ")" )))); theorem :: SCMPDS_7:53 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "sp")) "," (Set (Var "cv")) "," (Set (Var "result")) "," (Set (Var "pp")) "," (Set (Var "pD")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "sp")) ")" )) ($#r1_xxreal_0 :::">"::: ) (Set (Var "sp"))) & (Bool (Set (Var "cv")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "result"))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "pp")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "pD"))) & (Bool (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "sp")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "result"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "pp"))) & (Bool (Set (Var "pp")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "pD"))) & (Bool (Set (Var "pD")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "pD")) ")" )))) "holds" (Bool "(" (Bool (Set ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "sp")) ")" ) "," (Set (Var "cv")) "," (Num 1) "," (Set "(" (Set "(" ($#k12_scmpds_2 :::"AddTo"::: ) "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "sp")) ")" ) "," (Set (Var "result")) "," (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "pD")) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "pp")) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ) ")" ) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "sp")) ")" ) "," (Set (Var "cv")) "," (Num 1) "," (Set "(" (Set "(" ($#k12_scmpds_2 :::"AddTo"::: ) "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "sp")) ")" ) "," (Set (Var "result")) "," (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "pD")) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "pp")) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ) ")" ) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" )))) ; theorem :: SCMPDS_7:54 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "sp")) "," (Set (Var "cv")) "," (Set (Var "result")) "," (Set (Var "pp")) "," (Set (Var "pD")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "sp")) ")" )) ($#r1_xxreal_0 :::">"::: ) (Set (Var "sp"))) & (Bool (Set (Var "cv")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "result"))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "pp")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "pD"))) & (Bool (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "sp")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "result"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "pp"))) & (Bool (Set (Var "pp")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "pD"))) & (Bool (Set (Var "pD")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "pD")) ")" ))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "sp")) ")" ) ")" ) "," (Set (Var "result")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "sp")) ")" ) ")" ) "," (Set (Var "cv")) ")" ")" ))) & (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 ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "pD")) ")" ) ")" ) "," (Set (Var "k")) ")" ")" ))) ")" )) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "sp")) ")" ) "," (Set (Var "cv")) "," (Num 1) "," (Set "(" (Set "(" ($#k12_scmpds_2 :::"AddTo"::: ) "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "sp")) ")" ) "," (Set (Var "result")) "," (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "pD")) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "pp")) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ) ")" ) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "sp")) ")" ) ")" ) "," (Set (Var "result")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set (Var "f")))))))) ; theorem :: SCMPDS_7:55 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "sp")) "," (Set (Var "cv")) "," (Set (Var "result")) "," (Set (Var "pp")) "," (Set (Var "pD")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "sp")) ")" )) ($#r1_xxreal_0 :::">"::: ) (Set (Var "sp"))) & (Bool (Set (Var "cv")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "result"))) & (Bool (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "sp")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "result"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "pp"))) & (Bool (Set (Var "pp")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "pD"))) & (Bool (Set (Var "pD")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "pD")) ")" ))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "sp")) ")" ) ")" ) "," (Set (Var "cv")) ")" ")" ))) & (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 ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "pD")) ")" ) ")" ) "," (Set (Var "k")) ")" ")" ))) ")" )) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k4_scmpds_7 :::"sum"::: ) "(" (Set (Var "sp")) "," (Set (Var "cv")) "," (Set (Var "result")) "," (Set (Var "pp")) "," (Set (Var "pD")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "sp")) ")" ) ")" ) "," (Set (Var "result")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set (Var "f")))))))) ;