```(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))
```