```(def-language monoid-language
(embedded-languages h-o-real-arithmetic)
(base-types uu)
(constants
(e uu)
(** (uu uu uu))))
```

```
(def-theory monoid-theory
(component-theories h-o-real-arithmetic)
(language monoid-language)
(axioms
(associative-law-for-multiplication-for-monoids
"forall(z,y,x:uu, x**(y**z)=(x**y)**z)" rewrite)
(right-multiplicative-identity-for-monoids
"forall(x:uu,x**e=x)" rewrite)
(left-multiplicative-identity-for-monoids
"forall(x:uu,e**x=x)" rewrite)
("total_q(**,[uu,uu,uu])" d-r-convergence)))

```

```
(def-recursive-constant monoid%prod
"lambda(pi:[zz,zz,[zz,uu],uu],lambda(m,n:zz,f:[zz,uu],
if(m<=n,pi(m,n-1,f) ** f(n),e)))"
(theory monoid-theory))
```

```
(def-theorem monoid-prod-out
"forall(f:[zz,uu],m,n:zz,n<=m implies
monoid%prod(n,m,f)==monoid%prod(n,m-1,f)**f(m))"
(theory monoid-theory)
(proof
(

(induction integer-inductor ())
)
)
(usages transportable-macete))
```

```
(def-theorem monoid-triv-prod
"forall(f:[zz,uu],n,m:zz,m=n implies monoid%prod(n,m,f)==f(n))"
(theory monoid-theory)
(proof
(
direct-and-antecedent-inference-strategy
(unfold-single-defined-constant (0) monoid%prod)
(unfold-single-defined-constant (0) monoid%prod)
simplify
)
)
(usages transportable-macete))
```

```
(def-theorem monoid-null-prod
"forall(f:[zz,uu],n,m:zz,m<n implies monoid%prod(n,m,f)=e)"
(theory monoid-theory)
(proof
(
(unfold-single-defined-constant (0) monoid%prod)
simplify
)
)
(usages transportable-macete))
```

```
(def-theorem locality-for-monoid-prod
"forall(f,g:[zz,uu],p,m:zz,forall(x:zz,
p<=x and x<=m implies f(x)==g(x)) implies monoid%prod(p,m,f)==monoid%prod(p,m,g))"
(theory monoid-theory)
(usages transportable-macete)

(proof
(
direct-inference
(case-split ("p<=m"))
(induction integer-inductor ())
(prove-by-logic-and-simplification 3)
(apply-macete-with-minor-premises monoid-null-prod)
)))
```

```
(def-theorem local-context-introduction-for-monoid-prod
"forall(f:[zz,uu],m,n:zz,
monoid%prod(m,n,f)==monoid%prod(m,n,lambda(j:zz,if(m<=j and j<=n,f(j),e))))"
(theory monoid-theory)
(usages transportable-macete)
(proof
(
direct-inference
(instantiate-theorem locality-for-monoid-prod ("f" "lambda(j:zz,if(m<=j and j<=n, f(j), e))" "m" "n"))
(contrapose "with(p:prop, not(p))")
simplify
(contrapose "with(p:prop, not(p))")
simplify
)
))
```

```
(def-theorem interval-multiplicativity
"forall(m,n,p:zz, f:[zz,uu], m<=n and n<=p implies
monoid%prod(m,n,f) ** monoid%prod(n+1,p,f)
==
monoid%prod(m,p,f))"
(proof
(

(induction integer-inductor ("p"))
)
)
(usages transportable-macete)
(theory monoid-theory))
```

```
(def-theorem translation-invariance
"forall(m,n,p:zz, f:[zz,uu],
monoid%prod(m,n,f) == monoid%prod(m+p,n+p, lambda(n:zz, f(n-p))))"

(proof
(
direct-inference
(case-split ("m<=n"))
(induction integer-inductor ())
(unfold-single-defined-constant (1) monoid%prod)
simplify
(apply-macete-with-minor-premises monoid-null-prod)
)
)
(usages transportable-macete)
(theory monoid-theory))
```

```
(def-theory commutative-monoid-theory
(component-theories monoid-theory)
(axioms
(commutative-law-for-monoids "forall(x,y:uu, x ** y = y **x)")))
```

```
(def-constant zz%interval
"lambda(a,b:zz, indic{k:zz, a<=k and k<=b})"
(theory h-o-real-arithmetic))
```

```
(def-theorem reordering-lemma
"forall(a,b,d:zz, f:[zz,uu], a<=d and d<=b implies
monoid%prod(a,b,f)==monoid%prod(a,d-1,f)**monoid%prod(d+1,b,f)**f(d))"

(proof
(
(force-substitution "monoid%prod(a,d+1,f)**f(d)" "monoid%prod(a,d+1,f)**f(d)" ())
(force-substitution "monoid%prod(d+1,b,f)**f(d)" "f(d)**monoid%prod(d+1,b,f)" (0))
(force-substitution "monoid%prod(a,b,f)" "monoid%prod(a,d,f) ** monoid%prod(d+1,b,f)" (0))
(unfold-single-defined-constant (0) monoid%prod)
simplify
(apply-macete-with-minor-premises interval-multiplicativity)
(apply-macete-locally-with-minor-premises commutative-law-for-monoids (0) " monoid%prod(d+1,b,f)**f(d) ")
))
(theory commutative-monoid-theory))
```

```
(def-constant nullify%on%set
"lambda(f:[zz,uu],a:sets[zz], lambda(x:zz, if(x in a, e,f(x))))"
(theory monoid-theory))
```

```
(def-theorem reordering-lemma-corollary
"forall(a,b,d:zz, f:[zz,uu], a<=d and d<=b implies
monoid%prod(a,b,f)==monoid%prod(a,b,nullify%on%set(f,singleton{d})) ** f(d))"
(proof
(
(unfold-single-defined-constant (0) nullify%on%set)
(apply-macete-with-minor-premises tr%singleton-equality-conversion)
(force-substitution "monoid%prod(a,b,lambda(j:zz,if(j=d, e, f(j))))"
"monoid%prod(a,d-1,lambda(j:zz,if(j=d, e, f(j))))**
monoid%prod(d+1,b,lambda(j:zz,if(j=d, e, f(j))))**
lambda(j:zz,if(j=d, e, f(j)))(d)" (0))
direct-and-antecedent-inference-strategy
(cut-with-single-formula "monoid%prod(a,d-1,lambda(j:zz,if(j=d, e, f(j)))) ==
monoid%prod(a,d-1,f) and
monoid%prod(d+1,b,lambda(j:zz,if(j=d, e, f(j))))==monoid%prod(d+1,b,f)")
(backchain "with(b:zz,f:[zz,uu],d,a:zz,
monoid%prod(a,d-1,lambda(j:zz,if(j=d, e, f(j))))
==monoid%prod(a,d-1,f)
and
monoid%prod(d+1,b,lambda(j:zz,if(j=d, e, f(j))))
==monoid%prod(d+1,b,f));")
(backchain "with(b:zz,f:[zz,uu],d,a:zz,
monoid%prod(a,d-1,lambda(j:zz,if(j=d, e, f(j))))
==monoid%prod(a,d-1,f)
and
monoid%prod(d+1,b,lambda(j:zz,if(j=d, e, f(j))))
==monoid%prod(d+1,b,f));")
beta-reduce-repeatedly
(force-substitution "monoid%prod(d+1,b,f)**if(d=d, e, f(d))" "monoid%prod(d+1,b,f)" (0))
(force-substitution "(monoid%prod(a,d-1,f)**monoid%prod(d+1,b,f))**f(d)" "monoid%prod(a,d-1,f)**(monoid%prod(d+1,b,f)**f(d))" (0))
(apply-macete-with-minor-premises reordering-lemma)
(apply-macete-with-minor-premises associative-law-for-multiplication-for-monoids)
simplify
direct-inference
(apply-macete-with-minor-premises locality-for-monoid-prod)
(prove-by-logic-and-simplification 3)
(apply-macete-with-minor-premises locality-for-monoid-prod)
(prove-by-logic-and-simplification 3)
(apply-macete-with-minor-premises reordering-lemma)
))
(theory commutative-monoid-theory))
```

```
(def-theorem nullify%incrementally
"forall(c,t:zz,f:[zz,uu], phi:[zz,zz], c<=t implies
nullify%on%set(f,image{phi,zz%interval(c,t)})=
nullify%on%set(nullify%on%set(f,image{phi,zz%interval(c,t-1)}),singleton{phi(t)}))"
(proof
(

direct-and-antecedent-inference-strategy
unfold-defined-constants
extensionality
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
simplify-insistently
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 0)")
(case-split-on-conditionals (0 1))
(antecedent-inference "with(p:prop,p and p);")
(cut-with-single-formula "not(forsome(x:zz,c<=x and x<=t and x_0=phi(x)))")
(block
(script-comment "cut-with-single-formula' at (0)")
simplify
(contrapose "with(phi:[zz,zz],x_0,t,c:zz,
not(forsome(x:zz,c<=x and 1+x<=t and x_0=phi(x))));")
(instantiate-existential ("x"))
(cut-with-single-formula "not(x=t)")
simplify
(block
(script-comment "node added by `cut-with-single-formula' at (1)")
(contrapose "with(z,x_0:zz,not(x_0=z));")
simplify))
(block
(script-comment "node added by `cut-with-single-formula' at (1)")
(contrapose "with(p:prop,not(forsome(x:zz,p)));")
(instantiate-existential ("x"))
(cut-with-single-formula "not(x=t)")
simplify
(block
(script-comment "`cut-with-single-formula' at (1)")
(contrapose "with(p:prop,not(p));")
simplify)))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1 0)")
(contrapose "with(p:prop,not(p));")
(instantiate-existential ("t"))
simplify)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1 1 0 0 0)")
(contrapose "with(p:prop,not(forsome(x:zz,p)));")
(instantiate-existential ("x"))
simplify)
))
(theory monoid-theory))
```

```
(def-theorem general-commutative-law-induction-step-lemma
"forall(phi:[zz,zz],t,c:zz,f:[zz,uu],b,a:zz,
c<=t and
phi(t) in zz%interval(a,b) and
injective_q{phi}
implies
monoid%prod(a,
b,
nullify%on%set(f,image{phi,zz%interval(c,t)})) ** f(phi(t))
==monoid%prod(a,
b,
nullify%on%set(f,
image{phi,
zz%interval(c,t-1)})))"
(proof

(
(unfold-single-defined-constant (0) zz%interval)
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
(apply-macete nullify%incrementally)
(force-substitution "f(phi(t))" "nullify%on%set(f, image{phi, zz%interval(c, t- 1)})(phi(t))" (0))
(apply-macete-with-minor-premises reordering-lemma-corollary)
(unfold-single-defined-constant (0) nullify%on%set)
(force-substitution "phi(t) in image{phi,zz%interval(c,t-1)}" "falsehood" (0))
(unfold-single-defined-constant (0) zz%interval)
simplify-insistently
(contrapose "with(phi:[zz,zz],injective_q{phi});")
(instantiate-existential ("t" "x_\$2"))
simplify
))
(theory commutative-monoid-theory))
```

```
(def-theorem commutative-law-stack-lemma
"forall(phi:[zz,zz],t,c:zz,f:[zz,uu],b,a:zz,
c<=t and
phi(t) in zz%interval(a,b) and
injective_q{phi}
implies
monoid%prod(a,
b,
nullify%on%set(f,image{phi,zz%interval(c,t)})) **
monoid%prod(c,t,f oo phi)
==monoid%prod(a,
b,
nullify%on%set(f,
image{phi,
zz%interval(c,t-1)}))
**
monoid%prod(c,t-1,f oo phi))"
(theory commutative-monoid-theory)
(proof
(
direct-and-antecedent-inference-strategy
(apply-macete monoid-prod-out)
(force-substitution "monoid%prod(c,t-1,f oo phi)**f oo phi(t)" "f (phi(t)) ** monoid%prod(c,t-1,f oo phi)" (0))
(apply-macete-with-minor-premises associative-law-for-multiplication-for-monoids)
(apply-macete-with-minor-premises general-commutative-law-induction-step-lemma)
simplify-insistently
(apply-macete-locally commutative-law-for-monoids (0) " monoid%prod(c,[-1]+t,f oo phi)**f(phi(t)) ")
)))
```

```
(def-theorem constant-function-lemma
"forall(a,b,c:zz, f, g:[zz,ind_1], a<=b and forall(t:zz, a<=t and t<=b implies  f(t) == f(t-1)) and f(a-1)==g(c)
implies
f(b) == g(c))"
(proof

(
(induction integer-inductor ())
(prove-by-logic-and-simplification 3)
(backchain "with(f:[zz,ind_1],t,a:zz,
forall(t_\$0:zz,
a<=t_\$0 and t_\$0<=1+t implies f(t_\$0)==f([-1]+t_\$0)));")
(prove-by-logic-and-simplification 3)
))
(usages transportable-macete)
(theory generic-theory-1))
```

```
(def-theorem general-commutative-law
"forall(a,b,c,d:zz, phi:[zz,zz], f:[zz,uu],
zz%interval(c,d) subseteq dom{phi} and
injective_q{phi} and c<=d and
image{phi,zz%interval(c,d)} subseteq zz%interval(a,b)
implies
monoid%prod(a,b,nullify%on%set(f,image{phi,zz%interval(c,d)})) **
monoid%prod(c,d,f oo phi)
== monoid%prod(a,b,f))"
(theory commutative-monoid-theory)
(usages transportable-macete)
lemma
(proof
(
(force-substitution "monoid%prod(a,
b,
nullify%on%set(f,image{phi,zz%interval(c,d)}))**
monoid%prod(c,d,f oo phi)==monoid%prod(a,b,f)" "lambda(t:zz,monoid%prod(a,
b,
nullify%on%set(f,image{phi,zz%interval(c,t)}))**
monoid%prod(c,t,f oo phi))(d)==lambda(x:zz,monoid%prod(a,x,f))(b)" (0))
(apply-macete-with-minor-premises tr%constant-function-lemma)
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
(instantiate-existential ("c"))
(cut-with-single-formula "phi(t_\$1) in zz%interval(a,b)")
(apply-macete commutative-law-stack-lemma)
(incorporate-antecedent "with(b,a:zz,phi:[zz,zz],d,c:zz,
image{phi,zz%interval(c,d)} subseteq zz%interval(a,b));")
(incorporate-antecedent "with(phi:[zz,zz],d,c:zz,zz%interval(c,d) subseteq dom{phi});")
unfold-defined-constants
direct-and-antecedent-inference-strategy
(backchain "with(b,a:zz,phi:[zz,zz],d,c:zz,
image{phi,indic{k:zz,  c<=k and k<=d}}
subseteq indic{k:zz,  a<=k and k<=b});")
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-with-minor-premises
beta-reduce-repeatedly
(instantiate-existential ("t_\$1"))
(incorporate-antecedent "with(phi:[zz,zz],d,c:zz,
indic{k:zz,  c<=k and k<=d} subseteq dom{phi});")
(weaken (0 3))
simplify-insistently
(weaken (0 4))
(incorporate-antecedent "with(phi:[zz,zz],d,c:zz,
indic{k:zz,  c<=k and k<=d} subseteq dom{phi});")
(apply-macete monoid-null-prod)
simplify
(apply-macete-with-minor-premises locality-for-monoid-prod)
direct-and-antecedent-inference-strategy
(weaken (6 5 4 3 2 1 0))
unfold-defined-constants
simplify-insistently
(unfold-single-defined-constant (0) nullify%on%set)
beta-reduce-repeatedly
)))
```

```
(def-theorem nullified-monoid%prod-lemma
"forall(a,b:zz, s:sets[zz], f:[zz,uu],
zz%interval(a,b) subseteq s
implies
monoid%prod(a,b,nullify%on%set(f,s))==e)"
(theory monoid-theory)
lemma
(proof
(
(force-substitution "e" " monoid%prod(a, b,lambda(x:zz,e))" (0))
(apply-macete-with-minor-premises locality-for-monoid-prod)
beta-reduce-repeatedly
(unfold-single-defined-constant (0) nullify%on%set)
direct-and-antecedent-inference-strategy
(cut-with-single-formula "x in s")
simplify
(backchain "with(s:sets[zz],b,a:zz,zz%interval(a,b) subseteq s);")
(unfold-single-defined-constant (0) zz%interval)
simplify-insistently
(unfold-single-defined-constant (0) nullify%on%set)
(weaken (0))
(case-split ("a<=b"))
(induction integer-inductor ())
(apply-macete-with-minor-premises monoid-null-prod)
)))
```

```
(def-theorem general-commutative-law-corollary
"forall(a,b,c,d:zz, phi:[zz,zz], f:[zz,uu],
zz%interval(c,d) subseteq dom{phi} and
injective_q{phi} and c<=d and
image{phi,zz%interval(c,d)}=zz%interval(a,b)
implies
monoid%prod(c,d,f oo phi) == monoid%prod(a,b,f))"
(theory commutative-monoid-theory)
(usages transportable-macete)
lemma
(proof
(
direct-and-antecedent-inference-strategy
(force-substitution "monoid%prod(c,d,f oo phi)" "monoid%prod(a,b,nullify%on%set(f,image{phi,zz%interval(c,d)}))**monoid%prod(c,d,f oo phi)" (0))
(apply-macete-with-minor-premises general-commutative-law)
(apply-macete-with-minor-premises nullified-monoid%prod-lemma)
simplify
)))
```

```
(def-translation commutative-monoid-theory-to-multiplicative-rr
(source commutative-monoid-theory)
(target h-o-real-arithmetic)
(fixed-theories h-o-real-arithmetic)
(sort-pairs
(uu rr))
(constant-pairs
(e 1)
(** *)
)
(theory-interpretation-check using-simplification))
```

```
(source commutative-monoid-theory)
(target h-o-real-arithmetic)
(fixed-theories h-o-real-arithmetic)
(sort-pairs
(uu rr))
(constant-pairs
(e 0)
(** +)
)
(theory-interpretation-check using-simplification))
```

```(def-transported-symbols nullify%on%set
```

```
(def-theorem sum-nonnegativity
Remark: This entry is multiply defined. See:  [1] [2]
"forall(f:[zz,rr], a,b:zz, forall(z:zz,a<=z and z<=b implies 0<=f(z))
implies 0<=sum(a,b,f))"
(theory h-o-real-arithmetic)
(proof
(

direct-and-antecedent-inference-strategy
(case-split ("a<=b"))
(induction integer-inductor ())
direct-and-antecedent-inference-strategy
(cut-with-single-formula "0<=sum(a,t,f) and 0<=f(1+t)")
simplify
(prove-by-logic-and-simplification 3)
(unfold-single-defined-constant (0) sum)
simplify
)
))
```

```
(def-theorem cardinality-definedness-lemma
"forall(a,b,c,d:zz,phi:[zz,zz],
zz%interval(c,d) subseteq dom{phi}
and
injective_q{phi}
and
c<=d
and
image{phi,zz%interval(c,d)} subseteq zz%interval(a,b)
implies
d-c<=b-a)"
(theory h-o-real-arithmetic)
(proof
(
direct-and-antecedent-inference-strategy
(force-substitution "d-c<=b-a" "(d+1)-c<=(b+1)-a" (0))
(force-substitution "(b+1)-a" "sum(a,b,zero%on%set(lambda(x:zz,1),
image{phi,zz%interval(c,d)}))+sum(c,d,lambda(x:zz,1) oo phi)" (0))
(cut-with-single-formula "(d+1)-c=sum(c,d,lambda(x:zz,1) oo phi)
and 0<=sum(a, b, zero%on%set(lambda(x:zz,1), image{phi,zz%interval(c,d)}))")
simplify
direct-and-antecedent-inference-strategy
(weaken (0 2))
(induction integer-inductor ())
simplify-insistently
direct-and-antecedent-inference-strategy
beta-reduce-with-minor-premises
(backchain "with(phi:[zz,zz],c:zz,
forall(x_\$2:zz,c<=x_\$2 and x_\$2<=c implies #(phi(x_\$2))));")
simplify
(backchain "with(phi:[zz,zz],t,c:zz,
zz%interval(c,t) subseteq dom{phi}
implies
1+t=c+sum(c,t,lambda(x:zz,1) oo phi));")
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%subseteq-transitivity)
(instantiate-existential ("zz%interval(c,1+t)"))
unfold-defined-constants
simplify-insistently
(unfold-single-defined-constant (0) zz%interval)
(unfold-single-defined-constant (0) zz%interval)
(backchain-backwards "with(phi:[zz,zz],t,c:zz,
zz%interval(c,t) subseteq dom{phi}
implies
1+t=c+sum(c,t,lambda(x:zz,1) oo phi));")
beta-reduce-with-minor-premises
(antecedent-inference "with(phi:[zz,zz],t,c:zz,
zz%interval(c,t) subseteq dom{phi}
implies
1+t=c+sum(c,t,lambda(x:zz,1) oo phi));")
simplify
(incorporate-antecedent "with(phi:[zz,zz],t,c:zz,
zz%interval(c,1+t) subseteq dom{phi});")
(unfold-single-defined-constant (0) zz%interval)
simplify-insistently
direct-and-antecedent-inference-strategy
(backchain "with(phi:[zz,zz],t,c:zz,
forall(x_\$0:zz,
c<=x_\$0 and x_\$0<=1+t implies #(phi(x_\$0))));")
simplify
(apply-macete-with-minor-premises sum-nonnegativity)
direct-and-antecedent-inference-strategy
(unfold-single-defined-constant (0) zero%on%set)
(raise-conditional (0))
direct-inference
simplify
simplify
(unfold-single-defined-constant (0) zero%on%set)
(apply-macete-with-minor-premises tr%general-commutative-law)
(cut-with-single-formula "a<=b")
(weaken (1 2 3 4))
(induction integer-inductor ())
(cut-with-single-formula "phi(c) in zz%interval(a,b)")
(incorporate-antecedent "with(c:zz,phi:[zz,zz],b,a:zz,phi(c) in zz%interval(a,b));")
(unfold-single-defined-constant (0) zz%interval)
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
simplify
(backchain "with(b,a:zz,phi:[zz,zz],d,c:zz,
image{phi,zz%interval(c,d)} subseteq zz%interval(a,b));")
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-with-minor-premises
(instantiate-existential ("c"))
(unfold-single-defined-constant (0) zz%interval)
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
simplify
(incorporate-antecedent "with(phi:[zz,zz],d,c:zz,zz%interval(c,d) subseteq dom{phi});")
(unfold-single-defined-constant (0) zz%interval)
simplify-insistently
direct-and-antecedent-inference-strategy
(backchain "with(phi:[zz,zz],d,c:zz,
forall(x_\$0:zz,c<=x_\$0 and x_\$0<=d implies #(phi(x_\$0))));")
simplify
(incorporate-antecedent "with(phi:[zz,zz],d,c:zz,zz%interval(c,d) subseteq dom{phi});")
(unfold-single-defined-constant (0) zz%interval)
simplify-insistently
direct-and-antecedent-inference-strategy
(backchain "with(phi:[zz,zz],d,c:zz,
forall(x_\$0:zz,c<=x_\$0 and x_\$0<=d implies #(phi(x_\$0))));")
simplify
simplify
)))
```