---

Step * of Lemma lexico_induction

∀[T:Type]. ∀[lt:T ⟶ T ⟶ ℙ].
  ((∀[Q:T ⟶ ℙ]. ((∀b:T. ((∀a:T. (lt[a;b] ⇒ Q[a])) ⇒ Q[b])) ⇒ (∀b:T. Q[b])))
  ⇒ (∀[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
{ (InstLemma `lexico_well_fnd` [] THEN RepeatFor 2 (ParallelLast') THEN (D 0 THENA Auto) THEN D -2) }

1
.....antecedent..... 
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'
⊢ WellFnd{i}(T;a,b.lt[a;b])

2
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]))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[lt:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    ((\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])))
    {}\mRightarrow{}  (\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:
(InstLemma  `lexico\_well\_fnd`  []  THEN  RepeatFor  2  (ParallelLast')  THEN  (D  0  THENA  Auto)  THEN  D  -2)

---

Home Index