:: SCPINVAR semantic presentation begin theorem :: SCPINVAR:1 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set (Var "i")) ($#k4_scmpds_4 :::"';'"::: ) (Set (Var "j")) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "I")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "i"))) & (Bool (Set (Set "(" (Set "(" (Set (Var "i")) ($#k4_scmpds_4 :::"';'"::: ) (Set (Var "j")) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "I")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "j"))) ")" ))) ; theorem :: SCPINVAR:2 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" ($#k2_memstr_0 :::"the_Values_of"::: ) (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" ) ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k4_xxreal_0 :::"max"::: ) "(" (Set "(" ($#k1_int_2 :::"abs"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ")" ) "," (Set "(" ($#k1_int_2 :::"abs"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) ")" ) ")" )) ")" ")" )))) ; theorem :: SCPINVAR:3 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" ($#k2_memstr_0 :::"the_Values_of"::: ) (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" ) ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ))) ")" ")" )))) ; begin scheme :: SCPINVAR:sch 1 WhileLEnd{ F1( ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) )) -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F2() -> (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F3() -> ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F4() -> ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F5() -> ($#m1_subset_1 :::"Int_position":::), F6() -> ($#m1_hidden :::"Integer":::), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "(" (Bool (Set F1 "(" (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k1_scmpds_8 :::"while<0"::: ) "(" (Set F5 "(" ")" ) "," (Set F6 "(" ")" ) "," (Set F4 "(" ")" ) ")" ")" ) "," (Set F3 "(" ")" ) "," (Set F2 "(" ")" ) ")" ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool P1[(Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k1_scmpds_8 :::"while<0"::: ) "(" (Set F5 "(" ")" ) "," (Set F6 "(" ")" ) "," (Set F4 "(" ")" ) ")" ")" ) "," (Set F3 "(" ")" ) "," (Set F2 "(" ")" ) ")" ")" ))]) ")" ) provided (Bool "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool P1[(Set (Var "t"))])) "holds" (Bool "(" (Bool (Set F1 "(" (Set (Var "t")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ) ")" ) "," (Set F6 "(" ")" ) ")" ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) and (Bool P1[(Set F2 "(" ")" )]) and (Bool "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "Q")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool P1[(Set (Var "t"))]) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" )) ($#r1_hidden :::"="::: ) (Set (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ) ")" ) "," (Set F6 "(" ")" ) ")" ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set F4 "(" ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ))) & (Bool (Set F4 "(" ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set F4 "(" ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set F1 "(" (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set F4 "(" ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ")" ) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set F1 "(" (Set (Var "t")) ")" )) & (Bool P1[(Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set F4 "(" ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ))]) ")" ))) proof end; begin definitionlet "n", "p0" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"sum"::: "(" "n" "," "p0" ")" -> ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCPINVAR:def 1 (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) ($#k5_scmpds_2 :::":="::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 1) ")" ) ($#k5_scmpds_2 :::":="::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 2) ")" ) ($#k5_scmpds_2 :::":="::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) "n" ")" ) ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 3) ")" ) ($#k5_scmpds_2 :::":="::: ) (Set "(" "p0" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k1_scmpds_8 :::"while<0"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) "," (Set "(" (Set "(" (Set "(" ($#k12_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 1) "," (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 3) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) "," (Num 1) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) "," (Num 1) ")" ")" ) ")" ) ")" ")" )); end; :: deftheorem defines :::"sum"::: SCPINVAR:def 1 : (Bool "for" (Set (Var "n")) "," (Set (Var "p0")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_scpinvar :::"sum"::: ) "(" (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 "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 1) ")" ) ($#k5_scmpds_2 :::":="::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 2) ")" ) ($#k5_scmpds_2 :::":="::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 3) ")" ) ($#k5_scmpds_2 :::":="::: ) (Set "(" (Set (Var "p0")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k1_scmpds_8 :::"while<0"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) "," (Set "(" (Set "(" (Set "(" ($#k12_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 1) "," (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 3) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) "," (Num 1) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) "," (Num 1) ")" ")" ) ")" ) ")" ")" )))); definitionlet "ff" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" ($#k2_memstr_0 :::"the_Values_of"::: ) (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" ) ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ); let "s" be ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); :: original: :::"."::: redefine func "ff" :::"."::: "s" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; theorem :: SCPINVAR:4 (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 "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "," (Set (Var "p0")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool (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 (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p0")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (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 "ex" (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_scpisort :::"is_FinSequence_on"::: ) (Set (Var "s")) "," (Set (Var "p0"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "i")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k1_gr_cy_1 :::"Sum"::: ) (Set (Var "g")))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p0")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")) ")" ))) ")" )) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "i")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (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 (Var "p0")))) "holds" (Bool (Set (Set (Var "t")) ($#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")) ")" ))) ")" )) "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 ($#k6_numbers :::"0"::: ) )) & (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 "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "i")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1))) & (Bool "ex" (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_scpisort :::"is_FinSequence_on"::: ) (Set (Var "s")) "," (Set (Var "p0"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "i")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1))) & (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p0")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")) ")" ))) & (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k1_gr_cy_1 :::"Sum"::: ) (Set (Var "g")))) ")" )) & (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 (Var "p0")))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#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")) ")" ))) ")" ) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k1_scmpds_8 :::"while<0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k1_gr_cy_1 :::"Sum"::: ) (Set (Var "f")))) & (Bool (Set ($#k1_scmpds_8 :::"while<0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k1_scmpds_8 :::"while<0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" ))))))) ; theorem :: SCPINVAR: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 "n")) "," (Set (Var "p0")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool (Bool (Set (Var "p0")) ($#r1_xxreal_0 :::">="::: ) (Num 3)) & (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")))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k1_scpinvar :::"sum"::: ) "(" (Set (Var "n")) "," (Set (Var "p0")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_gr_cy_1 :::"Sum"::: ) (Set (Var "f")))) & (Bool (Set ($#k1_scpinvar :::"sum"::: ) "(" (Set (Var "n")) "," (Set (Var "p0")) ")" ) "is" ($#v2_scmpds_4 :::"parahalting"::: ) ) ")" ))))) ; begin scheme :: SCPINVAR:sch 2 WhileGEnd{ F1( ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) )) -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F2() -> (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F3() -> ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F4() -> ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F5() -> ($#m1_subset_1 :::"Int_position":::), F6() -> ($#m1_hidden :::"Integer":::), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "(" (Bool (Set F1 "(" (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set F5 "(" ")" ) "," (Set F6 "(" ")" ) "," (Set F4 "(" ")" ) ")" ")" ) "," (Set F3 "(" ")" ) "," (Set F2 "(" ")" ) ")" ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool P1[(Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set F5 "(" ")" ) "," (Set F6 "(" ")" ) "," (Set F4 "(" ")" ) ")" ")" ) "," (Set F3 "(" ")" ) "," (Set F2 "(" ")" ) ")" ")" ))]) ")" ) provided (Bool "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool P1[(Set (Var "t"))])) "holds" (Bool "(" (Bool (Set F1 "(" (Set (Var "t")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ) ")" ) "," (Set F6 "(" ")" ) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) and (Bool P1[(Set F2 "(" ")" )]) and (Bool "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "Q")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool P1[(Set (Var "t"))]) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" )) ($#r1_hidden :::"="::: ) (Set (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ) ")" ) "," (Set F6 "(" ")" ) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set F4 "(" ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ))) & (Bool (Set F4 "(" ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set F4 "(" ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set F1 "(" (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set F4 "(" ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ")" ) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set F1 "(" (Set (Var "t")) ")" )) & (Bool P1[(Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set F4 "(" ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ))]) ")" ))) proof end; begin definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"Fib-macro"::: "n" -> ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCPINVAR:def 2 (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) ($#k5_scmpds_2 :::":="::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 1) ")" ) ($#k5_scmpds_2 :::":="::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 2) ")" ) ($#k5_scmpds_2 :::":="::: ) (Num 1) ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 3) ")" ) ($#k5_scmpds_2 :::":="::: ) "n" ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) "," (Set "(" (Set "(" (Set "(" (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 4) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" ($#k12_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) "," (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 1) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 1) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 4) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ")" )); end; :: deftheorem defines :::"Fib-macro"::: SCPINVAR:def 2 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_scpinvar :::"Fib-macro"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) ($#k5_scmpds_2 :::":="::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 1) ")" ) ($#k5_scmpds_2 :::":="::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 2) ")" ) ($#k5_scmpds_2 :::":="::: ) (Num 1) ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 3) ")" ) ($#k5_scmpds_2 :::":="::: ) (Set (Var "n")) ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) "," (Set "(" (Set "(" (Set "(" (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 4) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) ")" ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" ($#k12_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) "," (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 1) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 1) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 4) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ")" )))); theorem :: SCPINVAR: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 "f0")) "," (Set (Var "f1")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "f0"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (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"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "i")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "k")))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "f0"))) ($#r1_hidden :::"="::: ) (Set ($#k1_pre_ff :::"Fib"::: ) (Set (Var "k")))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_pre_ff :::"Fib"::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (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 ($#k6_numbers :::"0"::: ) )) & (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 "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Set (Var "i")) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) & (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "f0"))) ($#r1_hidden :::"="::: ) (Set ($#k1_pre_ff :::"Fib"::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_pre_ff :::"Fib"::: ) (Set "(" (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" ))) ")" )) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "f0"))) ($#r1_hidden :::"="::: ) (Set ($#k1_pre_ff :::"Fib"::: ) (Set (Var "n")))) & (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_pre_ff :::"Fib"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k2_scmpds_8 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" )))))) ; theorem :: SCPINVAR: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 "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k3_scpinvar :::"Fib-macro"::: ) (Set (Var "n")) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_pre_ff :::"Fib"::: ) (Set (Var "n")))) & (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k3_scpinvar :::"Fib-macro"::: ) (Set (Var "n")) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_pre_ff :::"Fib"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set ($#k3_scpinvar :::"Fib-macro"::: ) (Set (Var "n"))) "is" ($#v2_scmpds_4 :::"parahalting"::: ) ) ")" )))) ; begin definitionlet "a" be ($#m1_subset_1 :::"Int_position":::); let "i" be ($#m1_hidden :::"Integer":::); let "I" be ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); func :::"while<>0"::: "(" "a" "," "i" "," "I" ")" -> ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCPINVAR:def 3 (Set (Set "(" (Set "(" (Set "(" "(" "a" "," "i" ")" ($#k7_scmpds_2 :::"<>0_goto"::: ) (Num 2) ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" ($#k3_scmpds_2 :::"goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) "I" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) "I" ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k3_scmpds_2 :::"goto"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) "I" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ")" )); end; :: deftheorem defines :::"while<>0"::: SCPINVAR:def 3 : (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k4_scpinvar :::"while<>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" "(" (Set (Var "a")) "," (Set (Var "i")) ")" ($#k7_scmpds_2 :::"<>0_goto"::: ) (Num 2) ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" ($#k3_scmpds_2 :::"goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "I")) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k3_scmpds_2 :::"goto"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ")" )))))); begin theorem :: SCPINVAR:8 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k4_scpinvar :::"while<>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3)))))) ; theorem :: SCPINVAR:9 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool "(" (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3))) "iff" (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k4_scpinvar :::"while<>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ))) ")" ))))) ; theorem :: SCPINVAR:10 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k4_scpinvar :::"while<>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ))) & (Bool (Num 1) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k4_scpinvar :::"while<>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ))) ")" )))) ; theorem :: SCPINVAR:11 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_scpinvar :::"while<>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "i")) ")" ($#k7_scmpds_2 :::"<>0_goto"::: ) (Num 2))) & (Bool (Set (Set "(" ($#k4_scpinvar :::"while<>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k3_scmpds_2 :::"goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ))) & (Bool (Set (Set "(" ($#k4_scpinvar :::"while<>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_scmpds_2 :::"goto"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ))) ")" )))) ; theorem :: SCPINVAR:12 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k4_scpinvar :::"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 ($#k4_scpinvar :::"while<>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" )))))) ; theorem :: SCPINVAR:13 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k4_scpinvar :::"while<>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) "," (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" ")" )))))))) ; theorem :: SCPINVAR:14 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k4_scpinvar :::"while<>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3)))))))) ; theorem :: SCPINVAR:15 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "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_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k4_scpinvar :::"while<>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))))))))) ; registrationlet "I" be ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "a" be ($#m1_subset_1 :::"Int_position":::); let "i" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k4_scpinvar :::"while<>0"::: ) "(" "a" "," "i" "," "I" ")" ) -> ($#v3_scmpds_4 :::"shiftable"::: ) ; end; registrationlet "I" be ($#v2_compos_1 :::"halt-free"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "a" be ($#m1_subset_1 :::"Int_position":::); let "i" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k4_scpinvar :::"while<>0"::: ) "(" "a" "," "i" "," "I" ")" ) -> ($#v2_compos_1 :::"halt-free"::: ) ; end; begin scheme :: SCPINVAR:sch 3 WhileNHalt{ F1( ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) )) -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F2() -> (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F3() -> ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F4() -> ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F5() -> ($#m1_subset_1 :::"Int_position":::), F6() -> ($#m1_hidden :::"Integer":::), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "(" (Bool (Set ($#k4_scpinvar :::"while<>0"::: ) "(" (Set F5 "(" ")" ) "," (Set F6 "(" ")" ) "," (Set F4 "(" ")" ) ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set F2 "(" ")" ) "," (Set F3 "(" ")" )) & (Bool (Set ($#k4_scpinvar :::"while<>0"::: ) "(" (Set F5 "(" ")" ) "," (Set F6 "(" ")" ) "," (Set F4 "(" ")" ) ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set F2 "(" ")" ) "," (Set F3 "(" ")" )) ")" ) provided (Bool "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool P1[(Set (Var "t"))]) & (Bool (Set F1 "(" (Set (Var "t")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ) ")" ) "," (Set F6 "(" ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) and (Bool P1[(Set F2 "(" ")" )]) and (Bool "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "Q")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool P1[(Set (Var "t"))]) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" )) ($#r1_hidden :::"="::: ) (Set (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ) ")" ) "," (Set F6 "(" ")" ) ")" ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set F4 "(" ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ))) & (Bool (Set F4 "(" ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set F4 "(" ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set F1 "(" (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set F4 "(" ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ")" ) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set F1 "(" (Set (Var "t")) ")" )) & (Bool P1[(Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set F4 "(" ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ))]) ")" ))) proof end; scheme :: SCPINVAR:sch 4 WhileNExec{ F1( ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) )) -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F2() -> (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F3() -> ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F4() -> ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F5() -> ($#m1_subset_1 :::"Int_position":::), F6() -> ($#m1_hidden :::"Integer":::), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k4_scpinvar :::"while<>0"::: ) "(" (Set F5 "(" ")" ) "," (Set F6 "(" ")" ) "," (Set F4 "(" ")" ) ")" ")" ) "," (Set F3 "(" ")" ) "," (Set F2 "(" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k4_scpinvar :::"while<>0"::: ) "(" (Set F5 "(" ")" ) "," (Set F6 "(" ")" ) "," (Set F4 "(" ")" ) ")" ")" ) "," (Set F3 "(" ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set F4 "(" ")" ) "," (Set F3 "(" ")" ) "," (Set F2 "(" ")" ) ")" ")" ) ")" ) ")" )) provided (Bool (Set (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ) ")" ) "," (Set F6 "(" ")" ) ")" ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) and (Bool "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool P1[(Set (Var "t"))]) & (Bool (Set F1 "(" (Set (Var "t")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ) ")" ) "," (Set F6 "(" ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) and (Bool P1[(Set F2 "(" ")" )]) and (Bool "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "Q")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool P1[(Set (Var "t"))]) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" )) ($#r1_hidden :::"="::: ) (Set (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ) ")" ) "," (Set F6 "(" ")" ) ")" ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set F4 "(" ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ))) & (Bool (Set F4 "(" ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set F4 "(" ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set F1 "(" (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set F4 "(" ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ")" ) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set F1 "(" (Set (Var "t")) ")" )) & (Bool P1[(Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set F4 "(" ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ))]) ")" ))) proof end; scheme :: SCPINVAR:sch 5 WhileNEnd{ F1( ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) )) -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F2() -> (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F3() -> ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F4() -> ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ), F5() -> ($#m1_subset_1 :::"Int_position":::), F6() -> ($#m1_hidden :::"Integer":::), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "(" (Bool (Set F1 "(" (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k4_scpinvar :::"while<>0"::: ) "(" (Set F5 "(" ")" ) "," (Set F6 "(" ")" ) "," (Set F4 "(" ")" ) ")" ")" ) "," (Set F3 "(" ")" ) "," (Set F2 "(" ")" ) ")" ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool P1[(Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k4_scpinvar :::"while<>0"::: ) "(" (Set F5 "(" ")" ) "," (Set F6 "(" ")" ) "," (Set F4 "(" ")" ) ")" ")" ) "," (Set F3 "(" ")" ) "," (Set F2 "(" ")" ) ")" ")" ))]) ")" ) provided (Bool "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool P1[(Set (Var "t"))])) "holds" (Bool "(" (Bool (Set F1 "(" (Set (Var "t")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ) ")" ) "," (Set F6 "(" ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) and (Bool P1[(Set F2 "(" ")" )]) and (Bool "for" (Set (Var "t")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "Q")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool P1[(Set (Var "t"))]) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" )) ($#r1_hidden :::"="::: ) (Set (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ) ")" ) "," (Set F6 "(" ")" ) ")" ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set F4 "(" ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set F5 "(" ")" ))) & (Bool (Set F4 "(" ")" ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set F4 "(" ")" ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "t")) "," (Set (Var "Q"))) & (Bool (Set F1 "(" (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set F4 "(" ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ")" ) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set F1 "(" (Set (Var "t")) ")" )) & (Bool P1[(Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set F4 "(" ")" ) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ))]) ")" ))) proof end; theorem :: SCPINVAR:16 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "," (Set (Var "d")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "I"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set (Var "d")) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (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 "b"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set (Var "d")) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))))) "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 (Var "d"))) & (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 (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_xxreal_0 :::">"::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))))) "implies" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ))) & (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))) ")" ) ")" & "(" (Bool (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))))) "implies" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ))) & (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))) ")" ) ")" & (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 (Var "d")) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ))) ")" )) ")" )) "holds" (Bool "(" (Bool (Set ($#k4_scpinvar :::"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 ($#k4_scpinvar :::"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_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k4_scpinvar :::"while<>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k4_scpinvar :::"while<>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ")" ) ")" )) ")" ")" )))))) ; begin definitionfunc :::"GCD-Algorithm"::: -> ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCPINVAR:def 4 (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 3) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 1) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k13_scmpds_2 :::"SubFrom"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) "," (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) ")" ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k4_scpinvar :::"while<>0"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) "," (Set "(" (Set "(" (Set "(" ($#k3_scmpds_6 :::"if>0"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) "," (Set "(" ($#k9_compos_1 :::"Load"::: ) (Set "(" ($#k13_scmpds_2 :::"SubFrom"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 1) "," (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) ")" ")" ) ")" ) "," (Set "(" ($#k9_compos_1 :::"Load"::: ) (Set "(" ($#k13_scmpds_2 :::"SubFrom"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) "," (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 1) ")" ")" ) ")" ) ")" ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 1) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k13_scmpds_2 :::"SubFrom"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) "," (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) ")" ")" ) ")" ) ")" ")" )); end; :: deftheorem defines :::"GCD-Algorithm"::: SCPINVAR:def 4 : (Bool (Set ($#k5_scpinvar :::"GCD-Algorithm"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) ($#k5_scmpds_2 :::":="::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k4_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 1) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k13_scmpds_2 :::"SubFrom"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) "," (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) ")" ")" ) ")" ) ($#k1_scmpds_4 :::"';'"::: ) (Set "(" ($#k4_scpinvar :::"while<>0"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) "," (Set "(" (Set "(" (Set "(" ($#k3_scmpds_6 :::"if>0"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) "," (Set "(" ($#k9_compos_1 :::"Load"::: ) (Set "(" ($#k13_scmpds_2 :::"SubFrom"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 1) "," (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) ")" ")" ) ")" ) "," (Set "(" ($#k9_compos_1 :::"Load"::: ) (Set "(" ($#k13_scmpds_2 :::"SubFrom"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) "," (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 1) ")" ")" ) ")" ) ")" ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 1) ")" ")" ) ")" ) ($#k3_scmpds_4 :::"';'"::: ) (Set "(" ($#k13_scmpds_2 :::"SubFrom"::: ) "(" (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 3) "," (Set ($#k2_scmp_gcd :::"GBP"::: ) ) "," (Num 2) ")" ")" ) ")" ) ")" ")" ))); theorem :: SCPINVAR:17 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "i")) "," (Set (Var "d")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set (Var "d")) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (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 "b"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set (Var "d")) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))))) "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 (Var "d"))) & (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 (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_xxreal_0 :::">"::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))))) "implies" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ))) & (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))) ")" ) ")" & "(" (Bool (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))))) "implies" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ))) & (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))) ")" ) ")" & (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 (Var "d")) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "Q")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ))) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k4_scpinvar :::"while<>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k3_int_2 :::"gcd"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ))) & (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k4_scpinvar :::"while<>0"::: ) "(" (Set (Var "a")) "," (Set (Var "i")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k3_int_2 :::"gcd"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ))) ")" )))))) ; theorem :: SCPINVAR:18 (Bool (Set ($#k5_card_1 :::"card"::: ) (Set ($#k5_scpinvar :::"GCD-Algorithm"::: ) )) ($#r1_hidden :::"="::: ) (Num 12)) ; theorem :: SCPINVAR:19 (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 "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "y")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set ($#k5_scpinvar :::"GCD-Algorithm"::: ) ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "y")))) & (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set ($#k5_scpinvar :::"GCD-Algorithm"::: ) ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmp_gcd :::"intpos"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "y")))) & (Bool (Set ($#k5_scpinvar :::"GCD-Algorithm"::: ) ) ($#r1_scmpds_6 :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k5_scpinvar :::"GCD-Algorithm"::: ) ) ($#r2_scmpds_6 :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" )))) ;