(def-language mach-arith-language (embedded-language h-o-real-arithmetic) (constants (maxint zz) (minint zz)))

(def-theory machine-arithmetic (language mach-arith-language) (component-theories h-o-real-arithmetic) (axioms (maxint-is-positive"0 < maxint") (minint-is-negative-maxint"minint = -maxint")))

(def-theorem minint-is-negative"minint < 0"(theory machine-arithmetic) (proof ( (apply-macete-with-minor-premises minint-is-negative-maxint) simplify )))

(def-atomic-sort int"lambda(i:zz, minint <= i and i <= maxint)"(theory machine-arithmetic) (witness"0"))

(def-constant =_ma"lambda(x,y:int, x=y)"(theory machine-arithmetic))

(def-constant <_ma"lambda(x,y:int, x<y)"(theory machine-arithmetic))

(def-constant <=_ma"lambda(x,y:int, x<=y)"(theory machine-arithmetic))

(def-constant >_ma"lambda(x,y:int, x>y)"(theory machine-arithmetic))

(def-constant >=_ma"lambda(x,y:int, x>=y)"(theory machine-arithmetic))

(def-script closed-on-int-2 0 ( sort-definedness direct-inference (case-split ("#(xx_0,int) and #(xx_1,int)")) simplify (simplify-antecedent"with(p:prop,p);") ))

(def-script unfold-ma-defined-expression 1 ( direct-inference (unfold-single-defined-constant-globally $1) (case-split ("#(x,int) and #(y,int)")) simplify (simplify-antecedent"with(p:prop,p);") ))

(def-theorem ()"#(lambda(x,y:int,if(#(x+y,int), x+y, ?int)),[int,int,int])"lemma (theory machine-arithmetic) (proof ( closed-on-int-2 )))

(def-constant +_ma"lambda(x,y:int, if(#(x+y,int),x+y,?int))"(sort"[int,int,int]") (theory machine-arithmetic))

(def-theorem unfold-defined-expression%+_ma"forall(x,y:zz, #(x +_ma y) implies x +_ma y = x + y)"(theory machine-arithmetic) (proof ( (unfold-ma-defined-expression +_ma) )))

(def-theorem ()"#(lambda(x,y:int,if(#(x*y,int), x*y, ?int)),[int,int,int])"lemma (theory machine-arithmetic) (proof ( closed-on-int-2 )))

(def-constant *_ma"lambda(x,y:int, if(#(x*y,int),x*y,?int))"(sort"[int,int,int]") (theory machine-arithmetic))

(def-theorem unfold-defined-expression%*_ma"forall(x,y:zz, #(x *_ma y) implies x *_ma y = x * y)"(theory machine-arithmetic) (proof ( (unfold-ma-defined-expression *_ma) )))

(def-theorem ()"#(lambda(x,y:int,if(#(x-y,int), x-y, ?int)),[int,int,int])"lemma (theory machine-arithmetic) (proof ( closed-on-int-2 )))

(def-constant sub_ma"lambda(x,y:int,if(#(x-y,int), x-y, ?int))"(sort"[int,int,int]") (theory machine-arithmetic))

(def-theorem unfold-defined-expression%sub_ma"forall(x,y:zz, #(x sub_ma y) implies x sub_ma y = x - y)"(theory machine-arithmetic) (proof ( (unfold-ma-defined-expression sub_ma) )))

(def-theorem unary-int-function-lemma"forall(f:[rr,rr], forall(x:zz, abs(f(x)) <= abs(x) and (#(f(x)) implies #(f(x),zz))) implies #(lambda(x:int, f(x)),[int,int]))"lemma (theory machine-arithmetic) (proof ( direct-and-antecedent-inference-strategy sort-definedness direct-inference (case-split ("#(xx_0,int)")) (block (script-comment"node added by `case-split' at (1)") simplify (cut-with-single-formula"#(xx_0,int) and 0=0") (incorporate-antecedent"with(xx_0:ind,#(xx_0,int));") (apply-macete-with-minor-premises int-defining-axiom_machine-arithmetic) (apply-macete-with-minor-premises minint-is-negative-maxint) (instantiate-universal-antecedent"with(p:prop,forall(x:zz,p));"("xx_0")) (incorporate-antecedent"with(r:rr,r<=r);") (unfold-single-defined-constant-globally abs) (case-split-on-conditionals (1)) (case-split-on-conditionals (0)) (case-split-on-conditionals (0))) simplify )))

(def-theorem binary-int-function-lemma"forall(f:[rr,rr,rr], forall(x,y:zz, abs(f(x,y)) <= abs(x) and (#(f(x,y)) implies #(f(x,y),zz))) implies #(lambda(x,y:int, f(x,y)),[int,int,int]))"lemma (theory machine-arithmetic) (proof ( direct-and-antecedent-inference-strategy sort-definedness direct-inference (case-split ("#(xx_0,int) and #(xx_1,int)")) (block (script-comment"node added by `case-split' at (1)") simplify (cut-with-single-formula"#(xx_0,int) and #(xx_1,int) and 0=0") (incorporate-antecedent"with(p:prop,p and p);") (apply-macete-with-minor-premises int-defining-axiom_machine-arithmetic) (apply-macete-with-minor-premises minint-is-negative-maxint) (instantiate-universal-antecedent"with(p:prop,forall(x,y:zz,p));"("xx_0""xx_1")) (incorporate-antecedent"with(r:rr,r<=r);") (unfold-single-defined-constant-globally abs) (case-split-on-conditionals (1)) (case-split-on-conditionals (0)) (case-split-on-conditionals (0))) (block (script-comment"node added by `case-split' at (2)") simplify (simplify-antecedent"with(p:prop,not(p));")) )))

(def-theorem int-minus-lemma"forall(x:int, #(-x,int))"(theory machine-arithmetic) (proof ( direct-and-antecedent-inference-strategy (cut-with-single-formula"#(x,int)") (incorporate-antecedent"with(p:prop,p);") (apply-macete-with-minor-premises int-defining-axiom_machine-arithmetic) (apply-macete-with-minor-premises minint-is-negative-maxint) simplify )))

(def-theorem ()"#(lambda(x:int, -x),[int,int])"lemma (theory machine-arithmetic) (proof ( (apply-macete-with-minor-premises unary-int-function-lemma) simplify (unfold-single-defined-constant-globally abs) (raise-conditional (0)) (raise-conditional (0)) (raise-conditional (0)) simplify )))

(def-constant -_ma"lambda(x:int, -x)"(sort"[int,int]") (theory machine-arithmetic))

(def-theorem ()"#(lambda(x:int, abs(x)),[int,int])"lemma (theory machine-arithmetic) (proof ( (apply-macete-with-minor-premises unary-int-function-lemma) simplify (unfold-single-defined-constant-globally abs) simplify )))

(def-constant abs_ma"lambda(x:int, abs(x))"(sort"[int,int]") (theory machine-arithmetic))

(def-theorem maxint-division-lemma"forall(a:int,b:zz, not(b=0) implies a/b<=maxint)"(theory machine-arithmetic) (proof ( (cut-with-single-formula"forall(a:int,b:zz,0<b implies a/b<=maxint)") (block (script-comment"`cut-with-single-formula' at (0)") direct-and-antecedent-inference-strategy (case-split ("0<b")) simplify (block (script-comment"`case-split' at (2)") (force-substitution"a/b""(-a)/(-b)"(0)) (block (script-comment"`force-substitution' at (0)") (backchain"with(p:prop,forall(a:int,b:zz,p));") simplify (block (script-comment"`backchain' at (1)") (cut-with-single-formula"#(a,int)") (incorporate-antecedent"with(a:int,#(a,int));") (apply-macete-with-minor-premises int-defining-axiom_machine-arithmetic) (apply-macete-with-minor-premises minint-is-negative-maxint) simplify)) simplify)) (block (script-comment"`cut-with-single-formula' at (1)") direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises fractional-expression-manipulation) (cut-with-single-formula"maxint<=maxint*b") (move-to-sibling 1) (block (script-comment"`cut-with-single-formula' at (1)") (cut-with-single-formula"0<=maxint*(b-1)") simplify simplify) (block (script-comment"`cut-with-single-formula' at (0)") (cut-with-single-formula"a<=maxint") simplify (block (script-comment"`cut-with-single-formula' at (1)") (cut-with-single-formula"minint <= a and a <= maxint") (apply-macete-with-minor-premises int-in-quasi-sort_machine-arithmetic)))) )))

(def-theorem minint-division-lemma"forall(a:int,b:zz, not(b=0) implies minint<=a/b)"(theory machine-arithmetic) (proof ( direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises minint-is-negative-maxint) (cut-with-single-formula"(-a)/b<=maxint") simplify (block (script-comment"node added by `cut-with-single-formula' at (1)") (apply-macete-with-minor-premises maxint-division-lemma) (cut-with-single-formula"#(a,int)") (incorporate-antecedent"with(a:int,#(a,int));") (apply-macete-with-minor-premises int-defining-axiom_machine-arithmetic) (apply-macete-with-minor-premises minint-is-negative-maxint) simplify) )))

(def-theorem int-division-lemma"forall(a:int,b:zz, not(b=0) implies #(a div b,int))"(theory machine-arithmetic) (proof ( direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises int-defining-axiom_machine-arithmetic) beta-reduce-repeatedly (unfold-single-defined-constant-globally div) (apply-macete-with-minor-premises floor-not-much-below-arg) direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises minint-division-lemma) (block (script-comment"`direct-and-antecedent-inference-strategy' at (1)") (cut-with-single-formula"floor(a/b)<=a/b and a/b<=maxint") simplify (block (script-comment"`cut-with-single-formula' at (1)") (apply-macete-with-minor-premises floor-below-arg) (apply-macete-with-minor-premises maxint-division-lemma))) )))

(def-theorem ()"#(lambda(x,y:int, x div y),[int,int,int])"lemma (theory machine-arithmetic) (proof ( sort-definedness direct-inference (case-split ("#(xx_0,int) and #(xx_1,int) and not xx_1 =0 ")) (block (script-comment"`case-split' at (1)") beta-reduce-repeatedly (apply-macete-with-minor-premises int-division-lemma) direct-and-antecedent-inference-strategy) (block (script-comment"`case-split' at (2)") beta-reduce-repeatedly (contrapose"with(p:prop,p);") direct-and-antecedent-inference-strategy (antecedent-inference"with(p:prop,p and p);") (contrapose"with(z:zz,#(z));") beta-reduce-repeatedly (unfold-single-defined-constant (0) div) simplify) )))

(def-constant div_ma"lambda(x,y:int, x div y)"(sort"[int,int,int]") (theory machine-arithmetic))

(def-theorem maxint-pos-mod-lemma"forall(a:zz,b:int, 0< b implies a mod b < maxint)"(theory machine-arithmetic) (proof ( direct-and-antecedent-inference-strategy (cut-with-single-formula" a mod b < b and b<=maxint") simplify (block (script-comment"`cut-with-single-formula' at (1)") (cut-with-single-formula"#(b,int)") (incorporate-antecedent"with(b:int,#(b,int));") (apply-macete-with-minor-premises int-defining-axiom_machine-arithmetic) beta-reduce-repeatedly direct-and-antecedent-inference-strategy (instantiate-theorem division-with-remainder ("b""a"))) )))

(def-theorem minint-pos-mod-lemma"forall(a:zz, b:int, 0< b implies minint < a mod b )"(theory machine-arithmetic) (proof ( direct-and-antecedent-inference-strategy (cut-with-single-formula"0<= a mod b") simplify (instantiate-theorem division-with-remainder ("b""a")) )))

(def-theorem int-mod-lemma"forall(a:zz, b:int, not(b=0) implies #(a mod b,int))"(theory machine-arithmetic) (proof ( (cut-with-single-formula"forall(a:zz,b:int,0<b implies #(a mod b,int))") (block (script-comment"`cut-with-single-formula' at (0)") direct-and-antecedent-inference-strategy (case-split ("0<b")) simplify (block (script-comment"`case-split' at (2)") (force-substitution"a mod b""-(- a mod -b)"(0)) (block (script-comment"`force-substitution' at (0)") (apply-macete-with-minor-premises int-minus-lemma) (backchain"with(p:prop,forall(a:zz,b:int,p));") simplify (block (script-comment"`backchain' at (1)") (cut-with-single-formula"#(-b, int)") (simplify-antecedent"with(r:rr,#(r,int));") (apply-macete-with-minor-premises int-minus-lemma))) (block (script-comment"`force-substitution' at (1)") (apply-macete-with-minor-premises mod-of-negative) simplify))) (block (script-comment"`cut-with-single-formula' at (1)") direct-and-antecedent-inference-strategy (cut-with-single-formula"#(a mod b ,zz)") (block (script-comment"`cut-with-single-formula' at (0)") (apply-macete-with-minor-premises int-defining-axiom_machine-arithmetic) beta-reduce-repeatedly simplify (cut-with-single-formula"minint<a mod b and a mod b<maxint") simplify (block (script-comment"`cut-with-single-formula' at (1)") (apply-macete-with-minor-premises minint-pos-mod-lemma) (apply-macete-with-minor-premises maxint-pos-mod-lemma))) (block (script-comment"`cut-with-single-formula' at (1)") (apply-macete-with-minor-premises mod-of-integer-is-integer) simplify)) )))

(def-theorem ()"#(lambda(x,y:int, x mod y),[int,int,int])"lemma (theory machine-arithmetic) (proof ( sort-definedness direct-inference (case-split ("#(xx_0,int) and #(xx_1,int) and not xx_1 =0 ")) (block (script-comment"node added by `case-split' at (1)") beta-reduce-repeatedly (apply-macete-with-minor-premises int-mod-lemma) direct-and-antecedent-inference-strategy) (block (script-comment"node added by `case-split' at (2)") beta-reduce-repeatedly (contrapose"with(p:prop,p);") direct-and-antecedent-inference-strategy (antecedent-inference"with(p:prop,p and p);") (contrapose"with(r:rr,#(r));") beta-reduce-repeatedly (unfold-single-defined-constant (0) mod) simplify) )))

(def-constant mod_ma"lambda(x,y:int, x mod y)"(sort"[int,int,int]") (theory machine-arithmetic))