---

Step * of Lemma accessible-induction

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[P:T ⟶ ℙ].
  ((∀t:T. ((∀x:T. (R[x;t] ⇒ P[x])) ⇒ P[t])) ⇒ (∀t:T. (accessible(T;x,y.R[x;y];t) ⇒ P[t])))
BY
{ (Auto
   THEN (InstLemma `param-W-induction` [⌜T⌝;⌜λ2t.Unit⌝;⌜λ2t a.x:T × R[x;t]⌝;⌜so_lambda(t,a,b.fst(b))⌝;⌜λ2t w.P[t]⌝]⋅
         THENA Auto
         )
   THEN All (Fold `accessible`)) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. [P] : T ⟶ ℙ
4. ∀t:T. ((∀x:T. (R[x;t] ⇒ P[x])) ⇒ P[t])@i
5. t : T@i
6. accessible(T;x,y.R[x;y];t)@i
7. par : T@i
8. a : Unit@i
9. f : b:(x:T × R[x;par]) ⟶ accessible(T;x,y.R[x;y];fst(b))@i
10. ∀b:x:T × R[x;par]. P[fst(b)]@i
⊢ P[par]

2
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. [P] : T ⟶ ℙ
4. ∀t:T. ((∀x:T. (R[x;t] ⇒ P[x])) ⇒ P[t])@i
5. t : T@i
6. accessible(T;x,y.R[x;y];t)@i
7. ∀par:T. ∀w:accessible(T;x,y.R[x;y];par).  P[par]
⊢ P[t]

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}t:T.  ((\mforall{}x:T.  (R[x;t]  {}\mRightarrow{}  P[x]))  {}\mRightarrow{}  P[t]))  {}\mRightarrow{}  (\mforall{}t:T.  (accessible(T;x,y.R[x;y];t)  {}\mRightarrow{}  P[t])))


By

---

Latex:
(Auto
  THEN  (InstLemma  `param-W-induction`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}t.Unit\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}t  a.x:T  \mtimes{}  R[x;t]\mkleeneclose{};\mkleeneopen{}so\_lambda(t,a,b.fst(b))\mkleeneclose{};
              \mkleeneopen{}\mlambda{}\msubtwo{}t  w.P[t]\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  All  (Fold  `accessible`))

---

Home Index