---

Step * of Lemma l-ordered-append

∀[T:Type]
  ∀L1,L2:T List.
    ∀[R:T ⟶ T ⟶ ℙ]
      (l-ordered(T;x,y.R[x;y];L1 @ L2)
      ⇐⇒ l-ordered(T;x,y.R[x;y];L1) ∧ l-ordered(T;x,y.R[x;y];L2) ∧ (∀x,y:T.  ((x ∈ L1) ⇒ (y ∈ L2) ⇒ R[x;y])))
BY
{ Auto }

1
1. [T] : Type
2. L1 : T List@i
3. L2 : T List@i
4. [R] : T ⟶ T ⟶ ℙ
5. l-ordered(T;x,y.R[x;y];L1 @ L2)@i
⊢ l-ordered(T;x,y.R[x;y];L1)

2
1. [T] : Type
2. L1 : T List@i
3. L2 : T List@i
4. [R] : T ⟶ T ⟶ ℙ
5. l-ordered(T;x,y.R[x;y];L1 @ L2)@i
⊢ l-ordered(T;x,y.R[x;y];L2)

3
1. [T] : Type
2. L1 : T List@i
3. L2 : T List@i
4. [R] : T ⟶ T ⟶ ℙ
5. l-ordered(T;x,y.R[x;y];L1 @ L2)@i
6. x : T@i
7. y : T@i
8. (x ∈ L1)@i
9. (y ∈ L2)@i
⊢ R[x;y]

4
1. [T] : Type
2. L1 : T List@i
3. L2 : T List@i
4. [R] : T ⟶ T ⟶ ℙ
5. l-ordered(T;x,y.R[x;y];L1)@i
6. l-ordered(T;x,y.R[x;y];L2)@i
7. ∀x,y:T.  ((x ∈ L1) ⇒ (y ∈ L2) ⇒ R[x;y])@i
⊢ l-ordered(T;x,y.R[x;y];L1 @ L2)

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}L1,L2:T  List.
        \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}]
            (l-ordered(T;x,y.R[x;y];L1  @  L2)
            \mLeftarrow{}{}\mRightarrow{}  l-ordered(T;x,y.R[x;y];L1)
                    \mwedge{}  l-ordered(T;x,y.R[x;y];L2)
                    \mwedge{}  (\mforall{}x,y:T.    ((x  \mmember{}  L1)  {}\mRightarrow{}  (y  \mmember{}  L2)  {}\mRightarrow{}  R[x;y])))


By

---

Latex:
Auto

---

Home Index