---

Step * 1 2 of Lemma wfd-tree-induction


1. [A] : Type
2. [P] : wfd-tree(A) ⟶ ℙ
3. P[w-nil()]
4. ∀f:A ⟶ wfd-tree(A). ((∀a:A. P[f a]) ⇒ P[mk-wfd-tree(f)])
5. w : wfd-tree(A)
6. s : {s:A List| ¬↑co-w-null(w@s)} 
7. ∀t:A. P[w@s @ [t]]
⊢ P[w@s]
BY
{ xxx(xxx(Assert ⌜∀s:A List. ∀w:wfd-tree(A).  (∀t:A. P[w@s @ [t]]) ⇒ P[w@s] supposing ¬↑co-w-null(w@s)⌝⋅
          THEN Try ((BHyp (-1) THEN Auto))
          )xxx
      THEN RepeatFor 3 (Thin (-1))
      THEN InductionOnListA
      THEN Auto
      THEN Try ((BLemma `co-w-select-wfd` THEN Auto)))xxx }

1
1. [A] : Type
2. [P] : wfd-tree(A) ⟶ ℙ
3. P[w-nil()]
4. ∀f:A ⟶ wfd-tree(A). ((∀a:A. P[f a]) ⇒ P[mk-wfd-tree(f)])
5. w : wfd-tree(A)
6. ¬↑co-w-null(w@[])
7. ∀t:A. P[w@[] @ [t]]
⊢ P[w@[]]

2
1. [A] : Type
2. [P] : wfd-tree(A) ⟶ ℙ
3. P[w-nil()]
4. ∀f:A ⟶ wfd-tree(A). ((∀a:A. P[f a]) ⇒ P[mk-wfd-tree(f)])
5. s : A
6. s1 : A List
7. ∀w:wfd-tree(A). (∀t:A. P[w@s1 @ [t]]) ⇒ P[w@s1] supposing ¬↑co-w-null(w@s1)
8. w : wfd-tree(A)
9. ¬↑co-w-null(w@[s / s1])
10. ∀t:A. P[w@[s / s1] @ [t]]
⊢ P[w@[s / s1]]

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [P]  :  wfd-tree(A)  {}\mrightarrow{}  \mBbbP{}
3.  P[w-nil()]
4.  \mforall{}f:A  {}\mrightarrow{}  wfd-tree(A).  ((\mforall{}a:A.  P[f  a])  {}\mRightarrow{}  P[mk-wfd-tree(f)])
5.  w  :  wfd-tree(A)
6.  s  :  \{s:A  List|  \mneg{}\muparrow{}co-w-null(w@s)\} 
7.  \mforall{}t:A.  P[w@s  @  [t]]
\mvdash{}  P[w@s]


By

---

Latex:
xxx(xxx(Assert  \mkleeneopen{}\mforall{}s:A  List.  \mforall{}w:wfd-tree(A).
                                    (\mforall{}t:A.  P[w@s  @  [t]])  {}\mRightarrow{}  P[w@s]  supposing  \mneg{}\muparrow{}co-w-null(w@s)\mkleeneclose{}\mcdot{}
                THEN  Try  ((BHyp  (-1)  THEN  Auto))
                )xxx
        THEN  RepeatFor  3  (Thin  (-1))
        THEN  InductionOnListA
        THEN  Auto
        THEN  Try  ((BLemma  `co-w-select-wfd`  THEN  Auto)))xxx

---

Home Index