Step
*
2
of Lemma
lexico_well_fnd
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. WellFnd{i}(T;a,b.R[a;b])
4. ∀m:ℕ. WellFnd{i}({L:T List| ||L|| = m ∈ ℕ} ;as,bs.as lexico(T; a,b.R[a;b]) bs)
⊢ WellFnd{i}(T List;as,bs.as lexico(T; a,b.R[a;b]) bs)
BY
{ ((D 0 THEN Auto) THEN Unfold `guard` 0) }
1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. WellFnd{i}(T;a,b.R[a;b])
4. ∀m:ℕ. WellFnd{i}({L:T List| ||L|| = m ∈ ℕ} ;as,bs.as lexico(T; a,b.R[a;b]) bs)
5. [P] : (T List) ⟶ ℙ
6. ∀j:T List. ((∀k:T List. ((k lexico(T; a,b.R[a;b]) j)
⇒ P[k]))
⇒ P[j])
⊢ ∀n:T List. P[n]
Latex:
Latex:
1. [T] : Type
2. [R] : T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}
3. WellFnd\{i\}(T;a,b.R[a;b])
4. \mforall{}m:\mBbbN{}. WellFnd\{i\}(\{L:T List| ||L|| = m\} ;as,bs.as lexico(T; a,b.R[a;b]) bs)
\mvdash{} WellFnd\{i\}(T List;as,bs.as lexico(T; a,b.R[a;b]) bs)
By
Latex:
((D 0 THEN Auto) THEN Unfold `guard` 0)
Home
Index