---

Step * of Lemma tree-secures_functionality

∀T:Type. ∀p:wfd-tree(T).
  ∀[A,B:n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ].
    ((∀n:ℕ. ∀s:ℕn ⟶ T.  ((A n s) ⇒ (B n s))) ⇒ tree-secures(T;A;p) ⇒ tree-secures(T;B;p))
BY
{ (((D 0 THENA Auto) THEN (BLemma `wfd-tree-induction`⋅ THENA Auto)) THEN Auto) }

1
1. T : Type@i'
2. [A] : n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ
3. [B] : n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ
4. ∀n:ℕ. ∀s:ℕn ⟶ T.  ((A n s) ⇒ (B n s))@i
5. tree-secures(T;A;Wsup(tt;⋅))@i
⊢ tree-secures(T;B;Wsup(tt;⋅))

2
1. T : Type@i'
2. A : n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ
3. B : n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ
4. ∀n:ℕ. ∀s:ℕn ⟶ T.  ((A n s) ⇒ (B n s))@i
⊢ Wsup(tt;⋅) ∈ wfd-tree(T)

3
1. T : Type@i'
2. f : T ⟶ wfd-tree(T)@i
3. ∀b:T
     ∀[A,B:n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ].
       ((∀n:ℕ. ∀s:ℕn ⟶ T.  ((A n s) ⇒ (B n s))) ⇒ tree-secures(T;A;f b) ⇒ tree-secures(T;B;f b))@i'
4. [A] : n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ
5. [B] : n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ
6. ∀n:ℕ. ∀s:ℕn ⟶ T.  ((A n s) ⇒ (B n s))@i
7. tree-secures(T;A;Wsup(ff;f))@i
⊢ tree-secures(T;B;Wsup(ff;f))

4
1. T : Type@i'
2. f : T ⟶ wfd-tree(T)@i
3. ∀b:T
     ∀[A,B:n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ].
       ((∀n:ℕ. ∀s:ℕn ⟶ T.  ((A n s) ⇒ (B n s))) ⇒ tree-secures(T;A;f b) ⇒ tree-secures(T;B;f b))@i'
4. A : n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ
5. B : n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ
6. ∀n:ℕ. ∀s:ℕn ⟶ T.  ((A n s) ⇒ (B n s))@i
⊢ Wsup(ff;f) ∈ wfd-tree(T)

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}p:wfd-tree(T).
    \mforall{}[A,B:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbP{}].
        ((\mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  T.    ((A  n  s)  {}\mRightarrow{}  (B  n  s)))  {}\mRightarrow{}  tree-secures(T;A;p)  {}\mRightarrow{}  tree-secures(T;B;p))


By

---

Latex:
(((D  0  THENA  Auto)  THEN  (BLemma  `wfd-tree-induction`\mcdot{}  THENA  Auto))  THEN  Auto)

---

Home Index