---

Step * 1 2 2 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. a : A
6. L : A List
7. ∀w:wfd-tree(A). (∀t:A. P[w@L @ [t]]) ⇒ P[w@L] supposing ¬↑co-w-null(w@L)
8. w : wfd-tree(A)
9. ¬↑co-w-null(w@[a / L])
10. ∀t:A. P[w@[a / L] @ [t]]
11. w@[a / L] ~ wfd-subtrees(w) a@L
⊢ P[w@[a / L]]
BY
{ xxx(Assert co-w-null(w) ~ ff BY
            ((InstLemma `wfd-tree-cases` [⌜A⌝;⌜w⌝]⋅ THENA Auto)
             THEN D -1
             THEN Auto
             THEN D (-4)
             THEN RecUnfold `co-w-select` 0
             THEN Reduce 0
             THEN Fold `co-w-null` 0
             THEN AutoSplit
             THEN RWO "assert-co-w-null" (-4)
             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. a : A
6. L : A List
7. ∀w:wfd-tree(A). (∀t:A. P[w@L @ [t]]) ⇒ P[w@L] supposing ¬↑co-w-null(w@L)
8. w : wfd-tree(A)
9. ¬↑co-w-null(w@[a / L])
10. ∀t:A. P[w@[a / L] @ [t]]
11. w@[a / L] ~ wfd-subtrees(w) a@L
12. co-w-null(w) ~ ff
⊢ P[w@[a / L]]

---

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.  a  :  A
6.  L  :  A  List
7.  \mforall{}w:wfd-tree(A).  (\mforall{}t:A.  P[w@L  @  [t]])  {}\mRightarrow{}  P[w@L]  supposing  \mneg{}\muparrow{}co-w-null(w@L)
8.  w  :  wfd-tree(A)
9.  \mneg{}\muparrow{}co-w-null(w@[a  /  L])
10.  \mforall{}t:A.  P[w@[a  /  L]  @  [t]]
11.  w@[a  /  L]  \msim{}  wfd-subtrees(w)  a@L
\mvdash{}  P[w@[a  /  L]]


By

---

Latex:
xxx(Assert  co-w-null(w)  \msim{}  ff  BY
                    ((InstLemma  `wfd-tree-cases`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}w\mkleeneclose{}]\mcdot{}  THENA  Auto)
                      THEN  D  -1
                      THEN  Auto
                      THEN  D  (-4)
                      THEN  RecUnfold  `co-w-select`  0
                      THEN  Reduce  0
                      THEN  Fold  `co-w-null`  0
                      THEN  AutoSplit
                      THEN  RWO  "assert-co-w-null"  (-4)
                      THEN  Auto))xxx

---

Home Index