```
"forall(x:zz_mod, x<modulus-1 implies +_mod(x,1)=x+1)"
(theory arithmetic-mod-n)
(proof
(
(unfold-single-defined-constant (0) +_mod)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises mod-characterization)
simplify
(cut-with-single-formula "#(x,zz_mod)")
(incorporate-antecedent "with(x:zz_mod,#(x,zz_mod));")
(apply-macete-with-minor-premises zz_mod-defining-axiom_arithmetic-mod-n)
(unfold-single-defined-constant (0) divides)
simplify
)))
```

```
"forall(x:zz_mod, +_mod(modulus-1,1)=0)"
(theory arithmetic-mod-n)
(proof
(

(unfold-single-defined-constant (0) +_mod)
simplify
(apply-macete-with-minor-premises mod-characterization)
(unfold-single-defined-constant (0) divides)
simplify
)))
```

```(def-theorem ()
"#(-_mod(1))"
(theory arithmetic-mod-n)
lemma
(proof
(
(apply-macete-with-minor-premises -_mod-computation-non-zero)
)))
```

```
(def-constant neg_1
"-_mod(1)"
(theory arithmetic-mod-n))
```

```
"forall(x:zz_mod, not(x=0) implies +_mod(x,neg_1)=x-1)"
(theory arithmetic-mod-n)
(proof
(
(unfold-single-defined-constant (0) neg_1)
(apply-macete-with-minor-premises -_mod-computation-non-zero)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises +_mod-characterization)
(move-to-sibling 1)
(block
(script-comment "`apply-macete-with-minor-premises' at (1)")
(apply-macete-with-minor-premises zz_mod-defining-axiom_arithmetic-mod-n)
(cut-with-single-formula "#(x,zz_mod)")
(incorporate-antecedent "with(x:zz_mod,#(x,zz_mod));")
(apply-macete-with-minor-premises zz_mod-defining-axiom_arithmetic-mod-n)
simplify)
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0)")
(cut-with-single-formula "#(x,zz_mod)")
(incorporate-antecedent "with(x:zz_mod,#(x,zz_mod));")
(apply-macete-with-minor-premises zz_mod-defining-axiom_arithmetic-mod-n)
simplify)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1)")
(weaken (0))
simplify
(cut-with-single-formula "#(x,zz_mod)")
(incorporate-antecedent "with(x:zz_mod,#(x,zz_mod));")
(apply-macete-with-minor-premises zz_mod-defining-axiom_arithmetic-mod-n)
simplify)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (2)")
(unfold-single-defined-constant (0) congruent)
simplify
(apply-macete-with-minor-premises multiplication-preserves-divisibility)
(apply-macete-with-minor-premises self-divisibility)
simplify))
)))
```

```
"forall(x:zz_mod, +_mod(0,neg_1)=modulus-1)"
(theory arithmetic-mod-n)
(proof
(
(unfold-single-defined-constant (0) neg_1)
(apply-macete-with-minor-premises -_mod-computation-non-zero)
(apply-macete-with-minor-premises +_mod-characterization)
(unfold-single-defined-constant (0) congruent)
(unfold-single-defined-constant (0) divides)
simplify
)))

```

```
(def-theory arithmetic-mod-5
(component-theories arithmetic-mod-n)
(axioms
(modular-value "modulus=5")))
```

```
(def-theorem example-op
"+_mod(2,3)=0"
(theory arithmetic-mod-5)
(proof
(
(unfold-single-defined-constant (0) +_mod)
(unfold-single-defined-constant (0) mod)
(apply-macete-with-minor-premises modular-value)
beta-reduce-with-minor-premises
simplify
(block
(script-comment "node added by `beta-reduce-with-minor-premises' at (1)")
(apply-macete-with-minor-premises zz_mod-defining-axiom_arithmetic-mod-n)
(apply-macete-with-minor-premises modular-value)
simplify)
(block
(script-comment "node added by `beta-reduce-with-minor-premises' at (2)")
(apply-macete-with-minor-premises zz_mod-defining-axiom_arithmetic-mod-n)
(apply-macete-with-minor-premises modular-value)
simplify)
)))
```

```(def-script mod-plus-compute 0

(
(unfold-single-defined-constant (0) +_mod)
(unfold-single-defined-constant (0) mod)
(apply-macete-with-minor-premises modular-value)
beta-reduce-with-minor-premises
simplify
(block
(script-comment "node added by `beta-reduce-with-minor-premises' at (1)")
(apply-macete-with-minor-premises zz_mod-defining-axiom_arithmetic-mod-n)
(apply-macete-with-minor-premises modular-value)
simplify)
(block
(script-comment "node added by `beta-reduce-with-minor-premises' at (2)")
(apply-macete-with-minor-premises zz_mod-defining-axiom_arithmetic-mod-n)
(apply-macete-with-minor-premises modular-value)
simplify)
))
```

```
(def-theorem example-op-1
"+_mod(2,4)=1"
(theory arithmetic-mod-5)
(proof
(
mod-plus-compute
)))
```