:: SCMPDS_6 semantic presentation begin theorem :: SCMPDS_6:1 canceled; theorem :: SCMPDS_6:2 canceled; theorem :: SCMPDS_6:3 canceled; theorem :: SCMPDS_6:4 canceled; theorem :: SCMPDS_6:5 canceled; theorem :: SCMPDS_6:6 (Bool "for" (Set (Var "i")) "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 ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "i")) ($#k2_scmpds_4 :::"';'"::: ) (Set (Var "I")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))))) ; theorem :: SCMPDS_6:7 (Bool "for" (Set (Var "i")) "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 (Var "i")) ($#k2_scmpds_4 :::"';'"::: ) (Set (Var "I")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "i"))))) ; theorem :: SCMPDS_6:8 canceled; theorem :: SCMPDS_6:9 canceled; theorem :: SCMPDS_6:10 canceled; theorem :: SCMPDS_6:11 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "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 "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set "(" (Set (Var "i")) ($#k2_scmpds_4 :::"';'"::: ) (Set (Var "I")) ")" ) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "i"))))))) ; theorem :: SCMPDS_6:12 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "m1")))) "holds" (Bool (Set ($#k17_scmpds_2 :::"ICplusConst"::: ) "(" (Set (Var "s")) "," (Set (Var "m2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "m1")) ($#k2_nat_1 :::"+"::: ) (Set (Var "m2")))))) ; theorem :: SCMPDS_6:13 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k61_valued_1 :::"Shift"::: ) "(" (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "J")) ")" ) "," (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k10_compos_1 :::"stop"::: ) (Set "(" (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J")) ")" )))) ; theorem :: SCMPDS_6:14 canceled; theorem :: SCMPDS_6: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" ($#v6_compos_0 :::"No-StopCode"::: ) ($#v1_scmpds_5 :::"parahalting"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "J")) "being" ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#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 "(" (Set (Var "i")) ($#k2_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 "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "i")) "," (Set (Var "s")) ")" ")" ) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))))))) ; theorem :: SCMPDS_6:16 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k7_scmpds_2 :::"<>0_goto"::: ) (Set (Var "k2"))) ($#r1_hidden :::"<>"::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ))))) ; theorem :: SCMPDS_6:17 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k8_scmpds_2 :::"<=0_goto"::: ) (Set (Var "k2"))) ($#r1_hidden :::"<>"::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ))))) ; theorem :: SCMPDS_6:18 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k9_scmpds_2 :::">=0_goto"::: ) (Set (Var "k2"))) ($#r1_hidden :::"<>"::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ))))) ; definitionlet "k1" be ($#m1_hidden :::"Integer":::); func :::"Goto"::: "k1" -> ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_6:def 1 (Set ($#k9_compos_1 :::"Load"::: ) (Set "(" ($#k3_scmpds_2 :::"goto"::: ) "k1" ")" )); end; :: deftheorem defines :::"Goto"::: SCMPDS_6:def 1 : (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k1_scmpds_6 :::"Goto"::: ) (Set (Var "k1"))) ($#r1_hidden :::"="::: ) (Set ($#k9_compos_1 :::"Load"::: ) (Set "(" ($#k3_scmpds_2 :::"goto"::: ) (Set (Var "k1")) ")" )))); registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k3_scmpds_2 :::"goto"::: ) (Set "(" "n" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) -> ($#v6_compos_0 :::"No-StopCode"::: ) ; cluster (Set ($#k3_scmpds_2 :::"goto"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set "(" "n" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) -> ($#v6_compos_0 :::"No-StopCode"::: ) ; end; registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k1_scmpds_6 :::"Goto"::: ) (Set "(" "n" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) -> ($#v2_compos_1 :::"halt-free"::: ) ; cluster (Set ($#k1_scmpds_6 :::"Goto"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set "(" "n" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) -> ($#v2_compos_1 :::"halt-free"::: ) ; end; theorem :: SCMPDS_6:19 (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_scmpds_6 :::"Goto"::: ) (Set (Var "k1")) ")" ))) & (Bool (Set (Set "(" ($#k1_scmpds_6 :::"Goto"::: ) (Set (Var "k1")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k3_scmpds_2 :::"goto"::: ) (Set (Var "k1")))) ")" )) ; begin definitionlet "I" be ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "s" be ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "P" be ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); pred "I" :::"is_closed_on"::: "s" "," "P" means :: SCMPDS_6:def 2 (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" "P" ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) "I" ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) "s" ")" ) "," (Set (Var "k")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) "I" ")" )))); pred "I" :::"is_halting_on"::: "s" "," "P" means :: SCMPDS_6:def 3 (Bool (Set "P" ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) "I" ")" )) ($#r1_extpro_1 :::"halts_on"::: ) (Set ($#k8_memstr_0 :::"Initialize"::: ) "s")); end; :: deftheorem defines :::"is_closed_on"::: SCMPDS_6:def 2 : (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 "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool "(" (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) "iff" (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (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")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" )))) ")" )))); :: deftheorem defines :::"is_halting_on"::: SCMPDS_6:def 3 : (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 "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool "(" (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) "iff" (Bool (Set (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" )) ($#r1_extpro_1 :::"halts_on"::: ) (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")))) ")" )))); theorem :: SCMPDS_6:20 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#v1_scmpds_4 :::"paraclosed"::: ) ) "iff" (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"::: ) ) "holds" (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))))) ")" )) ; theorem :: SCMPDS_6:21 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#v2_scmpds_4 :::"parahalting"::: ) ) "iff" (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"::: ) ) "holds" (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))))) ")" )) ; theorem :: SCMPDS_6:22 (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 ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s2")))) & (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s1")) "," (Set (Var "P1")))) "holds" (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s2")) "," (Set (Var "P2")))))) ; theorem :: SCMPDS_6:23 (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 ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s2")))) & (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 "(" (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s2")) "," (Set (Var "P2"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s2")) "," (Set (Var "P2"))) ")" )))) ; theorem :: SCMPDS_6:24 (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")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool "(" (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) "iff" (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s"))) "," (Set (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "J")))) ")" )))) ; theorem :: SCMPDS_6:25 (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")) "," (Set (Var "J")) "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 "P"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool "(" (Bool "(" "for" (Set (Var "k")) "being" ($#m1_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 (Var "s")) ")" ))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (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")) ")" ")" ))) ")" ) & (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set (Var "s")) "," (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set (Var "s")) ")" ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (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 "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set (Var "s")) ")" ")" ) ")" ")" ))) ")" )))) ; theorem :: SCMPDS_6:26 (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 "k")) "being" ($#m1_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_memstr_0 :::"IC"::: ) (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")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "I")))))))) ; theorem :: SCMPDS_6: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" ($#m1_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 (Var "I")) ")" ) ")" ) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (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")) ")" ")" ) ")" )))))) ; theorem :: SCMPDS_6:28 (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 "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m1_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 ($#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_6:29 (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 "s")) "being" ($#m1_hidden :::"State":::) "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 ($#k5_memstr_0 :::"IC"::: ) (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")) ")" ) ")" ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "I"))))))) ; theorem :: SCMPDS_6:30 (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"::: ) ) "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 "(" (Bool (Set (Set "(" (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k1_scmpds_6 :::"Goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J"))) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Set "(" (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k1_scmpds_6 :::"Goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J"))) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" )))) ; theorem :: SCMPDS_6:31 (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")))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k61_valued_1 :::"Shift"::: ) "(" (Set "(" ($#k10_compos_1 :::"stop"::: ) (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" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ))) & (Bool (Set ($#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_6:32 (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" ($#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")))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" (Set "(" (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k1_scmpds_6 :::"Goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J")) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))))))) ; theorem :: SCMPDS_6:33 (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" ($#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")))) "holds" (Bool (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" (Set "(" (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k1_scmpds_6 :::"Goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J")) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" ")" ))))))) ; theorem :: SCMPDS_6:34 (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"::: ) ($#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")))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "I"))))))) ; begin definitionlet "a" be ($#m1_subset_1 :::"Int_position":::); let "k" be ($#m1_hidden :::"Integer":::); let "I", "J" be ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); func :::"if=0"::: "(" "a" "," "k" "," "I" "," "J" ")" -> ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_6:def 4 (Set (Set "(" (Set "(" (Set "(" "(" "a" "," "k" ")" ($#k7_scmpds_2 :::"<>0_goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) "I" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k2_scmpds_4 :::"';'"::: ) "I" ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k1_scmpds_6 :::"Goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) "J" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) "J"); func :::"if>0"::: "(" "a" "," "k" "," "I" "," "J" ")" -> ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_6:def 5 (Set (Set "(" (Set "(" (Set "(" "(" "a" "," "k" ")" ($#k8_scmpds_2 :::"<=0_goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) "I" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k2_scmpds_4 :::"';'"::: ) "I" ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k1_scmpds_6 :::"Goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) "J" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) "J"); func :::"if<0"::: "(" "a" "," "k" "," "I" "," "J" ")" -> ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_6:def 6 (Set (Set "(" (Set "(" (Set "(" "(" "a" "," "k" ")" ($#k9_scmpds_2 :::">=0_goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) "I" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k2_scmpds_4 :::"';'"::: ) "I" ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k1_scmpds_6 :::"Goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) "J" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) "J"); end; :: deftheorem defines :::"if=0"::: SCMPDS_6:def 4 : (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k2_scmpds_6 :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" "(" (Set (Var "a")) "," (Set (Var "k")) ")" ($#k7_scmpds_2 :::"<>0_goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k2_scmpds_4 :::"';'"::: ) (Set (Var "I")) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k1_scmpds_6 :::"Goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J"))))))); :: deftheorem defines :::"if>0"::: SCMPDS_6:def 5 : (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k3_scmpds_6 :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" "(" (Set (Var "a")) "," (Set (Var "k")) ")" ($#k8_scmpds_2 :::"<=0_goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k2_scmpds_4 :::"';'"::: ) (Set (Var "I")) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k1_scmpds_6 :::"Goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J"))))))); :: deftheorem defines :::"if<0"::: SCMPDS_6:def 6 : (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k4_scmpds_6 :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "k")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" "(" (Set (Var "a")) "," (Set (Var "k")) ")" ($#k9_scmpds_2 :::">=0_goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k2_scmpds_4 :::"';'"::: ) (Set (Var "I")) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k1_scmpds_6 :::"Goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J"))))))); definitionlet "a" be ($#m1_subset_1 :::"Int_position":::); let "k" be ($#m1_hidden :::"Integer":::); let "I" be ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); func :::"if=0"::: "(" "a" "," "k" "," "I" ")" -> ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_6:def 7 (Set (Set "(" "(" "a" "," "k" ")" ($#k7_scmpds_2 :::"<>0_goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) "I" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k2_scmpds_4 :::"';'"::: ) "I"); func :::"if<>0"::: "(" "a" "," "k" "," "I" ")" -> ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_6:def 8 (Set (Set "(" (Set "(" "(" "a" "," "k" ")" ($#k7_scmpds_2 :::"<>0_goto"::: ) (Num 2) ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" ($#k3_scmpds_2 :::"goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) "I" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) "I"); func :::"if>0"::: "(" "a" "," "k" "," "I" ")" -> ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_6:def 9 (Set (Set "(" "(" "a" "," "k" ")" ($#k8_scmpds_2 :::"<=0_goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) "I" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k2_scmpds_4 :::"';'"::: ) "I"); func :::"if<=0"::: "(" "a" "," "k" "," "I" ")" -> ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_6:def 10 (Set (Set "(" (Set "(" "(" "a" "," "k" ")" ($#k8_scmpds_2 :::"<=0_goto"::: ) (Num 2) ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" ($#k3_scmpds_2 :::"goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) "I" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) "I"); func :::"if<0"::: "(" "a" "," "k" "," "I" ")" -> ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_6:def 11 (Set (Set "(" "(" "a" "," "k" ")" ($#k9_scmpds_2 :::">=0_goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) "I" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k2_scmpds_4 :::"';'"::: ) "I"); func :::"if>=0"::: "(" "a" "," "k" "," "I" ")" -> ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_6:def 12 (Set (Set "(" (Set "(" "(" "a" "," "k" ")" ($#k9_scmpds_2 :::">=0_goto"::: ) (Num 2) ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" ($#k3_scmpds_2 :::"goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) "I" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) "I"); end; :: deftheorem defines :::"if=0"::: SCMPDS_6:def 7 : (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k5_scmpds_6 :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k")) "," (Set (Var "I")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" "(" (Set (Var "a")) "," (Set (Var "k")) ")" ($#k7_scmpds_2 :::"<>0_goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k2_scmpds_4 :::"';'"::: ) (Set (Var "I"))))))); :: deftheorem defines :::"if<>0"::: SCMPDS_6:def 8 : (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k6_scmpds_6 :::"if<>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k")) "," (Set (Var "I")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" "(" (Set (Var "a")) "," (Set (Var "k")) ")" ($#k7_scmpds_2 :::"<>0_goto"::: ) (Num 2) ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" ($#k3_scmpds_2 :::"goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "I"))))))); :: deftheorem defines :::"if>0"::: SCMPDS_6:def 9 : (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k7_scmpds_6 :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k")) "," (Set (Var "I")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" "(" (Set (Var "a")) "," (Set (Var "k")) ")" ($#k8_scmpds_2 :::"<=0_goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k2_scmpds_4 :::"';'"::: ) (Set (Var "I"))))))); :: deftheorem defines :::"if<=0"::: SCMPDS_6:def 10 : (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k8_scmpds_6 :::"if<=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k")) "," (Set (Var "I")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" "(" (Set (Var "a")) "," (Set (Var "k")) ")" ($#k8_scmpds_2 :::"<=0_goto"::: ) (Num 2) ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" ($#k3_scmpds_2 :::"goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "I"))))))); :: deftheorem defines :::"if<0"::: SCMPDS_6:def 11 : (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k9_scmpds_6 :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "k")) "," (Set (Var "I")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" "(" (Set (Var "a")) "," (Set (Var "k")) ")" ($#k9_scmpds_2 :::">=0_goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k2_scmpds_4 :::"';'"::: ) (Set (Var "I"))))))); :: deftheorem defines :::"if>=0"::: SCMPDS_6:def 12 : (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k10_scmpds_6 :::"if>=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k")) "," (Set (Var "I")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" "(" (Set (Var "a")) "," (Set (Var "k")) ")" ($#k9_scmpds_2 :::">=0_goto"::: ) (Num 2) ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" ($#k3_scmpds_2 :::"goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "I"))))))); begin theorem :: SCMPDS_6:35 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_scmpds_6 :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2)))))) ; theorem :: SCMPDS_6:36 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_scmpds_6 :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ))) & (Bool (Num 1) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_scmpds_6 :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ))) ")" )))) ; theorem :: SCMPDS_6:37 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set (Set "(" ($#k2_scmpds_6 :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k7_scmpds_2 :::"<>0_goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )))))) ; theorem :: SCMPDS_6:38 (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")) "," (Set (Var "J")) "being" ($#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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (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 "(" (Bool (Set ($#k2_scmpds_6 :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k2_scmpds_6 :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" )))))) ; theorem :: SCMPDS_6: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" ($#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"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "J")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "J")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool "(" (Bool (Set ($#k2_scmpds_6 :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k2_scmpds_6 :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" ))))))) ; theorem :: SCMPDS_6: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 "J")) "being" ($#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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (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 ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_6 :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) "," (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" ")" ))))))))) ; theorem :: SCMPDS_6:41 (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 "J")) "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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "J")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "J")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_6 :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) "," (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" ")" ))))))))) ; registrationlet "I", "J" be ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "a" be ($#m1_subset_1 :::"Int_position":::); let "k1" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k2_scmpds_6 :::"if=0"::: ) "(" "a" "," "k1" "," "I" "," "J" ")" ) -> ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ; end; registrationlet "I", "J" be ($#v2_compos_1 :::"halt-free"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "a" be ($#m1_subset_1 :::"Int_position":::); let "k1" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k2_scmpds_6 :::"if=0"::: ) "(" "a" "," "k1" "," "I" "," "J" ")" ) -> ($#v2_compos_1 :::"halt-free"::: ) ; end; theorem :: SCMPDS_6:42 (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")) "," (Set (Var "J")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v2_scmpds_4 :::"parahalting"::: ) ($#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 "k1")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_6 :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2)))))))) ; theorem :: SCMPDS_6:43 (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"::: ) ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#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"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_6 :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))))))))) ; theorem :: SCMPDS_6: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 "J")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_6 :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))))))))) ; begin theorem :: SCMPDS_6:45 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k5_scmpds_6 :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))))) ; theorem :: SCMPDS_6:46 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k5_scmpds_6 :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" )))))) ; theorem :: SCMPDS_6:47 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set (Set "(" ($#k5_scmpds_6 :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k7_scmpds_2 :::"<>0_goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))))) ; theorem :: SCMPDS_6: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" ($#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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (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 "(" (Bool (Set ($#k5_scmpds_6 :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k5_scmpds_6 :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" )))))) ; theorem :: SCMPDS_6:49 (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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k5_scmpds_6 :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k5_scmpds_6 :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" )))))) ; theorem :: SCMPDS_6:50 (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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (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 ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k5_scmpds_6 :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (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 1) ")" ) "," (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" ")" )))))))) ; theorem :: SCMPDS_6:51 (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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k5_scmpds_6 :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (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 1) ")" ) "," (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" ")" )))))))) ; registrationlet "I" be ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "a" be ($#m1_subset_1 :::"Int_position":::); let "k1" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k5_scmpds_6 :::"if=0"::: ) "(" "a" "," "k1" "," "I" ")" ) -> ($#v2_scmpds_4 :::"parahalting"::: ) ($#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 "k1" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k5_scmpds_6 :::"if=0"::: ) "(" "a" "," "k1" "," "I" ")" ) -> ($#v2_compos_1 :::"halt-free"::: ) ; end; theorem :: SCMPDS_6: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 "I")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v2_scmpds_4 :::"parahalting"::: ) ($#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 "k1")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k5_scmpds_6 :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))))))) ; theorem :: SCMPDS_6:53 (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"::: ) ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k5_scmpds_6 :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (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 "b"))))))))) ; theorem :: SCMPDS_6:54 (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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k5_scmpds_6 :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (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"))))))))) ; begin theorem :: SCMPDS_6:55 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k6_scmpds_6 :::"if<>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2)))))) ; theorem :: SCMPDS_6:56 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k6_scmpds_6 :::"if<>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" ))) & (Bool (Num 1) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k6_scmpds_6 :::"if<>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" ))) ")" )))) ; theorem :: SCMPDS_6:57 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_6 :::"if<>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k7_scmpds_2 :::"<>0_goto"::: ) (Num 2))) & (Bool (Set (Set "(" ($#k6_scmpds_6 :::"if<>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k3_scmpds_2 :::"goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" )))) ; theorem :: SCMPDS_6:58 (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" ($#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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (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 "(" (Bool (Set ($#k6_scmpds_6 :::"if<>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k6_scmpds_6 :::"if<>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" )))))) ; theorem :: SCMPDS_6:59 (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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k6_scmpds_6 :::"if<>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k6_scmpds_6 :::"if<>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" )))))) ; theorem :: SCMPDS_6:60 (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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (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 ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k6_scmpds_6 :::"if<>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (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 2) ")" ) "," (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" ")" )))))))) ; theorem :: SCMPDS_6:61 (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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k6_scmpds_6 :::"if<>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (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 2) ")" ) "," (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" ")" )))))))) ; registrationlet "I" be ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "a" be ($#m1_subset_1 :::"Int_position":::); let "k1" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k6_scmpds_6 :::"if<>0"::: ) "(" "a" "," "k1" "," "I" ")" ) -> ($#v2_scmpds_4 :::"parahalting"::: ) ($#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 "k1" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k6_scmpds_6 :::"if<>0"::: ) "(" "a" "," "k1" "," "I" ")" ) -> ($#v2_compos_1 :::"halt-free"::: ) ; end; theorem :: SCMPDS_6:62 (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"::: ) ($#v2_scmpds_4 :::"parahalting"::: ) ($#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 "k1")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k6_scmpds_6 :::"if<>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (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 2)))))))) ; theorem :: SCMPDS_6:63 (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"::: ) ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k6_scmpds_6 :::"if<>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (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 "b"))))))))) ; theorem :: SCMPDS_6:64 (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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k6_scmpds_6 :::"if<>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (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"))))))))) ; begin theorem :: SCMPDS_6:65 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k3_scmpds_6 :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2)))))) ; theorem :: SCMPDS_6:66 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k3_scmpds_6 :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ))) & (Bool (Num 1) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k3_scmpds_6 :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ))) ")" )))) ; theorem :: SCMPDS_6:67 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set (Set "(" ($#k3_scmpds_6 :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k8_scmpds_2 :::"<=0_goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )))))) ; theorem :: SCMPDS_6:68 (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")) "," (Set (Var "J")) "being" ($#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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (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 "(" (Bool (Set ($#k3_scmpds_6 :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k3_scmpds_6 :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" )))))) ; theorem :: SCMPDS_6:69 (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 "J")) "being" ($#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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "J")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "J")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool "(" (Bool (Set ($#k3_scmpds_6 :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k3_scmpds_6 :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" ))))))) ; theorem :: SCMPDS_6:70 (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 "J")) "being" ($#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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (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 ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k3_scmpds_6 :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) "," (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" ")" ))))))))) ; theorem :: SCMPDS_6:71 (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 "J")) "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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "J")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "J")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k3_scmpds_6 :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) "," (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" ")" ))))))))) ; registrationlet "I", "J" be ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "a" be ($#m1_subset_1 :::"Int_position":::); let "k1" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k3_scmpds_6 :::"if>0"::: ) "(" "a" "," "k1" "," "I" "," "J" ")" ) -> ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ; end; registrationlet "I", "J" be ($#v2_compos_1 :::"halt-free"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "a" be ($#m1_subset_1 :::"Int_position":::); let "k1" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k3_scmpds_6 :::"if>0"::: ) "(" "a" "," "k1" "," "I" "," "J" ")" ) -> ($#v2_compos_1 :::"halt-free"::: ) ; end; theorem :: SCMPDS_6:72 (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")) "," (Set (Var "J")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v2_scmpds_4 :::"parahalting"::: ) ($#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 "k1")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k3_scmpds_6 :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2)))))))) ; theorem :: SCMPDS_6:73 (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"::: ) ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#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"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k3_scmpds_6 :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))))))))) ; theorem :: SCMPDS_6:74 (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 "J")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k3_scmpds_6 :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))))))))) ; begin theorem :: SCMPDS_6:75 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k7_scmpds_6 :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))))) ; theorem :: SCMPDS_6:76 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k7_scmpds_6 :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" )))))) ; theorem :: SCMPDS_6:77 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set (Set "(" ($#k7_scmpds_6 :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k8_scmpds_2 :::"<=0_goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))))) ; theorem :: SCMPDS_6:78 (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" ($#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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (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 "(" (Bool (Set ($#k7_scmpds_6 :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k7_scmpds_6 :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" )))))) ; theorem :: SCMPDS_6:79 (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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k7_scmpds_6 :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k7_scmpds_6 :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" )))))) ; theorem :: SCMPDS_6:80 (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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (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 ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k7_scmpds_6 :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (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 1) ")" ) "," (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" ")" )))))))) ; theorem :: SCMPDS_6:81 (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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k7_scmpds_6 :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (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 1) ")" ) "," (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" ")" )))))))) ; registrationlet "I" be ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "a" be ($#m1_subset_1 :::"Int_position":::); let "k1" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k7_scmpds_6 :::"if>0"::: ) "(" "a" "," "k1" "," "I" ")" ) -> ($#v2_scmpds_4 :::"parahalting"::: ) ($#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 "k1" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k7_scmpds_6 :::"if>0"::: ) "(" "a" "," "k1" "," "I" ")" ) -> ($#v2_compos_1 :::"halt-free"::: ) ; end; theorem :: SCMPDS_6:82 (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"::: ) ($#v2_scmpds_4 :::"parahalting"::: ) ($#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 "k1")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k7_scmpds_6 :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))))))) ; theorem :: SCMPDS_6:83 (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"::: ) ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k7_scmpds_6 :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (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 "b"))))))))) ; theorem :: SCMPDS_6:84 (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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k7_scmpds_6 :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (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"))))))))) ; begin theorem :: SCMPDS_6:85 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k8_scmpds_6 :::"if<=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2)))))) ; theorem :: SCMPDS_6:86 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k8_scmpds_6 :::"if<=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" ))) & (Bool (Num 1) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k8_scmpds_6 :::"if<=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" ))) ")" )))) ; theorem :: SCMPDS_6:87 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k8_scmpds_6 :::"if<=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k8_scmpds_2 :::"<=0_goto"::: ) (Num 2))) & (Bool (Set (Set "(" ($#k8_scmpds_6 :::"if<=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k3_scmpds_2 :::"goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" )))) ; theorem :: SCMPDS_6:88 (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" ($#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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (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 "(" (Bool (Set ($#k8_scmpds_6 :::"if<=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k8_scmpds_6 :::"if<=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" )))))) ; theorem :: SCMPDS_6:89 (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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k8_scmpds_6 :::"if<=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k8_scmpds_6 :::"if<=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" )))))) ; theorem :: SCMPDS_6:90 (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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (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 ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k8_scmpds_6 :::"if<=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (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 2) ")" ) "," (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" ")" )))))))) ; theorem :: SCMPDS_6:91 (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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k8_scmpds_6 :::"if<=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (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 2) ")" ) "," (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" ")" )))))))) ; registrationlet "I" be ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "a" be ($#m1_subset_1 :::"Int_position":::); let "k1" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k8_scmpds_6 :::"if<=0"::: ) "(" "a" "," "k1" "," "I" ")" ) -> ($#v2_scmpds_4 :::"parahalting"::: ) ($#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 "k1" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k8_scmpds_6 :::"if<=0"::: ) "(" "a" "," "k1" "," "I" ")" ) -> ($#v2_compos_1 :::"halt-free"::: ) ; end; theorem :: SCMPDS_6:92 (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"::: ) ($#v2_scmpds_4 :::"parahalting"::: ) ($#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 "k1")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k8_scmpds_6 :::"if<=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2)))))))) ; theorem :: SCMPDS_6:93 (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"::: ) ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k8_scmpds_6 :::"if<=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (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 "b"))))))))) ; theorem :: SCMPDS_6:94 (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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k8_scmpds_6 :::"if<=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (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"))))))))) ; begin theorem :: SCMPDS_6:95 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k4_scmpds_6 :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2)))))) ; theorem :: SCMPDS_6:96 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k4_scmpds_6 :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ))) & (Bool (Num 1) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k4_scmpds_6 :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ))) ")" )))) ; theorem :: SCMPDS_6:97 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set (Set "(" ($#k4_scmpds_6 :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k9_scmpds_2 :::">=0_goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )))))) ; theorem :: SCMPDS_6:98 (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")) "," (Set (Var "J")) "being" ($#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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (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 "(" (Bool (Set ($#k4_scmpds_6 :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k4_scmpds_6 :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" )))))) ; theorem :: SCMPDS_6:99 (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 "J")) "being" ($#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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "J")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "J")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool "(" (Bool (Set ($#k4_scmpds_6 :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k4_scmpds_6 :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" ))))))) ; theorem :: SCMPDS_6:100 (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 "J")) "being" ($#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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (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 ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k4_scmpds_6 :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) "," (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" ")" ))))))))) ; theorem :: SCMPDS_6:101 (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 "J")) "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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "J")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "J")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k4_scmpds_6 :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) "," (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" ")" ))))))))) ; registrationlet "I", "J" be ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "a" be ($#m1_subset_1 :::"Int_position":::); let "k1" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k4_scmpds_6 :::"if<0"::: ) "(" "a" "," "k1" "," "I" "," "J" ")" ) -> ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ; end; registrationlet "I", "J" be ($#v2_compos_1 :::"halt-free"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "a" be ($#m1_subset_1 :::"Int_position":::); let "k1" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k4_scmpds_6 :::"if<0"::: ) "(" "a" "," "k1" "," "I" "," "J" ")" ) -> ($#v2_compos_1 :::"halt-free"::: ) ; end; theorem :: SCMPDS_6:102 (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")) "," (Set (Var "J")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v2_scmpds_4 :::"parahalting"::: ) ($#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 "k1")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k4_scmpds_6 :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2)))))))) ; theorem :: SCMPDS_6:103 (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"::: ) ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#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"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k4_scmpds_6 :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))))))))) ; theorem :: SCMPDS_6:104 (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 "J")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k4_scmpds_6 :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))))))))) ; begin theorem :: SCMPDS_6:105 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k9_scmpds_6 :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))))) ; theorem :: SCMPDS_6:106 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k9_scmpds_6 :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" )))))) ; theorem :: SCMPDS_6:107 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set (Set "(" ($#k9_scmpds_6 :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k9_scmpds_2 :::">=0_goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))))) ; theorem :: SCMPDS_6:108 (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" ($#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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (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 "(" (Bool (Set ($#k9_scmpds_6 :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k9_scmpds_6 :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" )))))) ; theorem :: SCMPDS_6:109 (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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k9_scmpds_6 :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k9_scmpds_6 :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" )))))) ; theorem :: SCMPDS_6:110 (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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (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 ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k9_scmpds_6 :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (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 1) ")" ) "," (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" ")" )))))))) ; theorem :: SCMPDS_6:111 (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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k9_scmpds_6 :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (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 1) ")" ) "," (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" ")" )))))))) ; registrationlet "I" be ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "a" be ($#m1_subset_1 :::"Int_position":::); let "k1" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k9_scmpds_6 :::"if<0"::: ) "(" "a" "," "k1" "," "I" ")" ) -> ($#v2_scmpds_4 :::"parahalting"::: ) ($#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 "k1" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k9_scmpds_6 :::"if<0"::: ) "(" "a" "," "k1" "," "I" ")" ) -> ($#v2_compos_1 :::"halt-free"::: ) ; end; theorem :: SCMPDS_6:112 (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"::: ) ($#v2_scmpds_4 :::"parahalting"::: ) ($#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 "k1")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k9_scmpds_6 :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (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 1)))))))) ; theorem :: SCMPDS_6:113 (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"::: ) ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k9_scmpds_6 :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (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 "b"))))))))) ; theorem :: SCMPDS_6:114 (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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k9_scmpds_6 :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (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"))))))))) ; begin theorem :: SCMPDS_6:115 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k10_scmpds_6 :::"if>=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2)))))) ; theorem :: SCMPDS_6:116 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k10_scmpds_6 :::"if>=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" ))) & (Bool (Num 1) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k10_scmpds_6 :::"if>=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" ))) ")" )))) ; theorem :: SCMPDS_6:117 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k10_scmpds_6 :::"if>=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k9_scmpds_2 :::">=0_goto"::: ) (Num 2))) & (Bool (Set (Set "(" ($#k10_scmpds_6 :::"if>=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k3_scmpds_2 :::"goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" )))) ; theorem :: SCMPDS_6:118 (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" ($#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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (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 "(" (Bool (Set ($#k10_scmpds_6 :::"if>=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k10_scmpds_6 :::"if>=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" )))))) ; theorem :: SCMPDS_6:119 (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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k10_scmpds_6 :::"if>=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k10_scmpds_6 :::"if>=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" )))))) ; theorem :: SCMPDS_6:120 (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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (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 ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k10_scmpds_6 :::"if>=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (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 2) ")" ) "," (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" ")" )))))))) ; theorem :: SCMPDS_6:121 (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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k10_scmpds_6 :::"if>=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (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 2) ")" ) "," (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" ")" )))))))) ; registrationlet "I" be ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "a" be ($#m1_subset_1 :::"Int_position":::); let "k1" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k10_scmpds_6 :::"if>=0"::: ) "(" "a" "," "k1" "," "I" ")" ) -> ($#v2_scmpds_4 :::"parahalting"::: ) ($#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 "k1" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k10_scmpds_6 :::"if>=0"::: ) "(" "a" "," "k1" "," "I" ")" ) -> ($#v2_compos_1 :::"halt-free"::: ) ; end; theorem :: SCMPDS_6:122 (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"::: ) ($#v2_scmpds_4 :::"parahalting"::: ) ($#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 "k1")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k10_scmpds_6 :::"if>=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2)))))))) ; theorem :: SCMPDS_6:123 (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"::: ) ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k10_scmpds_6 :::"if>=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (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 "b"))))))))) ; theorem :: SCMPDS_6:124 (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 "k1")) "being" ($#m1_hidden :::"Integer":::) "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 "k1")) ")" ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k10_scmpds_6 :::"if>=0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (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_6:125 (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"::: ) ) "holds" (Bool "(" (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) "iff" (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s"))) "," (Set (Var "P"))) ")" )))) ; theorem :: SCMPDS_6:126 (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"::: ) ) "holds" (Bool "(" (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) "iff" (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s"))) "," (Set (Var "P"))) ")" )))) ;