---

Step * 1 1 of Lemma lexico_well_fnd

.....basecase..... 
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. WellFnd{i}(T;a,b.R[a;b])
⊢ WellFnd{i}({L:T List| ||L|| = 0 ∈ ℕ} ;as,bs.as lexico(T; a,b.R[a;b]) bs)
BY
{ xxx((InstLemma `lexico_wf` [⌜T⌝;⌜R⌝]⋅ THENA Auto) THEN RepeatFor 2 ((D 0 THEN Auto)) THEN D -1 THEN D -2)xxx }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. WellFnd{i}(T;a,b.R[a;b])
4. lexico(T; a,b.R[a;b]) ∈ (T List) ⟶ (T List) ⟶ ℙ
5. [P] : {L:T List| ||L|| = 0 ∈ ℕ}  ⟶ ℙ
6. ∀j:{L:T List| ||L|| = 0 ∈ ℕ} . ((∀k:{L:T List| ||L|| = 0 ∈ ℕ} . ((k lexico(T; a,b.R[a;b]) j) ⇒ P[k])) ⇒ P[j])
7. [%6] : ||[]|| = 0 ∈ ℕ
⊢ P[[]]

2
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. WellFnd{i}(T;a,b.R[a;b])
4. lexico(T; a,b.R[a;b]) ∈ (T List) ⟶ (T List) ⟶ ℙ
5. [P] : {L:T List| ||L|| = 0 ∈ ℕ}  ⟶ ℙ
6. ∀j:{L:T List| ||L|| = 0 ∈ ℕ} . ((∀k:{L:T List| ||L|| = 0 ∈ ℕ} . ((k lexico(T; a,b.R[a;b]) j) ⇒ P[k])) ⇒ P[j])
7. u : T
8. v : T List
9. [%6] : ||[u / v]|| = 0 ∈ ℕ
⊢ P[[u / v]]

---

Latex:

---

Latex:
.....basecase..... 
1.  [T]  :  Type
2.  [R]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  WellFnd\{i\}(T;a,b.R[a;b])
\mvdash{}  WellFnd\{i\}(\{L:T  List|  ||L||  =  0\}  ;as,bs.as  lexico(T;  a,b.R[a;b])  bs)


By

---

Latex:
xxx((InstLemma  `lexico\_wf`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  RepeatFor  2  ((D  0  THEN  Auto))
        THEN  D  -1
        THEN  D  -2)xxx

---

Home Index