---

Step * 1 2 of Lemma int_add_grp_wf2

.....set predicate..... 
(UniformLinorder(|<ℤ+>|;x,y.↑(x ≤b y)) ∧ (=b = (λx,y. ((x ≤b y) ∧b (y ≤b x))) ∈ (|<ℤ+>| ⟶ |<ℤ+>| ⟶ 𝔹)))
∧ Cancel(|<ℤ+>|;|<ℤ+>|;*)
∧ (∀[z:|<ℤ+>|]. monot(|<ℤ+>|;x,y.↑(x ≤b y);λw.(z * w)))
BY
{ ((Reduce 0 THENM GenRepD 
THENM RW bool_to_propC 0) THENA Auto) }

1
UniformLinorder(ℤ;x,y.x ≤ y)

2
(λx,y. (x =z y)) = (λx,y. (x ≤z y ∧b y ≤z x)) ∈ (ℤ ⟶ ℤ ⟶ 𝔹)

3
Cancel(ℤ;ℤ;λx,y. (x + y))

4
1. z : ℤ
⊢ monot(ℤ;x,y.x ≤ y;λw.(z + w))

---

Latex:

---

Latex:
.....set  predicate..... 
(UniformLinorder(|<\mBbbZ{}+>|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))  \mwedge{}  (=\msubb{}  =  (\mlambda{}x,y.  ((x  \mleq{}\msubb{}  y)  \mwedge{}\msubb{}  (y  \mleq{}\msubb{}  x)))))
\mwedge{}  Cancel(|<\mBbbZ{}+>|;|<\mBbbZ{}+>|;*)
\mwedge{}  (\mforall{}[z:|<\mBbbZ{}+>|].  monot(|<\mBbbZ{}+>|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y);\mlambda{}w.(z  *  w)))


By

---

Latex:
((Reduce  0  THENM  GenRepD 
THENM  RW  bool\_to\_propC  0)  THENA  Auto)

---

Home Index