:: SCMPDS_8 semantic presentation begin theorem :: SCMPDS_8:1 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "ex" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "i")))))) ; theorem :: SCMPDS_8:2 canceled; theorem :: SCMPDS_8:3 (Bool "for" (Set (Var "t")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 4) "," (Num 5) "," (Num 6) "," (Num 14) ($#k10_domain_1 :::"}"::: ) ))) "holds" (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "i")) "," (Set (Var "t")) ")" ")" ))))) ; theorem :: SCMPDS_8:4 canceled; theorem :: SCMPDS_8:5 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" ($#k2_memstr_0 :::"the_Values_of"::: ) (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" ) ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "f")) ($#k1_recdef_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "f")) ($#k1_recdef_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) ")" ")" )))) ; begin definitioncanceled; let "a" be ($#m1_subset_1 :::"Int_position":::); let "i" be ($#m1_hidden :::"Integer":::); let "I" be ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); func :::"while<0"::: "(" "a" "," "i" "," "I" ")" -> ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_8:def 2 (Set (Set "(" (Set "(" "(" "a" "," "i" ")" ($#k9_scmpds_2 :::">=0_goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) "I" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k2_scmpds_4 :::"';'"::: ) "I" ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k3_scmpds_2 :::"goto"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) "I" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" )); end; :: deftheorem SCMPDS_8:def 1 : canceled; :: deftheorem defines :::"while<0"::: SCMPDS_8:def 2 : (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k1_scmpds_8 :::"while<0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" "(" (Set (Var "a")) "," (Set (Var "i")) ")" ($#k9_scmpds_2 :::">=0_goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k2_scmpds_4 :::"';'"::: ) (Set (Var "I")) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k3_scmpds_2 :::"goto"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" )))))); registrationlet "I" be ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "a" be ($#m1_subset_1 :::"Int_position":::); let "i" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k1_scmpds_8 :::"while<0"::: ) "(" "a" "," "i" "," "I" ")" ) -> ($#v3_scmpds_4 :::"shiftable"::: ) ; end; registrationlet "I" be ($#v2_compos_1 :::"halt-free"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "a" be ($#m1_subset_1 :::"Int_position":::); let "i" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k1_scmpds_8 :::"while<0"::: ) "(" "a" "," "i" "," "I" ")" ) -> ($#v2_compos_1 :::"halt-free"::: ) ; end; theorem :: SCMPDS_8:6 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "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 "(" ($#k1_scmpds_8 :::"while<0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2)))))) ; theorem :: SCMPDS_8:7 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool "(" (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2))) "iff" (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_scmpds_8 :::"while<0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ))) ")" ))))) ; theorem :: SCMPDS_8:8 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_scmpds_8 :::"while<0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "i")) ")" ($#k9_scmpds_2 :::">=0_goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ))) & (Bool (Set (Set "(" ($#k1_scmpds_8 :::"while<0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_scmpds_2 :::"goto"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" )))) ; theorem :: SCMPDS_8:9 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k1_scmpds_8 :::"while<0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k1_scmpds_8 :::"while<0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" )))))) ; theorem :: SCMPDS_8:10 (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 "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "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 "i")) ")" ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k1_scmpds_8 :::"while<0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (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"::: ) ) ")" ")" )))))))) ; theorem :: SCMPDS_8:11 (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 "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "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 "i")) ")" ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k1_scmpds_8 :::"while<0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (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_8:12 (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 "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "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 "i")) ")" ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k1_scmpds_8 :::"while<0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))))))))) ; scheme :: SCMPDS_8:sch 1 WhileLHalt{ F1( ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) )) -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F2() -> (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F3() -> ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F4() -> ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F5() -> ($#m1_subset_1 :::"Int_position":::), F6() -> ($#m1_hidden :::"Integer":::), P1[ ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) )] } : (Bool "(" (Bool (Set ($#k1_scmpds_8 :::"while<0"::: ) "(" (Set F5 "(" ")" ) "," (Set F6 "(" ")" ) "," (Set F4 "(" ")" ) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set F2 "(" ")" ) "," (Set F3 "(" ")" )) & (Bool (Set ($#k1_scmpds_8 :::"while<0"::: ) "(" (Set F5 "(" ")" ) "," (Set F6 "(" ")" ) "," (Set F4 "(" ")" ) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set F2 "(" ")" ) "," (Set F3 "(" ")" )) ")" ) provided (Bool "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool P1[(Set (Var "t"))]) & (Bool (Set F1 "(" (Set (Var "t")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ) ")" ) "," (Set F6 "(" ")" ) ")" ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) and (Bool P1[(Set F2 "(" ")" )]) and (Bool "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "Q")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool P1[(Set (Var "t"))]) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" )) ($#r1_hidden :::"="::: ) (Set (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ) ")" ) "," (Set F6 "(" ")" ) ")" ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set F4 "(" ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ))) & (Bool (Set F4 "(" ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set F4 "(" ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set F1 "(" (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set F4 "(" ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ")" ) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set F1 "(" (Set (Var "t")) ")" )) & (Bool P1[(Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set F4 "(" ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ))]) ")" ))) proof end; scheme :: SCMPDS_8:sch 2 WhileLExec{ F1( ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) )) -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F2() -> (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F3() -> ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F4() -> ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F5() -> ($#m1_subset_1 :::"Int_position":::), F6() -> ($#m1_hidden :::"Integer":::), P1[ ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) )] } : (Bool (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k1_scmpds_8 :::"while<0"::: ) "(" (Set F5 "(" ")" ) "," (Set F6 "(" ")" ) "," (Set F4 "(" ")" ) ")" ")" ) "," (Set F3 "(" ")" ) "," (Set F2 "(" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k1_scmpds_8 :::"while<0"::: ) "(" (Set F5 "(" ")" ) "," (Set F6 "(" ")" ) "," (Set F4 "(" ")" ) ")" ")" ) "," (Set F3 "(" ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set F4 "(" ")" ) "," (Set F3 "(" ")" ) "," (Set F2 "(" ")" ) ")" ")" ) ")" ) ")" )) provided (Bool (Set (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ) ")" ) "," (Set F6 "(" ")" ) ")" ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) and (Bool "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool P1[(Set (Var "t"))]) & (Bool (Set F1 "(" (Set (Var "t")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ) ")" ) "," (Set F6 "(" ")" ) ")" ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) and (Bool P1[(Set F2 "(" ")" )]) and (Bool "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "Q")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool P1[(Set (Var "t"))]) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" )) ($#r1_hidden :::"="::: ) (Set (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ) ")" ) "," (Set F6 "(" ")" ) ")" ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set F4 "(" ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ))) & (Bool (Set F4 "(" ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set F4 "(" ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set F1 "(" (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set F4 "(" ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ")" ) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set F1 "(" (Set (Var "t")) ")" )) & (Bool P1[(Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set F4 "(" ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ))]) ")" ))) proof end; theorem :: SCMPDS_8:13 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" ($#k2_memstr_0 :::"the_Values_of"::: ) (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" ) ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_recdef_1 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "Q")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Set (Var "f")) ($#k1_recdef_1 :::"."::: ) (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "f")) ($#k1_recdef_1 :::"."::: ) (Set (Var "t")))) & (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) ")" )) ")" )) "holds" (Bool "(" (Bool (Set ($#k1_scmpds_8 :::"while<0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k1_scmpds_8 :::"while<0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" )))))))) ; theorem :: SCMPDS_8:14 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" ($#k2_memstr_0 :::"the_Values_of"::: ) (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" ) ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_recdef_1 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "Q")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set (Set (Var "f")) ($#k1_recdef_1 :::"."::: ) (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "f")) ($#k1_recdef_1 :::"."::: ) (Set (Var "t")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) ")" )) ")" )) "holds" (Bool (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k1_scmpds_8 :::"while<0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k1_scmpds_8 :::"while<0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ")" ) ")" ))))))))) ; theorem :: SCMPDS_8: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" ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "Q")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" ))) & (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) ")" )) ")" )) "holds" (Bool "(" (Bool (Set ($#k1_scmpds_8 :::"while<0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k1_scmpds_8 :::"while<0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" ))))))) ; theorem :: SCMPDS_8:16 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "Q")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" ))) & (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) ")" )) ")" )) "holds" (Bool (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k1_scmpds_8 :::"while<0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k1_scmpds_8 :::"while<0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ")" ) ")" )))))))) ; begin definitionlet "a" be ($#m1_subset_1 :::"Int_position":::); let "i" be ($#m1_hidden :::"Integer":::); let "I" be ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); func :::"while>0"::: "(" "a" "," "i" "," "I" ")" -> ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_8:def 3 (Set (Set "(" (Set "(" "(" "a" "," "i" ")" ($#k8_scmpds_2 :::"<=0_goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) "I" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k2_scmpds_4 :::"';'"::: ) "I" ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k3_scmpds_2 :::"goto"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) "I" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" )); end; :: deftheorem defines :::"while>0"::: SCMPDS_8:def 3 : (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" "(" (Set (Var "a")) "," (Set (Var "i")) ")" ($#k8_scmpds_2 :::"<=0_goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k2_scmpds_4 :::"';'"::: ) (Set (Var "I")) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k3_scmpds_2 :::"goto"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" )))))); registrationlet "I" be ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "a" be ($#m1_subset_1 :::"Int_position":::); let "i" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k2_scmpds_8 :::"while>0"::: ) "(" "a" "," "i" "," "I" ")" ) -> ($#v3_scmpds_4 :::"shiftable"::: ) ; end; registrationlet "I" be ($#v2_compos_1 :::"halt-free"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "a" be ($#m1_subset_1 :::"Int_position":::); let "i" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k2_scmpds_8 :::"while>0"::: ) "(" "a" "," "i" "," "I" ")" ) -> ($#v2_compos_1 :::"halt-free"::: ) ; end; theorem :: SCMPDS_8:17 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "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 "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2)))))) ; theorem :: SCMPDS_8:18 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool "(" (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2))) "iff" (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ))) ")" ))))) ; theorem :: SCMPDS_8:19 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "i")) ")" ($#k8_scmpds_2 :::"<=0_goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ))) & (Bool (Set (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_scmpds_2 :::"goto"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" )))) ; theorem :: SCMPDS_8:20 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" )))))) ; theorem :: SCMPDS_8:21 (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 "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "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 "i")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (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"::: ) ) ")" ")" )))))))) ; theorem :: SCMPDS_8:22 (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 "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "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 "i")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (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_8:23 (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 "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "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 "i")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))))))))) ; scheme :: SCMPDS_8:sch 3 WhileGHalt{ F1( ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) )) -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F2() -> (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F3() -> ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F4() -> ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F5() -> ($#m1_subset_1 :::"Int_position":::), F6() -> ($#m1_hidden :::"Integer":::), P1[ ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) )] } : (Bool "(" (Bool (Set ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set F5 "(" ")" ) "," (Set F6 "(" ")" ) "," (Set F4 "(" ")" ) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set F2 "(" ")" ) "," (Set F3 "(" ")" )) & (Bool (Set ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set F5 "(" ")" ) "," (Set F6 "(" ")" ) "," (Set F4 "(" ")" ) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set F2 "(" ")" ) "," (Set F3 "(" ")" )) ")" ) provided (Bool "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool P1[(Set (Var "t"))]) & (Bool (Set F1 "(" (Set (Var "t")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ) ")" ) "," (Set F6 "(" ")" ) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) and (Bool P1[(Set F2 "(" ")" )]) and (Bool "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "Q")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool P1[(Set (Var "t"))]) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" )) ($#r1_hidden :::"="::: ) (Set (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ) ")" ) "," (Set F6 "(" ")" ) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set F4 "(" ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ))) & (Bool (Set F4 "(" ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set F4 "(" ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set F1 "(" (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set F4 "(" ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ")" ) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set F1 "(" (Set (Var "t")) ")" )) & (Bool P1[(Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set F4 "(" ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ))]) ")" ))) proof end; scheme :: SCMPDS_8:sch 4 WhileGExec{ F1( ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) )) -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F2() -> (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F3() -> ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F4() -> ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F5() -> ($#m1_subset_1 :::"Int_position":::), F6() -> ($#m1_hidden :::"Integer":::), P1[ ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) )] } : (Bool (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set F5 "(" ")" ) "," (Set F6 "(" ")" ) "," (Set F4 "(" ")" ) ")" ")" ) "," (Set F3 "(" ")" ) "," (Set F2 "(" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set F5 "(" ")" ) "," (Set F6 "(" ")" ) "," (Set F4 "(" ")" ) ")" ")" ) "," (Set F3 "(" ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set F4 "(" ")" ) "," (Set F3 "(" ")" ) "," (Set F2 "(" ")" ) ")" ")" ) ")" ) ")" )) provided (Bool (Set (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ) ")" ) "," (Set F6 "(" ")" ) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) and (Bool "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool P1[(Set (Var "t"))]) & (Bool (Set F1 "(" (Set (Var "t")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ) ")" ) "," (Set F6 "(" ")" ) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) and (Bool P1[(Set F2 "(" ")" )]) and (Bool "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "Q")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool P1[(Set (Var "t"))]) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" )) ($#r1_hidden :::"="::: ) (Set (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ) ")" ) "," (Set F6 "(" ")" ) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set F4 "(" ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ))) & (Bool (Set F4 "(" ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set F4 "(" ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set F1 "(" (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set F4 "(" ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ")" ) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set F1 "(" (Set (Var "t")) ")" )) & (Bool P1[(Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set F4 "(" ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ))]) ")" ))) proof end; theorem :: SCMPDS_8:24 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "," (Set (Var "c")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" ($#k2_memstr_0 :::"the_Values_of"::: ) (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" ) ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_recdef_1 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "c")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" ) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "Q")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "c")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" ) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set (Set (Var "f")) ($#k1_recdef_1 :::"."::: ) (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "f")) ($#k1_recdef_1 :::"."::: ) (Set (Var "t")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "c")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" ) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) ")" )) ")" )) "holds" (Bool "(" (Bool (Set ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" )))))))) ; theorem :: SCMPDS_8: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")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "," (Set (Var "c")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" ($#k2_memstr_0 :::"the_Values_of"::: ) (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" ) ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_recdef_1 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "c")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" ) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "Q")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "c")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" ) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set (Set (Var "f")) ($#k1_recdef_1 :::"."::: ) (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "f")) ($#k1_recdef_1 :::"."::: ) (Set (Var "t")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "c")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" ) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) ")" )) ")" )) "holds" (Bool (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ")" ) ")" ))))))))) ; theorem :: SCMPDS_8:26 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" ($#k2_memstr_0 :::"the_Values_of"::: ) (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" ) ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_recdef_1 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "Q")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set (Set (Var "f")) ($#k1_recdef_1 :::"."::: ) (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "f")) ($#k1_recdef_1 :::"."::: ) (Set (Var "t")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) ")" )) ")" )) "holds" (Bool "(" (Bool (Set ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ")" ) ")" )) ")" ")" )))))))) ; theorem :: SCMPDS_8:27 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "," (Set (Var "c")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "c")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" ) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "Q")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "c")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" ) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "c")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" ) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) ")" )) ")" )) "holds" (Bool "(" (Bool (Set ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ")" ) ")" )) ")" ")" ))))))) ; theorem :: SCMPDS_8:28 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "Q")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) ")" )) ")" )) "holds" (Bool "(" (Bool (Set ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ")" ) ")" )) ")" ")" ))))))) ; theorem :: SCMPDS_8:29 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "," (Set (Var "c")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "c")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" ) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "Q")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "c")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" ) ")" ))) ")" ) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "c")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" ) ")" ))) ")" ) ")" )) ")" )) "holds" (Bool "(" (Bool (Set ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ")" ) ")" )) ")" ")" ))))))) ;