---

Step * 2 1 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)
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])
BY
{ (With ⌜P⌝ (D (-2)) ⋅ 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. [P] : (T List) ⟶ ℙ
5. (∀j:T List. ((∀k:T List. ((k lexico(T; a,b.lt[a;b]) j) ⇒ P[k])) ⇒ P[j])) ⇒ {∀n:T List. P[n]}
⊢ (∀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)
5.  [P]  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
\mvdash{}  (\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:
(With  \mkleeneopen{}P\mkleeneclose{}  (D  (-2))  \mcdot{}  THENA  Auto)

---

Home Index