---

Step * 1 1 of Lemma oal_lt_iff_grp_lt


1. s : LOSet@i'
2. g : OGrp@i'
3. ps : |oal(s;g)|@i
4. qs : |oal(s;g)|@i
⊢ ps << qs ⇐⇒ (ps ≤ qs) ∧ (¬(qs ≤ ps))
BY
{ % Need binrel_ap abstraction here for  
  functionality reasoning in subsequent rewrite % 
 
RWN 2 ab_binrel_apC 0 
 }

1
1. s : LOSet@i'
2. g : OGrp@i'
3. ps : |oal(s;g)|@i
4. qs : |oal(s;g)|@i
⊢ ps [x,y:|oal(s;g)|. x << y] qs ⇐⇒ (ps ≤ qs) ∧ (¬(qs ≤ ps))

---

Latex:

---

Latex:

1.  s  :  LOSet@i'
2.  g  :  OGrp@i'
3.  ps  :  |oal(s;g)|@i
4.  qs  :  |oal(s;g)|@i
\mvdash{}  ps  <<  qs  \mLeftarrow{}{}\mRightarrow{}  (ps  \mleq{}  qs)  \mwedge{}  (\mneg{}(qs  \mleq{}  ps))


By

---

Latex:
\%  Need  binrel\_ap  abstraction  here  for   
    functionality  reasoning  in  subsequent  rewrite  \% 
 
RWN  2  ab\_binrel\_apC  0 

---

Home Index