---

Step * of Lemma last_induction

∀[T:Type]. ∀[Q:(T List) ⟶ ℙ].  (Q[[]] ⇒ (∀ys:T List. ∀y:T.  (Q[ys] ⇒ Q[ys @ [y]])) ⇒ {∀zs:T List. Q[zs]})
BY
{ ((Auto THEN Unfold `guard` 0 THEN InductionOnLength THEN Decide ⌜↑null(zs)⌝⋅) THENA Auto) }

1
1. [T] : Type
2. [Q] : (T List) ⟶ ℙ
3. Q[[]]
4. ∀ys:T List. ∀y:T.  (Q[ys] ⇒ Q[ys @ [y]])
5. n : ℕ
6. zs : T List
7. ∀z1:T List. (||z1|| < ||zs|| ⇒ Q[z1])
8. ↑null(zs)
⊢ Q[zs]

2
1. [T] : Type
2. [Q] : (T List) ⟶ ℙ
3. Q[[]]
4. ∀ys:T List. ∀y:T.  (Q[ys] ⇒ Q[ys @ [y]])
5. n : ℕ
6. zs : T List
7. ∀z1:T List. (||z1|| < ||zs|| ⇒ Q[z1])
8. ¬↑null(zs)
⊢ Q[zs]

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[Q:(T  List)  {}\mrightarrow{}  \mBbbP{}].
    (Q[[]]  {}\mRightarrow{}  (\mforall{}ys:T  List.  \mforall{}y:T.    (Q[ys]  {}\mRightarrow{}  Q[ys  @  [y]]))  {}\mRightarrow{}  \{\mforall{}zs:T  List.  Q[zs]\})


By

---

Latex:
((Auto  THEN  Unfold  `guard`  0  THEN  InductionOnLength  THEN  Decide  \mkleeneopen{}\muparrow{}null(zs)\mkleeneclose{}\mcdot{})  THENA  Auto)

---

Home Index