:: BINARI_4 semantic presentation begin theorem :: BINARI_4:1 (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "m")) ($#k24_binop_2 :::"*"::: ) (Num 2)) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "m")) ($#k23_binop_2 :::"+"::: ) (Num 1)))) ; theorem :: BINARI_4:2 (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set (Var "m"))) ($#r1_xxreal_0 :::">="::: ) (Set (Var "m")))) ; theorem :: BINARI_4:3 (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k5_euclid :::"0*"::: ) (Set (Var "m")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" ($#k5_euclid :::"0*"::: ) (Set (Var "m")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "m"))))) ; theorem :: BINARI_4:4 (Bool "for" (Set (Var "k")) "," (Set (Var "m")) "," (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "l"))) & (Bool (Set (Var "l")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Bool "not" (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Var "l"))))) "holds" (Bool "(" (Bool (Set (Set (Var "k")) ($#k23_binop_2 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "l"))) & (Bool (Set (Var "l")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) ")" )) ; theorem :: BINARI_4:5 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n"))))) "holds" (Bool (Set ($#k4_binarith :::"carry"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))))) ; theorem :: BINARI_4:6 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "x")) ($#k7_binarith :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))))) ; theorem :: BINARI_4:7 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n"))))) "holds" (Bool (Set ($#k3_binari_2 :::"Intval"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: BINARI_4:8 (Bool "for" (Set (Var "l")) "," (Set (Var "m")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "l")) ($#k23_binop_2 :::"+"::: ) (Set (Var "m"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "k")) ($#k21_binop_2 :::"-"::: ) (Num 1)))) "holds" (Bool "(" (Bool (Set (Var "l")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k"))) ")" )) ; theorem :: BINARI_4:9 (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "h")) ($#k20_binop_2 :::"+"::: ) (Set (Var "i")))) & (Bool (Set (Var "h")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "h"))) & (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) ")" )) ; theorem :: BINARI_4:10 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "l")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "l")) ($#k23_binop_2 :::"+"::: ) (Set (Var "m"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set (Var "n")) ")" ) ($#k21_binop_2 :::"-"::: ) (Num 1)))) "holds" (Bool (Set ($#k8_binarith :::"add_ovfl"::: ) "(" (Set "(" (Set (Var "n")) ($#k1_binari_3 :::"-BinarySequence"::: ) (Set (Var "l")) ")" ) "," (Set "(" (Set (Var "n")) ($#k1_binari_3 :::"-BinarySequence"::: ) (Set (Var "m")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )))) ; theorem :: BINARI_4:11 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "l")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "l")) ($#k23_binop_2 :::"+"::: ) (Set (Var "m"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set (Var "n")) ")" ) ($#k21_binop_2 :::"-"::: ) (Num 1)))) "holds" (Bool (Set ($#k6_binarith :::"Absval"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k1_binari_3 :::"-BinarySequence"::: ) (Set (Var "l")) ")" ) ($#k7_binarith :::"+"::: ) (Set "(" (Set (Var "n")) ($#k1_binari_3 :::"-BinarySequence"::: ) (Set (Var "m")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "l")) ($#k23_binop_2 :::"+"::: ) (Set (Var "m")))))) ; theorem :: BINARI_4:12 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Set (Var "z")) ($#k7_partfun1 :::"/."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) "holds" (Bool (Set ($#k6_binarith :::"Absval"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::">="::: ) (Set (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ))))) ; theorem :: BINARI_4:13 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "l")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "l")) ($#k23_binop_2 :::"+"::: ) (Set (Var "m"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k21_binop_2 :::"-"::: ) (Num 1)))) "holds" (Bool (Set (Set "(" ($#k4_binarith :::"carry"::: ) "(" (Set "(" (Set (Var "n")) ($#k1_binari_3 :::"-BinarySequence"::: ) (Set (Var "l")) ")" ) "," (Set "(" (Set (Var "n")) ($#k1_binari_3 :::"-BinarySequence"::: ) (Set (Var "m")) ")" ) ")" ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )))) ; theorem :: BINARI_4:14 (Bool "for" (Set (Var "l")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "l")) ($#k23_binop_2 :::"+"::: ) (Set (Var "m"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k21_binop_2 :::"-"::: ) (Num 1)))) "holds" (Bool (Set ($#k3_binari_2 :::"Intval"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k1_binari_3 :::"-BinarySequence"::: ) (Set (Var "l")) ")" ) ($#k7_binarith :::"+"::: ) (Set "(" (Set (Var "n")) ($#k1_binari_3 :::"-BinarySequence"::: ) (Set (Var "m")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "l")) ($#k23_binop_2 :::"+"::: ) (Set (Var "m")))))) ; theorem :: BINARI_4:15 (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Num 1) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set ($#k3_binari_2 :::"Intval"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k19_binop_2 :::"-"::: ) (Num 1)))) ; theorem :: BINARI_4:16 (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Num 1) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set ($#k3_binari_2 :::"Intval"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: BINARI_4:17 (Bool "for" (Set (Var "x")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set ($#k8_margrel1 :::"TRUE"::: ) ) ($#k5_xboolean :::"'or'"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) ; theorem :: BINARI_4:18 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k21_binop_2 :::"-"::: ) (Num 1))) & (Bool (Set ($#k19_binop_2 :::"-"::: ) (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: BINARI_4:19 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "n")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n"))))) "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_binarith :::"are_summable"::: ) ))) ; theorem :: BINARI_4:20 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set "(" (Set (Var "i")) ($#k22_binop_2 :::"*"::: ) (Set (Var "n")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; begin definitionlet "m", "j" be ($#m1_hidden :::"Nat":::); func :::"MajP"::: "(" "m" "," "j" ")" -> ($#m1_hidden :::"Nat":::) means :: BINARI_4:def 1 (Bool "(" (Bool (Set (Num 2) ($#k5_series_1 :::"to_power"::: ) it) ($#r1_xxreal_0 :::">="::: ) "j") & (Bool it ($#r1_xxreal_0 :::">="::: ) "m") & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::">="::: ) "j") & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">="::: ) "m")) "holds" (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">="::: ) it) ")" ) ")" ); end; :: deftheorem defines :::"MajP"::: BINARI_4:def 1 : (Bool "for" (Set (Var "m")) "," (Set (Var "j")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_binari_4 :::"MajP"::: ) "(" (Set (Var "m")) "," (Set (Var "j")) ")" )) "iff" (Bool "(" (Bool (Set (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set (Var "b3"))) ($#r1_xxreal_0 :::">="::: ) (Set (Var "j"))) & (Bool (Set (Var "b3")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "m"))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::">="::: ) (Set (Var "j"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "m")))) "holds" (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "b3"))) ")" ) ")" ) ")" )); theorem :: BINARI_4:21 (Bool "for" (Set (Var "j")) "," (Set (Var "k")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "k")))) "holds" (Bool (Set ($#k1_binari_4 :::"MajP"::: ) "(" (Set (Var "m")) "," (Set (Var "j")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k1_binari_4 :::"MajP"::: ) "(" (Set (Var "m")) "," (Set (Var "k")) ")" ))) ; theorem :: BINARI_4:22 (Bool "for" (Set (Var "l")) "," (Set (Var "m")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "l")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k1_binari_4 :::"MajP"::: ) "(" (Set (Var "l")) "," (Set (Var "j")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k1_binari_4 :::"MajP"::: ) "(" (Set (Var "m")) "," (Set (Var "j")) ")" ))) ; theorem :: BINARI_4:23 (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set ($#k1_binari_4 :::"MajP"::: ) "(" (Set (Var "m")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "m")))) ; theorem :: BINARI_4:24 (Bool "for" (Set (Var "j")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set (Var "m"))))) "holds" (Bool (Set ($#k1_binari_4 :::"MajP"::: ) "(" (Set (Var "m")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "m")))) ; theorem :: BINARI_4:25 (Bool "for" (Set (Var "j")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::">"::: ) (Set (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set (Var "m"))))) "holds" (Bool (Set ($#k1_binari_4 :::"MajP"::: ) "(" (Set (Var "m")) "," (Set (Var "j")) ")" ) ($#r1_xxreal_0 :::">"::: ) (Set (Var "m")))) ; begin definitionlet "m" be ($#m1_hidden :::"Nat":::); let "i" be ($#m1_hidden :::"Integer":::); func :::"2sComplement"::: "(" "m" "," "i" ")" -> ($#m2_finseq_1 :::"Tuple":::) "of" "m" "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) equals :: BINARI_4:def 2 (Set "m" ($#k1_binari_3 :::"-BinarySequence"::: ) (Set "(" ($#k1_int_2 :::"abs"::: ) (Set "(" (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set "(" ($#k1_binari_4 :::"MajP"::: ) "(" "m" "," (Set "(" ($#k1_int_2 :::"abs"::: ) "i" ")" ) ")" ")" ) ")" ) ($#k20_binop_2 :::"+"::: ) "i" ")" ) ")" )) if (Bool "i" ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) otherwise (Set "m" ($#k1_binari_3 :::"-BinarySequence"::: ) (Set "(" ($#k1_int_2 :::"abs"::: ) "i" ")" )); end; :: deftheorem defines :::"2sComplement"::: BINARI_4:def 2 : (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k2_binari_4 :::"2sComplement"::: ) "(" (Set (Var "m")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k1_binari_3 :::"-BinarySequence"::: ) (Set "(" ($#k1_int_2 :::"abs"::: ) (Set "(" (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set "(" ($#k1_binari_4 :::"MajP"::: ) "(" (Set (Var "m")) "," (Set "(" ($#k1_int_2 :::"abs"::: ) (Set (Var "i")) ")" ) ")" ")" ) ")" ) ($#k20_binop_2 :::"+"::: ) (Set (Var "i")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )))) "implies" (Bool (Set ($#k2_binari_4 :::"2sComplement"::: ) "(" (Set (Var "m")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k1_binari_3 :::"-BinarySequence"::: ) (Set "(" ($#k1_int_2 :::"abs"::: ) (Set (Var "i")) ")" ))) ")" ")" ))); theorem :: BINARI_4:26 (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k2_binari_4 :::"2sComplement"::: ) "(" (Set (Var "m")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "m"))))) ; theorem :: BINARI_4:27 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k21_binop_2 :::"-"::: ) (Num 1))) & (Bool (Set ($#k19_binop_2 :::"-"::: ) (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i")))) "holds" (Bool (Set ($#k3_binari_2 :::"Intval"::: ) (Set "(" ($#k2_binari_4 :::"2sComplement"::: ) "(" (Set (Var "n")) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "i"))))) ; theorem :: BINARI_4:28 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "h")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool "(" (Bool "(" (Bool (Set (Var "h")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) "or" (Bool "(" (Bool (Set (Var "h")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ) & (Bool (Set (Set (Var "h")) ($#k6_int_1 :::"mod"::: ) (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k6_int_1 :::"mod"::: ) (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set ($#k2_binari_4 :::"2sComplement"::: ) "(" (Set (Var "n")) "," (Set (Var "h")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_binari_4 :::"2sComplement"::: ) "(" (Set (Var "n")) "," (Set (Var "i")) ")" )))) ; theorem :: BINARI_4:29 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "h")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool "(" (Bool "(" (Bool (Set (Var "h")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) "or" (Bool "(" (Bool (Set (Var "h")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ) & (Bool (Set (Var "h")) "," (Set (Var "i")) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set (Var "n"))))) "holds" (Bool (Set ($#k2_binari_4 :::"2sComplement"::: ) "(" (Set (Var "n")) "," (Set (Var "h")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_binari_4 :::"2sComplement"::: ) "(" (Set (Var "n")) "," (Set (Var "i")) ")" )))) ; theorem :: BINARI_4:30 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "l")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "l")) ($#k4_nat_d :::"mod"::: ) (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k4_nat_d :::"mod"::: ) (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set (Set (Var "n")) ($#k1_binari_3 :::"-BinarySequence"::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_binari_3 :::"-BinarySequence"::: ) (Set (Var "m")))))) ; theorem :: BINARI_4:31 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "l")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "l")) "," (Set (Var "m")) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "n")) ($#k1_binari_3 :::"-BinarySequence"::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_binari_3 :::"-BinarySequence"::: ) (Set (Var "m")))))) ; theorem :: BINARI_4:32 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set "(" ($#k2_binari_4 :::"2sComplement"::: ) "(" (Set "(" (Set (Var "n")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "i")) ")" ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_binari_4 :::"2sComplement"::: ) "(" (Set (Var "n")) "," (Set (Var "i")) ")" ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "j"))))))) ; theorem :: BINARI_4:33 (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Set ($#k2_binari_4 :::"2sComplement"::: ) "(" (Set "(" (Set (Var "m")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_binari_4 :::"2sComplement"::: ) "(" (Set (Var "m")) "," (Set (Var "i")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) )))))) ; theorem :: BINARI_4:34 (Bool "for" (Set (Var "m")) "," (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Set (Set "(" (Set (Var "m")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ($#k1_binari_3 :::"-BinarySequence"::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "m")) ($#k1_binari_3 :::"-BinarySequence"::: ) (Set (Var "l")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ))))) ; theorem :: BINARI_4:35 (Bool "for" (Set (Var "h")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k19_binop_2 :::"-"::: ) (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set (Var "n")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "h")) ($#k20_binop_2 :::"+"::: ) (Set (Var "i")))) & (Bool (Set (Var "h")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k19_binop_2 :::"-"::: ) (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "h"))) & (Bool (Set ($#k19_binop_2 :::"-"::: ) (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i")))) "holds" (Bool (Set (Set "(" ($#k4_binarith :::"carry"::: ) "(" (Set "(" ($#k2_binari_4 :::"2sComplement"::: ) "(" (Set "(" (Set (Var "n")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "h")) ")" ")" ) "," (Set "(" ($#k2_binari_4 :::"2sComplement"::: ) "(" (Set "(" (Set (Var "n")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "i")) ")" ")" ) ")" ")" ) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "n")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )))) ; theorem :: BINARI_4:36 (Bool "for" (Set (Var "h")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "h")) ($#k20_binop_2 :::"+"::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k21_binop_2 :::"-"::: ) (Num 1))) & (Bool (Set (Var "h")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k3_binari_2 :::"Intval"::: ) (Set "(" (Set "(" ($#k2_binari_4 :::"2sComplement"::: ) "(" (Set (Var "n")) "," (Set (Var "h")) ")" ")" ) ($#k7_binarith :::"+"::: ) (Set "(" ($#k2_binari_4 :::"2sComplement"::: ) "(" (Set (Var "n")) "," (Set (Var "i")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k20_binop_2 :::"+"::: ) (Set (Var "i")))))) ; theorem :: BINARI_4:37 (Bool "for" (Set (Var "h")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k19_binop_2 :::"-"::: ) (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "h")) ($#k20_binop_2 :::"+"::: ) (Set (Var "i")))) & (Bool (Set (Var "h")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k19_binop_2 :::"-"::: ) (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "h"))) & (Bool (Set ($#k19_binop_2 :::"-"::: ) (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i")))) "holds" (Bool (Set ($#k3_binari_2 :::"Intval"::: ) (Set "(" (Set "(" ($#k2_binari_4 :::"2sComplement"::: ) "(" (Set "(" (Set (Var "n")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k7_binarith :::"+"::: ) (Set "(" ($#k2_binari_4 :::"2sComplement"::: ) "(" (Set "(" (Set (Var "n")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "i")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k20_binop_2 :::"+"::: ) (Set (Var "i")))))) ; theorem :: BINARI_4:38 (Bool "for" (Set (Var "h")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k19_binop_2 :::"-"::: ) (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "h"))) & (Bool (Set (Var "h")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k21_binop_2 :::"-"::: ) (Num 1))) & (Bool (Set ($#k19_binop_2 :::"-"::: ) (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k21_binop_2 :::"-"::: ) (Num 1))) & (Bool (Set ($#k19_binop_2 :::"-"::: ) (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "h")) ($#k20_binop_2 :::"+"::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "h")) ($#k20_binop_2 :::"+"::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k21_binop_2 :::"-"::: ) (Num 1))) & (Bool "(" (Bool "(" (Bool (Set (Var "h")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) "or" (Bool "(" (Bool (Set (Var "h")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )) "holds" (Bool (Set ($#k3_binari_2 :::"Intval"::: ) (Set "(" (Set "(" ($#k2_binari_4 :::"2sComplement"::: ) "(" (Set (Var "n")) "," (Set (Var "h")) ")" ")" ) ($#k7_binarith :::"+"::: ) (Set "(" ($#k2_binari_4 :::"2sComplement"::: ) "(" (Set (Var "n")) "," (Set (Var "i")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k20_binop_2 :::"+"::: ) (Set (Var "i")))))) ;