Step
*
2
2
1
of Lemma
llex-append1
1. [A] : Type
2. [<] : A ⟶ A ⟶ ℙ
3. L1 : A List
4. L2 : A List
5. a : A
6. i : ℕ
7. i < ||L1||
8. i < ||L2 @ [a]||
9. ∀j:ℕi. (L1[j] = L2 @ [a][j] ∈ A)
10. <[L1[i];L2 @ [a][i]]
11. ¬i < ||L2||
⊢ ∃L3:A List. ((L1 = (L2 @ L3) ∈ (A List)) ∧ <[hd(L3);a] supposing 0 < ||L3||)
BY
{ ((Assert i = ||L2|| ∈ ℤ BY Auto') THEN Eliminate ⌜i⌝⋅ THEN ThinVar `i' THEN Thin (-1) THEN Thin (-3)) }
1
1. [A] : Type
2. L2 : A List
3. [<] : A ⟶ A ⟶ ℙ
4. L1 : A List
5. a : A
6. ||L2|| < ||L1||
7. ∀j:ℕ||L2||. (L1[j] = L2 @ [a][j] ∈ A)
8. <[L1[||L2||];L2 @ [a][||L2||]]
⊢ ∃L3:A List. ((L1 = (L2 @ L3) ∈ (A List)) ∧ <[hd(L3);a] supposing 0 < ||L3||)
Latex:
Latex:
1. [A] : Type
2. [<] : A {}\mrightarrow{} A {}\mrightarrow{} \mBbbP{}
3. L1 : A List
4. L2 : A List
5. a : A
6. i : \mBbbN{}
7. i < ||L1||
8. i < ||L2 @ [a]||
9. \mforall{}j:\mBbbN{}i. (L1[j] = L2 @ [a][j])
10. <[L1[i];L2 @ [a][i]]
11. \mneg{}i < ||L2||
\mvdash{} \mexists{}L3:A List. ((L1 = (L2 @ L3)) \mwedge{} <[hd(L3);a] supposing 0 < ||L3||)
By
Latex:
((Assert i = ||L2|| BY Auto') THEN Eliminate \mkleeneopen{}i\mkleeneclose{}\mcdot{} THEN ThinVar `i' THEN Thin (-1) THEN Thin (-3))
Home
Index