---

Step * 1 2 of Lemma qadd_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
{ TACTIC:(((Reduce 0 THENM GenRepD) THENM RW bool_to_propC 0) THENA Auto) }

1
UniformLinorder(ℚ;x,y.↑q_le(x;y))

2
(λx,y. qeq(x;y)) = (λx,y. (q_le(x;y) ∧b q_le(y;x))) ∈ (ℚ ⟶ ℚ ⟶ 𝔹)

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

4
1. z : ℚ
⊢ monot(ℚ;x,y.↑q_le(x;y);λw.(z + w))

---

Latex:

---

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


By

---

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

---

Home Index