Step
*
of Lemma
before-upto
∀n:ℕ. ∀x,y:ℕn. (x before y ∈ upto(n)
⇐⇒ x < y)
BY
{ (Unfold `l_before` 0 THEN Unfold `sublist` 0 THEN Reduce 0 THEN Auto THEN Reduce 0 THEN Auto' THEN ExRepD) }
1
1. n : ℕ
2. x : ℕn
3. y : ℕn
4. f : ℕ2 ⟶ ℕ||upto(n)||
5. increasing(f;2)
6. ∀j:ℕ2. ([x; y][j] = upto(n)[f j] ∈ ℕn)
⊢ x < y
2
1. n : ℕ
2. x : ℕn
3. y : ℕn
4. f : ℕ2 ⟶ ℕ||upto(n)||
5. increasing(f;2)
6. j : ℕ2
⊢ f j < n
3
1. n : ℕ
2. x : ℕn
3. y : ℕn
4. x < y
⊢ ∃f:ℕ2 ⟶ ℕ||upto(n)||. (increasing(f;2) ∧ (∀j:ℕ2. ([x; y][j] = upto(n)[f j] ∈ ℕn)))
Latex:
Latex:
\mforall{}n:\mBbbN{}. \mforall{}x,y:\mBbbN{}n. (x before y \mmember{} upto(n) \mLeftarrow{}{}\mRightarrow{} x < y)
By
Latex:
(Unfold `l\_before` 0
THEN Unfold `sublist` 0
THEN Reduce 0
THEN Auto
THEN Reduce 0
THEN Auto'
THEN ExRepD)
Home
Index