---

Step * of Lemma descending-append

No Annotations
∀[A:Type]. ∀[<:A ⟶ A ⟶ ℙ].
  ∀L1,L2:A List.
    (descending(a,b.<[a;b];L1 @ L2)
    ⇐⇒ descending(a,b.<[a;b];L1)
        ∧ descending(a,b.<[a;b];L2)
        ∧ (<[hd(L2);last(L1)]) supposing (0 < ||L2|| and 0 < ||L1||))
BY
{ ((UnivCD THENA Auto) THEN RepeatFor 2 ((D 0 THENA Auto))) }

1
1. [A] : Type
2. [<] : A ⟶ A ⟶ ℙ
3. L1 : A List
4. L2 : A List
5. descending(a,b.<[a;b];L1 @ L2)
⊢ descending(a,b.<[a;b];L1) ∧ descending(a,b.<[a;b];L2) ∧ (<[hd(L2);last(L1)]) supposing (0 < ||L2|| and 0 < ||L1||)

2
1. [A] : Type
2. [<] : A ⟶ A ⟶ ℙ
3. L1 : A List
4. L2 : A List
5. descending(a,b.<[a;b];L1) ∧ descending(a,b.<[a;b];L2) ∧ (<[hd(L2);last(L1)]) supposing (0 < ||L2|| and 0 < ||L1||)
⊢ descending(a,b.<[a;b];L1 @ L2)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A:Type].  \mforall{}[<:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}L1,L2:A  List.
        (descending(a,b.<[a;b];L1  @  L2)
        \mLeftarrow{}{}\mRightarrow{}  descending(a,b.<[a;b];L1)
                \mwedge{}  descending(a,b.<[a;b];L2)
                \mwedge{}  (<[hd(L2);last(L1)])  supposing  (0  <  ||L2||  and  0  <  ||L1||))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepeatFor  2  ((D  0  THENA  Auto)))

---

Home Index