Step
*
of Lemma
oal_lt_irrefl
∀s:LOSet. ∀g:OCMon. Irrefl(|oal(s;g)|;ps,qs.ps << qs)
BY
{ ((RepUnfolds ``irrefl not`` 0
THENM RepD
THENM Unfold `oal_lt` (-1)
THENM ExRepD) THENA Auto) }
1
1. s : LOSet@i'
2. g : OCMon@i'
3. a : |oal(s;g)|
4. k : |s|@i
5. ∀k':|s|. ((k <s k')
⇒ ((a[k']) = (a[k']) ∈ |g|))@i
6. (a[k]) < (a[k])@i
⊢ False
Latex:
Latex:
\mforall{}s:LOSet. \mforall{}g:OCMon. Irrefl(|oal(s;g)|;ps,qs.ps << qs)
By
Latex:
((RepUnfolds ``irrefl not`` 0
THENM RepD
THENM Unfold `oal\_lt` (-1)
THENM ExRepD) THENA Auto)
Home
Index