---

Step * of Lemma l-ordered-equality

No Annotations
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  (∀as,bs:T List.
     (l-ordered(T;x,y.R[x;y];as)
     ⇒ l-ordered(T;x,y.R[x;y];bs)
     ⇒ (as = bs ∈ (T List) ⇐⇒ ∀x:T. ((x ∈ as) ⇐⇒ (x ∈ bs))))) supposing 
     ((∀x,y:T.  (R[x;y] ⇒ (¬R[y;x]))) and 
     (∀x:T. (¬R[x;x])))
BY
{ ((((UnivCD THENA Auto) THEN (InstLemma `no_repeats-before-equality` [⌜T⌝; ⌜as⌝; ⌜bs⌝])⋅) THENA Auto)
   THEN Try (((Using [`R',⌜R⌝] (BLemma `l-ordered-no_repeats`))⋅ THEN Auto))
   THEN ParallelLast) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. ∀x:T. (¬R[x;x])
4. ∀x,y:T.  (R[x;y] ⇒ (¬R[y;x]))
5. as : T List
6. bs : T List
7. l-ordered(T;x,y.R[x;y];as)
8. l-ordered(T;x,y.R[x;y];bs)
9. as = bs ∈ (T List)
10. (∀x:T. ((x ∈ as) ⇐⇒ (x ∈ bs))) ∧ (∀x,y:T.  (x before y ∈ as ⇐⇒ x before y ∈ bs))
⊢ ∀x:T. ((x ∈ as) ⇐⇒ (x ∈ bs))

2
.....antecedent..... 
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. ∀x:T. (¬R[x;x])
4. ∀x,y:T.  (R[x;y] ⇒ (¬R[y;x]))
5. as : T List
6. bs : T List
7. l-ordered(T;x,y.R[x;y];as)
8. l-ordered(T;x,y.R[x;y];bs)
9. ∀x:T. ((x ∈ as) ⇐⇒ (x ∈ bs))
⊢ (∀x:T. ((x ∈ as) ⇐⇒ (x ∈ bs))) ∧ (∀x,y:T.  (x before y ∈ as ⇐⇒ x before y ∈ bs))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (\mforall{}as,bs:T  List.
          (l-ordered(T;x,y.R[x;y];as)
          {}\mRightarrow{}  l-ordered(T;x,y.R[x;y];bs)
          {}\mRightarrow{}  (as  =  bs  \mLeftarrow{}{}\mRightarrow{}  \mforall{}x:T.  ((x  \mmember{}  as)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  bs)))))  supposing 
          ((\mforall{}x,y:T.    (R[x;y]  {}\mRightarrow{}  (\mneg{}R[y;x])))  and 
          (\mforall{}x:T.  (\mneg{}R[x;x])))


By

---

Latex:
((((UnivCD  THENA  Auto)  THEN  (InstLemma  `no\_repeats-before-equality`  [\mkleeneopen{}T\mkleeneclose{};  \mkleeneopen{}as\mkleeneclose{};  \mkleeneopen{}bs\mkleeneclose{}])\mcdot{})  THENA  Auto)
  THEN  Try  (((Using  [`R',\mkleeneopen{}R\mkleeneclose{}]  (BLemma  `l-ordered-no\_repeats`))\mcdot{}  THEN  Auto))
  THEN  ParallelLast)

---

Home Index