---

Step * 2 of Lemma lexico_induction


1. [T] : Type
2. [lt] : T ⟶ T ⟶ ℙ
3. ∀[Q:T ⟶ ℙ]. ((∀b:T. ((∀a:T. (lt[a;b] ⇒ Q[a])) ⇒ Q[b])) ⇒ (∀b:T. Q[b]))@i'
4. WellFnd{i}(T List;as,bs.as lexico(T; a,b.lt[a;b]) bs)
⊢ ∀[P:(T List) ⟶ ℙ]
    ((∀L:T List. ((∀L':T List. ((L' lexico(T; a,b.lt[a;b]) L) ⇒ P[L'])) ⇒ P[L])) ⇒ (∀L:T List. P[L]))
BY
{ (D 0 THENA Auto) }

1
1. [T] : Type
2. [lt] : T ⟶ T ⟶ ℙ
3. ∀[Q:T ⟶ ℙ]. ((∀b:T. ((∀a:T. (lt[a;b] ⇒ Q[a])) ⇒ Q[b])) ⇒ (∀b:T. Q[b]))@i'
4. WellFnd{i}(T List;as,bs.as lexico(T; a,b.lt[a;b]) bs)
5. [P] : (T List) ⟶ ℙ
⊢ (∀L:T List. ((∀L':T List. ((L' lexico(T; a,b.lt[a;b]) L) ⇒ P[L'])) ⇒ P[L])) ⇒ (∀L:T List. P[L])

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [lt]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}[Q:T  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}b:T.  ((\mforall{}a:T.  (lt[a;b]  {}\mRightarrow{}  Q[a]))  {}\mRightarrow{}  Q[b]))  {}\mRightarrow{}  (\mforall{}b:T.  Q[b]))@i'
4.  WellFnd\{i\}(T  List;as,bs.as  lexico(T;  a,b.lt[a;b])  bs)
\mvdash{}  \mforall{}[P:(T  List)  {}\mrightarrow{}  \mBbbP{}]
        ((\mforall{}L:T  List.  ((\mforall{}L':T  List.  ((L'  lexico(T;  a,b.lt[a;b])  L)  {}\mRightarrow{}  P[L']))  {}\mRightarrow{}  P[L]))
        {}\mRightarrow{}  (\mforall{}L:T  List.  P[L]))


By

---

Latex:
(D  0  THENA  Auto)

---

Home Index