---

Step * of Lemma oal_lt_trans

No Annotations
∀s:LOSet. ∀g:OCMon.  Trans(|oal(s;g)|;ps,qs.ps << qs)
BY
{ (((ARepD ["basic"] 
   THENM OnCls [0;-1;-2] (Unfold `oal_lt`) 
   THENM ExRepD) THENA Auto)
   THEN Try (Complete ((BLemma `omon_inc` THEN Auto)))
   ) }

1
1. s : LOSet
2. g : OCMon
3. a : |oal(s;g)|
4. b : |oal(s;g)|
5. c : |oal(s;g)|
6. k1 : |s|
7. ∀k':|s|. ((k1 <s k') ⇒ ((a[k']) = (b[k']) ∈ |g|))
8. (a[k1]) < (b[k1])
9. k : |s|
10. ∀k':|s|. ((k <s k') ⇒ ((b[k']) = (c[k']) ∈ |g|))
11. (b[k]) < (c[k])
⊢ ∃k:|s|. ((∀k':|s|. ((k <s k') ⇒ ((a[k']) = (c[k']) ∈ |g|))) ∧ ((a[k]) < (c[k])))

---

Latex:

---

Latex:
No  Annotations
\mforall{}s:LOSet.  \mforall{}g:OCMon.    Trans(|oal(s;g)|;ps,qs.ps  <<  qs)


By

---

Latex:
(((ARepD  ["basic"] 
  THENM  OnCls  [0;-1;-2]  (Unfold  `oal\_lt`) 
  THENM  ExRepD)  THENA  Auto)
  THEN  Try  (Complete  ((BLemma  `omon\_inc`  THEN  Auto)))
  )

---

Home Index