:: SCPISORT semantic presentation begin definitionlet "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ); let "s" be ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "m" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); pred "f" :::"is_FinSequence_on"::: "s" "," "m" means :: SCPISORT:def 1 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "f"))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set "s" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set "(" "m" ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" ) ")" )))); end; :: deftheorem defines :::"is_FinSequence_on"::: SCPISORT:def 1 : (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_scpisort :::"is_FinSequence_on"::: ) (Set (Var "s")) "," (Set (Var "m"))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" ) ")" )))) ")" )))); theorem :: SCPISORT:1 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" ) ")" ))) ")" ) ")" )))) ; theorem :: SCPISORT:2 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Var "f")) ($#r1_scpisort :::"is_FinSequence_on"::: ) (Set (Var "s")) "," (Set (Var "m"))) ")" )))) ; theorem :: SCPISORT:3 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "m")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_hidden :::"<>"::: ) (Set (Var "m"))) & (Bool (Set (Var "k")) ($#r1_hidden :::"<>"::: ) (Set (Var "n"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")))) ")" )) "holds" (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ))) ; theorem :: SCPISORT:4 (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s2")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) ")" )) "holds" (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s2"))))) ; theorem :: SCPISORT:5 (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"::: ) ) (Bool "for" (Set (Var "j")) "being" ($#v4_scmpds_4 :::"shiftable"::: ) ($#v1_scmpds_5 :::"parahalting"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool "(" (Bool (Set (Set (Var "I")) ($#k3_scmpds_4 :::"';'"::: ) (Set (Var "j"))) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Set (Var "I")) ($#k3_scmpds_4 :::"';'"::: ) (Set (Var "j"))) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" ))))) ; theorem :: SCPISORT:6 (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" ($#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":::) "st" (Bool (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J")) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))))))) ; theorem :: SCPISORT:7 (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"::: ) ($#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":::) "st" (Bool (Bool (Set (Var "J")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) "," (Set (Var "P"))) & (Bool (Set (Var "J")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) "," (Set (Var "P")))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J")) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))))))) ; theorem :: SCPISORT:8 (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_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool "(" (Bool (Set (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J"))) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J"))) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" ))))) ; theorem :: SCPISORT: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" ($#v2_scmpds_4 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "J")) "being" ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Var "J")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ) "," (Set (Var "P"))) & (Bool (Set (Var "J")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ) "," (Set (Var "P")))) "holds" (Bool "(" (Bool (Set (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J"))) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J"))) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" ))))) ; theorem :: SCPISORT:10 (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" ($#v4_scmpds_4 :::"shiftable"::: ) ($#v1_scmpds_5 :::"parahalting"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool "(" (Bool (Set (Set (Var "I")) ($#k3_scmpds_4 :::"';'"::: ) (Set (Var "j"))) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Set (Var "I")) ($#k3_scmpds_4 :::"';'"::: ) (Set (Var "j"))) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" ))))) ; begin scheme :: SCPISORT:sch 1 ForDownHalt{ P1[ ($#m1_hidden :::"set"::: ) ], F1() -> (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F2() -> ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F3() -> ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F4() -> ($#m1_subset_1 :::"Int_position":::), F5() -> ($#m1_hidden :::"Integer":::), F6() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) } : (Bool "(" (Bool (Set ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set F4 "(" ")" ) "," (Set F5 "(" ")" ) "," (Set F6 "(" ")" ) "," (Set F3 "(" ")" ) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" )) & (Bool (Set ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set F4 "(" ")" ) "," (Set F5 "(" ")" ) "," (Set F6 "(" ")" ) "," (Set F3 "(" ")" ) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" )) ")" ) provided (Bool (Set F6 "(" ")" ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) and (Bool P1[(Set F1 "(" ")" )]) 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 F4 "(" ")" )) ($#r1_hidden :::"="::: ) (Set (Set F1 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F4 "(" ")" ))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set F1 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F4 "(" ")" ) ")" ) "," (Set F5 "(" ")" ) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" (Set F3 "(" ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set F4 "(" ")" ) "," (Set F5 "(" ")" ) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set F6 "(" ")" ) ")" ) ")" ")" ) ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set F4 "(" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set F4 "(" ")" ))) & (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" (Set F3 "(" ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set F4 "(" ")" ) "," (Set F5 "(" ")" ) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set F6 "(" ")" ) ")" ) ")" ")" ) ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set F1 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F4 "(" ")" ) ")" ) "," (Set F5 "(" ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set F1 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F4 "(" ")" ) ")" ) "," (Set F5 "(" ")" ) ")" ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set F6 "(" ")" ))) & (Bool (Set F3 "(" ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set F3 "(" ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool P1[(Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" (Set F3 "(" ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set F4 "(" ")" ) "," (Set F5 "(" ")" ) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set F6 "(" ")" ) ")" ) ")" ")" ) ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ))]) ")" ))) proof end; scheme :: SCPISORT:sch 2 ForDownExec{ P1[ ($#m1_hidden :::"set"::: ) ], F1() -> (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F2() -> ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F3() -> ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F4() -> ($#m1_subset_1 :::"Int_position":::), F5() -> ($#m1_hidden :::"Integer":::), F6() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) } : (Bool (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set F4 "(" ")" ) "," (Set F5 "(" ")" ) "," (Set F6 "(" ")" ) "," (Set F3 "(" ")" ) ")" ")" ) "," (Set F2 "(" ")" ) "," (Set F1 "(" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set F4 "(" ")" ) "," (Set F5 "(" ")" ) "," (Set F6 "(" ")" ) "," (Set F3 "(" ")" ) ")" ")" ) "," (Set F2 "(" ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" (Set F3 "(" ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set F4 "(" ")" ) "," (Set F5 "(" ")" ) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set F6 "(" ")" ) ")" ) ")" ")" ) ")" ) "," (Set F2 "(" ")" ) "," (Set F1 "(" ")" ) ")" ")" ) ")" ) ")" )) provided (Bool (Set F6 "(" ")" ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) and (Bool (Set (Set F1 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set F1 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F4 "(" ")" ) ")" ) "," (Set F5 "(" ")" ) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) and (Bool P1[(Set F1 "(" ")" )]) 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 F4 "(" ")" )) ($#r1_hidden :::"="::: ) (Set (Set F1 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F4 "(" ")" ))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set F1 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F4 "(" ")" ) ")" ) "," (Set F5 "(" ")" ) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" (Set F3 "(" ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set F4 "(" ")" ) "," (Set F5 "(" ")" ) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set F6 "(" ")" ) ")" ) ")" ")" ) ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set F4 "(" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set F4 "(" ")" ))) & (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" (Set F3 "(" ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set F4 "(" ")" ) "," (Set F5 "(" ")" ) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set F6 "(" ")" ) ")" ) ")" ")" ) ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set F1 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F4 "(" ")" ) ")" ) "," (Set F5 "(" ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set F1 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F4 "(" ")" ) ")" ) "," (Set F5 "(" ")" ) ")" ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set F6 "(" ")" ))) & (Bool (Set F3 "(" ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set F3 "(" ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool P1[(Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" (Set F3 "(" ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set F4 "(" ")" ) "," (Set F5 "(" ")" ) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set F6 "(" ")" ) ")" ) ")" ")" ) ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ))]) ")" ))) proof end; scheme :: SCPISORT:sch 3 ForDownEnd{ P1[ ($#m1_hidden :::"set"::: ) ], F1() -> (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F2() -> ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F3() -> ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F4() -> ($#m1_subset_1 :::"Int_position":::), F5() -> ($#m1_hidden :::"Integer":::), F6() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) } : (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set F4 "(" ")" ) "," (Set F5 "(" ")" ) "," (Set F6 "(" ")" ) "," (Set F2 "(" ")" ) ")" ")" ) "," (Set F3 "(" ")" ) "," (Set F1 "(" ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set F1 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F4 "(" ")" ) ")" ) "," (Set F5 "(" ")" ) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool P1[(Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set F4 "(" ")" ) "," (Set F5 "(" ")" ) "," (Set F6 "(" ")" ) "," (Set F2 "(" ")" ) ")" ")" ) "," (Set F3 "(" ")" ) "," (Set F1 "(" ")" ) ")" ")" ))]) ")" ) provided (Bool (Set F6 "(" ")" ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) and (Bool P1[(Set F1 "(" ")" )]) and (Bool "for" (Set (Var "Q")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (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 (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set F4 "(" ")" )) ($#r1_hidden :::"="::: ) (Set (Set F1 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F4 "(" ")" ))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set F1 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F4 "(" ")" ) ")" ) "," (Set F5 "(" ")" ) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" (Set F2 "(" ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set F4 "(" ")" ) "," (Set F5 "(" ")" ) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set F6 "(" ")" ) ")" ) ")" ")" ) ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set F4 "(" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set F4 "(" ")" ))) & (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" (Set F2 "(" ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set F4 "(" ")" ) "," (Set F5 "(" ")" ) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set F6 "(" ")" ) ")" ) ")" ")" ) ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set F1 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F4 "(" ")" ) ")" ) "," (Set F5 "(" ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set F1 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F4 "(" ")" ) ")" ) "," (Set F5 "(" ")" ) ")" ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set F6 "(" ")" ))) & (Bool (Set F2 "(" ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set F2 "(" ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool P1[(Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" (Set F2 "(" ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set F4 "(" ")" ) "," (Set F5 "(" ")" ) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set F6 "(" ")" ) ")" ) ")" ")" ) ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ))]) ")" ))) proof end; theorem :: SCPISORT: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" ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "," (Set (Var "c")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c")))) & (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 (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c")))) & (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 "(" (Set (Var "I")) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "n")) ")" ) ")" ")" ) ")" ) "," (Set (Var "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 "(" (Set (Var "I")) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "n")) ")" ) ")" ")" ) ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "n")))) & (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 "(" (Set (Var "I")) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "n")) ")" ) ")" ")" ) ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set "(" (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" (Set (Var "I")) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "n")) ")" ) ")" ")" ) ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c")))) ")" )) ")" )) "holds" (Bool "(" (Bool (Set ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" ))))))) ; theorem :: SCPISORT: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" ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "," (Set (Var "c")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c")))) & (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 (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c")))) & (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 "(" (Set (Var "I")) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "n")) ")" ) ")" ")" ) ")" ) "," (Set (Var "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 "(" (Set (Var "I")) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "n")) ")" ) ")" ")" ) ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "n")))) & (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 "(" (Set (Var "I")) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "n")) ")" ) ")" ")" ) ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set "(" (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" (Set (Var "I")) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "n")) ")" ) ")" ")" ) ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c")))) ")" )) ")" )) "holds" (Bool (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" (Set (Var "I")) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "n")) ")" ) ")" ")" ) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ")" ) ")" )))))))) ; theorem :: SCPISORT: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 "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" )) & (Bool "(" "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "Q")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" ))) & (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) ")" )) ")" )) "holds" (Bool "(" (Bool (Set ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "I")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" ))))))) ; begin definitionlet "n", "p0" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"insert-sort"::: "(" "n" "," "p0" ")" -> ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCPISORT:def 2 (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) ($#k5_scmpds_2 :::":="::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 1) ")" ($#k10_scmpds_2 :::":="::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) ")" ($#k10_scmpds_2 :::":="::: ) (Set "(" "n" ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) ")" ($#k10_scmpds_2 :::":="::: ) "p0" ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) "," (Num 1) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) "," (Num 1) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 4) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 1) "," (Num 1) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 6) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 1) ")" ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 6) "," (Set "(" (Set "(" (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 4) ")" ) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" ($#k13_scmpds_2 :::"SubFrom"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) "," (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 4) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k3_scmpds_6 :::"if>0"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 4) ")" ) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 4) ")" ) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 4) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 4) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 4) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 6) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ")" ) ")" ) "," (Set "(" ($#k9_compos_1 :::"Load"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 6) ")" ($#k10_scmpds_2 :::":="::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ) ")" ")" )); end; :: deftheorem defines :::"insert-sort"::: SCPISORT:def 2 : (Bool "for" (Set (Var "n")) "," (Set (Var "p0")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_scpisort :::"insert-sort"::: ) "(" (Set (Var "n")) "," (Set (Var "p0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) ($#k5_scmpds_2 :::":="::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 1) ")" ($#k10_scmpds_2 :::":="::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) ")" ($#k10_scmpds_2 :::":="::: ) (Set "(" (Set (Var "n")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) ")" ($#k10_scmpds_2 :::":="::: ) (Set (Var "p0")) ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k2_scmpds_7 :::"for-down"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) "," (Num 1) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) "," (Num 1) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 4) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 1) "," (Num 1) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 6) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 1) ")" ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 6) "," (Set "(" (Set "(" (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 4) ")" ) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" ($#k13_scmpds_2 :::"SubFrom"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) "," (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 4) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k3_scmpds_6 :::"if>0"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 4) ")" ) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 4) ")" ) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 4) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 4) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 4) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 6) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ")" ) ")" ) "," (Set "(" ($#k9_compos_1 :::"Load"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 6) ")" ($#k10_scmpds_2 :::":="::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ) ")" ")" )))); begin theorem :: SCPISORT:14 (Bool "for" (Set (Var "n")) "," (Set (Var "p0")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_scpisort :::"insert-sort"::: ) "(" (Set (Var "n")) "," (Set (Var "p0")) ")" ")" )) ($#r1_hidden :::"="::: ) (Num 23))) ; theorem :: SCPISORT:15 (Bool "for" (Set (Var "p0")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p0")) ($#r1_xxreal_0 :::">="::: ) (Num 7))) "holds" (Bool (Set ($#k1_scpisort :::"insert-sort"::: ) "(" (Set (Var "n")) "," (Set (Var "p0")) ")" ) "is" ($#v2_scmpds_4 :::"parahalting"::: ) )) ; theorem :: SCPISORT: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 "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) (Bool "for" (Set (Var "k0")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 4) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set (Num 7) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 6) ")" ) ")" ))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set ($#k2_scmp_gcd :::"GBP"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 6) ")" ))) & (Bool (Set (Var "k0")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 4) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 6) ")" ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) & (Bool (Set (Var "f")) ($#r1_scpisort :::"is_FinSequence_on"::: ) (Set (Var "s")) "," (Set (Var "k0"))) & (Bool (Set (Var "g")) ($#r1_scpisort :::"is_FinSequence_on"::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 6) "," (Set "(" (Set "(" (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 4) ")" ) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" ($#k13_scmpds_2 :::"SubFrom"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) "," (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 4) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k3_scmpds_6 :::"if>0"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 4) ")" ) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 4) ")" ) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 4) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 4) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 4) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 6) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ")" ) ")" ) "," (Set "(" ($#k9_compos_1 :::"Load"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 6) ")" ($#k10_scmpds_2 :::":="::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ")" ) ")" ) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) "," (Set (Var "k0"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">"::: ) (Set (Var "k"))) & (Bool (Set (Var "f")) ($#r3_graph_2 :::"is_non_decreasing_on"::: ) (Num 1) "," (Set (Var "k")))) "holds" (Bool "(" (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ) & (Bool (Set (Var "g")) ($#r3_graph_2 :::"is_non_decreasing_on"::: ) (Num 1) "," (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">"::: ) (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool "ex" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")))) ")" )) ")" ) ")" ))))) ; theorem :: SCPISORT:17 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) (Bool "for" (Set (Var "p0")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p0")) ($#r1_xxreal_0 :::">="::: ) (Num 6)) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Var "f")) ($#r1_scpisort :::"is_FinSequence_on"::: ) (Set (Var "s")) "," (Set (Var "p0"))) & (Bool (Set (Var "g")) ($#r1_scpisort :::"is_FinSequence_on"::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k1_scpisort :::"insert-sort"::: ) "(" (Set (Var "n")) "," (Set "(" (Set (Var "p0")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) "," (Set (Var "p0")))) "holds" (Bool "(" (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ) & (Bool (Set (Var "g")) ($#r3_graph_2 :::"is_non_decreasing_on"::: ) (Num 1) "," (Set (Var "n"))) ")" ))))) ;