:: SCPQSORT semantic presentation begin registrationlet "I", "J" be ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "a" be ($#m1_subset_1 :::"Int_position":::); let "k1" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k3_scmpds_6 :::"if>0"::: ) "(" "a" "," "k1" "," "I" "," "J" ")" ) -> ($#v3_scmpds_4 :::"shiftable"::: ) ; end; theorem :: SCPQSORT:1 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "J")) "being" ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (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 "(" ($#k3_scmpds_6 :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))))))))) ; theorem :: SCPQSORT:2 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "," (Set (Var "sm")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (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 "m")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2))) & (Bool (Set (Var "sm")) ($#r6_pboole :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set (Var "m")) ")" ))) "holds" (Bool "(" (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "sm"))) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ))) & (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "sm"))) ($#r6_pboole :::"="::: ) (Set (Var "sm"))) ")" ))))))) ; theorem :: SCPQSORT:3 (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"::: ) ) "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 (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s"))))) "holds" (Bool (Set (Var "I")) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "t")) "," (Set (Var "Q")))) ")" )) "holds" (Bool (Set (Var "I")) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P")))))) ; theorem :: SCPQSORT:4 (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "," (Set (Var "i4")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "i1")) ($#k4_scmpds_4 :::"';'"::: ) (Set (Var "i2")) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set (Var "i3")) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set (Var "i4")) ")" )) ($#r1_hidden :::"="::: ) (Num 4))) ; theorem :: SCPQSORT:5 (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":::) "st" (Bool (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 (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 "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) & (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 (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 (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) ")" )) ")" )) "holds" (Bool "(" (Bool (Set ($#k2_scmpds_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")) ")" ) ($#r6_pboole :::"="::: ) (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 :: SCPQSORT: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"::: ) ($#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":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_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 (Var "c"))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) & (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 (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 (Var "c"))) & (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) ")" )) ")" )) "holds" (Bool "(" (Bool (Set ($#k2_scmpds_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")) ")" ) ($#r6_pboole :::"="::: ) (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 :: SCPQSORT: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"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "," (Set (Var "c")) "," (Set (Var "md")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x4"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x3")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x1")) ")" ))) & (Bool (Set (Var "md")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x3")) ")" ) ($#k6_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 "x4"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x3")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x1")) ")" ))) & (Bool (Set (Var "md")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x3")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c")))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "x2")))) & (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 (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x4"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x3")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (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 (Var "x1")) ")" ))) & (Bool (Set (Var "md")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x3")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c")))) & (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "x2")))) ")" )) ")" )) "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")) ")" ) ($#r6_pboole :::"="::: ) (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 :: SCPQSORT:8 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) (Bool "for" (Set (Var "m")) "," (Set (Var "k1")) "," (Set (Var "k")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) & (Bool (Set (Var "f")) ($#r3_graph_2 :::"is_non_decreasing_on"::: ) (Set (Var "m")) "," (Set (Var "k1"))) & (Bool (Set (Var "f")) ($#r3_graph_2 :::"is_non_decreasing_on"::: ) (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) "," (Set (Var "n"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")))) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" )) "holds" (Bool (Set (Var "f")) ($#r3_graph_2 :::"is_non_decreasing_on"::: ) (Set (Var "m")) "," (Set (Var "n"))))) ; begin definitionfunc :::"Partition"::: -> ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCPQSORT:def 1 (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 4) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" ($#k13_scmpds_2 :::"SubFrom"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) "," (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) "," (Num 1) ")" ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) "," (Set "(" (Set "(" (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 7) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 6) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 4) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k13_scmpds_2 :::"SubFrom"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 6) "," (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 2) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k3_scmpds_6 :::"if>0"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 6) "," (Set "(" (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 4) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 7) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ")" ) ")" ) "," (Set "(" ($#k9_compos_1 :::"Load"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) ")" ($#k10_scmpds_2 :::":="::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ")" ) ")" ) ")" ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 7) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 7) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 7) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 6) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 2) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k13_scmpds_2 :::"SubFrom"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 6) "," (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 3) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k3_scmpds_6 :::"if>0"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 6) "," (Set "(" (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) "," (Num 1) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ")" ) ")" ) "," (Set "(" ($#k9_compos_1 :::"Load"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 7) ")" ($#k10_scmpds_2 :::":="::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k7_scmpds_6 :::"if>0"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 6) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 4) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 4) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 3) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 3) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 6) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 2) ")" ) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) "," (Num 1) ")" ")" ) ")" ) ($#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 "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 6) ")" ($#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 "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 2) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 2) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 6) ")" ")" )); end; :: deftheorem defines :::"Partition"::: SCPQSORT:def 1 : (Bool (Set ($#k1_scpqsort :::"Partition"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 4) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" ($#k13_scmpds_2 :::"SubFrom"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) "," (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) "," (Num 1) ")" ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) "," (Set "(" (Set "(" (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 7) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 6) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 4) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k13_scmpds_2 :::"SubFrom"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 6) "," (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 2) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k3_scmpds_6 :::"if>0"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 6) "," (Set "(" (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 4) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 7) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ")" ) ")" ) "," (Set "(" ($#k9_compos_1 :::"Load"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) ")" ($#k10_scmpds_2 :::":="::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ")" ) ")" ) ")" ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 7) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 7) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 7) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 6) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 2) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k13_scmpds_2 :::"SubFrom"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 6) "," (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 3) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k3_scmpds_6 :::"if>0"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 6) "," (Set "(" (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) "," (Num 1) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ")" ) ")" ) "," (Set "(" ($#k9_compos_1 :::"Load"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 7) ")" ($#k10_scmpds_2 :::":="::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k7_scmpds_6 :::"if>0"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 6) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 4) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 4) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 3) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 3) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 6) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 5) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 2) ")" ) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) "," (Num 1) ")" ")" ) ")" ) ($#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 "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 6) ")" ($#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 "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 2) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 2) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 6) ")" ")" ))); begin definitionlet "n", "p0" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"QuickSort"::: "(" "n" "," "p0" ")" -> ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCPQSORT:def 2 (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) ($#k5_scmpds_2 :::":="::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" (Set ($#k3_scmp_gcd :::"SBP"::: ) ) ($#k5_scmpds_2 :::":="::: ) (Num 1) ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k3_scmp_gcd :::"SBP"::: ) ) "," (Set "(" "p0" ($#k2_nat_1 :::"+"::: ) "n" ")" ) ")" ($#k10_scmpds_2 :::":="::: ) (Set "(" "p0" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k3_scmp_gcd :::"SBP"::: ) ) "," (Set "(" (Set "(" "p0" ($#k2_nat_1 :::"+"::: ) "n" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ($#k10_scmpds_2 :::":="::: ) (Set "(" "p0" ($#k2_nat_1 :::"+"::: ) "n" ")" ) ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 1) "," (Set "(" (Set "(" (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k3_scmp_gcd :::"SBP"::: ) ) "," (Set "(" (Set "(" "p0" ($#k2_nat_1 :::"+"::: ) "n" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" ($#k13_scmpds_2 :::"SubFrom"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) "," (Set ($#k3_scmp_gcd :::"SBP"::: ) ) "," (Set "(" "p0" ($#k2_nat_1 :::"+"::: ) "n" ")" ) ")" ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k3_scmpds_6 :::"if>0"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) "," (Set "(" (Set "(" (Set "(" (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k3_scmp_gcd :::"SBP"::: ) ) "," (Set "(" "p0" ($#k2_nat_1 :::"+"::: ) "n" ")" ) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 4) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k3_scmp_gcd :::"SBP"::: ) ) "," (Set "(" (Set "(" "p0" ($#k2_nat_1 :::"+"::: ) "n" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set ($#k1_scpqsort :::"Partition"::: ) ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" "(" (Set ($#k3_scmp_gcd :::"SBP"::: ) ) "," (Set "(" (Set "(" "p0" ($#k2_nat_1 :::"+"::: ) "n" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k3_scmp_gcd :::"SBP"::: ) ) "," (Set "(" (Set "(" "p0" ($#k2_nat_1 :::"+"::: ) "n" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k3_scmp_gcd :::"SBP"::: ) ) "," (Set "(" (Set "(" "p0" ($#k2_nat_1 :::"+"::: ) "n" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 4) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k3_scmp_gcd :::"SBP"::: ) ) "," (Set "(" (Set "(" "p0" ($#k2_nat_1 :::"+"::: ) "n" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 4) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k3_scmp_gcd :::"SBP"::: ) ) "," (Set "(" (Set "(" "p0" ($#k2_nat_1 :::"+"::: ) "n" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k3_scmp_gcd :::"SBP"::: ) ) "," (Set "(" (Set "(" "p0" ($#k2_nat_1 :::"+"::: ) "n" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) "," (Num 1) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 1) "," (Num 2) ")" ")" ) ")" ) ")" ) "," (Set "(" ($#k9_compos_1 :::"Load"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 1) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 2) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ) ")" ")" )); end; :: deftheorem defines :::"QuickSort"::: SCPQSORT:def 2 : (Bool "for" (Set (Var "n")) "," (Set (Var "p0")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k2_scpqsort :::"QuickSort"::: ) "(" (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 ($#k3_scmp_gcd :::"SBP"::: ) ) ($#k5_scmpds_2 :::":="::: ) (Num 1) ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k3_scmp_gcd :::"SBP"::: ) ) "," (Set "(" (Set (Var "p0")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ")" ($#k10_scmpds_2 :::":="::: ) (Set "(" (Set (Var "p0")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k3_scmp_gcd :::"SBP"::: ) ) "," (Set "(" (Set "(" (Set (Var "p0")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ($#k10_scmpds_2 :::":="::: ) (Set "(" (Set (Var "p0")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 1) "," (Set "(" (Set "(" (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k3_scmp_gcd :::"SBP"::: ) ) "," (Set "(" (Set "(" (Set (Var "p0")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" ($#k13_scmpds_2 :::"SubFrom"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) "," (Set ($#k3_scmp_gcd :::"SBP"::: ) ) "," (Set "(" (Set (Var "p0")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ")" ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k3_scmpds_6 :::"if>0"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) "," (Set "(" (Set "(" (Set "(" (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k3_scmp_gcd :::"SBP"::: ) ) "," (Set "(" (Set (Var "p0")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 4) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k3_scmp_gcd :::"SBP"::: ) ) "," (Set "(" (Set "(" (Set (Var "p0")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set ($#k1_scpqsort :::"Partition"::: ) ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" "(" (Set ($#k3_scmp_gcd :::"SBP"::: ) ) "," (Set "(" (Set "(" (Set (Var "p0")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k3_scmp_gcd :::"SBP"::: ) ) "," (Set "(" (Set "(" (Set (Var "p0")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k3_scmp_gcd :::"SBP"::: ) ) "," (Set "(" (Set "(" (Set (Var "p0")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 4) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k3_scmp_gcd :::"SBP"::: ) ) "," (Set "(" (Set "(" (Set (Var "p0")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 4) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k3_scmp_gcd :::"SBP"::: ) ) "," (Set "(" (Set "(" (Set (Var "p0")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k3_scmp_gcd :::"SBP"::: ) ) "," (Set "(" (Set "(" (Set (Var "p0")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) "," (Num 1) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 1) "," (Num 2) ")" ")" ) ")" ) ")" ) "," (Set "(" ($#k9_compos_1 :::"Load"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 1) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 2) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ) ")" ")" )))); begin theorem :: SCPQSORT:9 (Bool (Set ($#k5_card_1 :::"card"::: ) (Set ($#k1_scpqsort :::"Partition"::: ) )) ($#r1_hidden :::"="::: ) (Num 38)) ; theorem :: SCPQSORT: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 "md")) "," (Set (Var "p0")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set ($#k2_scmp_gcd :::"GBP"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "md"))) & (Bool (Set (Var "md")) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "p0")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "p0")) ($#r1_xxreal_0 :::">="::: ) (Num 7))) "holds" (Bool "(" (Bool (Set ($#k1_scpqsort :::"Partition"::: ) ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k1_scpqsort :::"Partition"::: ) ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" )))) ; theorem :: SCPQSORT: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 "md")) "," (Set (Var "p0")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "," (Set (Var "f1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set ($#k2_scmp_gcd :::"GBP"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (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 2) ")" ) ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "md"))) & (Bool (Set (Var "md")) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "p0")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 4) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "p0")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")))) & (Bool (Set (Var "p0")) ($#r1_xxreal_0 :::">="::: ) (Num 7)) & (Bool (Set (Var "f")) ($#r1_scpisort :::"is_FinSequence_on"::: ) (Set (Var "s")) "," (Set (Var "p0"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Var "f1")) ($#r1_scpisort :::"is_FinSequence_on"::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set ($#k1_scpqsort :::"Partition"::: ) ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) "," (Set (Var "p0"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set (Var "n")))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set ($#k1_scpqsort :::"Partition"::: ) ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k2_scmp_gcd :::"GBP"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set ($#k1_scpqsort :::"Partition"::: ) ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 1) ")" ))) & (Bool (Set (Var "f")) "," (Set (Var "f1")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ) & (Bool "ex" (Set (Var "m4")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "m4")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set ($#k1_scpqsort :::"Partition"::: ) ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 4) ")" ))) & (Bool (Set (Var "md")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m4"))) & (Bool (Set (Var "m4")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 4) ")" ))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "md")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m4")))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set ($#k1_scpqsort :::"Partition"::: ) ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "m4")) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set ($#k1_scpqsort :::"Partition"::: ) ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "i")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m4")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 4) ")" )))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set ($#k1_scpqsort :::"Partition"::: ) ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "m4")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set ($#k1_scpqsort :::"Partition"::: ) ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "i")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "p0")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool "(" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 2) ")" ))) "or" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">"::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 4) ")" ))) ")" )) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set ($#k1_scpqsort :::"Partition"::: ) ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "i")) ")" ))) ")" ) ")" )) ")" ))))) ; theorem :: SCPQSORT:12 (Bool "(" (Bool (Set ($#k1_scpqsort :::"Partition"::: ) ) "is" ($#v2_compos_1 :::"halt-free"::: ) ) & (Bool (Set ($#k1_scpqsort :::"Partition"::: ) ) "is" ($#v3_scmpds_4 :::"shiftable"::: ) ) ")" ) ; begin theorem :: SCPQSORT:13 (Bool "for" (Set (Var "n")) "," (Set (Var "p0")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_scpqsort :::"QuickSort"::: ) "(" (Set (Var "n")) "," (Set (Var "p0")) ")" ")" )) ($#r1_hidden :::"="::: ) (Num 57))) ; theorem :: SCPQSORT:14 (Bool "for" (Set (Var "p0")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p0")) ($#r1_xxreal_0 :::">="::: ) (Num 7))) "holds" (Bool (Set ($#k2_scpqsort :::"QuickSort"::: ) "(" (Set (Var "n")) "," (Set (Var "p0")) ")" ) "is" ($#v2_scmpds_4 :::"parahalting"::: ) )) ; theorem :: SCPQSORT: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 "p0")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p0")) ($#r1_xxreal_0 :::">="::: ) (Num 7))) "holds" (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "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 "p0"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Var "g")) ($#r1_scpisort :::"is_FinSequence_on"::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scpqsort :::"QuickSort"::: ) "(" (Set (Var "n")) "," (Set (Var "p0")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) "," (Set (Var "p0"))) & (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"))) ")" ))))) ;