(def-theorem add-one-typical-case"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 )))

(def-theorem add-one-special-case"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))

(def-theorem add-neg_1-typical-case"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)) )))

(def-theorem add-neg_1-0"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 )))