---

Step * of Lemma before_trans

∀a:LOSet. ∀u,v:|a|. ∀ws:|a| List.  ((v <a u) ⇒ (↑before(v;ws)) ⇒ (↑before(u;ws)))
BY
{ ((RepeatMFor 4 (D 0) 
THENM OnVar `ws' D) THENA Auto) 
THEN AbReduce 0 THEN ((RW bool_to_propC 0) THEN Auto) }

1
1. a : LOSet@i'
2. u : |a|@i
3. v : |a|@i
4. u1 : |a|
5. v1 : |a| List
6. v <a u@i
7. u1 <a v@i
⊢ u1 <a u

---

Latex:

---

Latex:
\mforall{}a:LOSet.  \mforall{}u,v:|a|.  \mforall{}ws:|a|  List.    ((v  <a  u)  {}\mRightarrow{}  (\muparrow{}before(v;ws))  {}\mRightarrow{}  (\muparrow{}before(u;ws)))


By

---

Latex:
((RepeatMFor  4  (D  0) 
THENM  OnVar  `ws'  D)  THENA  Auto) 
THEN  AbReduce  0  THEN  ((RW  bool\_to\_propC  0)  THEN  Auto)

---

Home Index