---

Step * 2 of Lemma Veldman-Coquand


1. X : Type
⊢ ∀f:X ⟶ wfd-tree(X)
    ((∀b:X. ∀q:wfd-tree(X).
        ∀[A,B:n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ]. ∀[R,S:0-aryRel(X)].
          (tree-secures(X;λm,s. ((A m s) ∨ ([[R]] m s));f b)
          ⇒ tree-secures(X;λm,s. ((B m s) ∨ ([[S]] m s));q)
          ⇒ tree-secures(X;λm,s. (((A m s) ∨ (B m s)) ∨ (([[R]] m s) ∧ ([[S]] m s)));tree-tensor(0;f b;q))))
    ⇒ (∀q:wfd-tree(X)
          ∀[A,B:n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ]. ∀[R,S:0-aryRel(X)].
            (tree-secures(X;λm,s. ((A m s) ∨ ([[R]] m s));Wsup(ff;f))
            ⇒ tree-secures(X;λm,s. ((B m s) ∨ ([[S]] m s));q)
            ⇒ tree-secures(X;λm,s. (((A m s) ∨ (B m s)) ∨ (([[R]] m s) ∧ ([[S]] m s)));tree-tensor(0;Wsup(ff;f);q)))))
BY
{ TACTIC:(Auto
          THEN Try ((Unfold `wfd-tree` 0 THEN Auto))
          THEN RepUR ``Wsup`` -2
          THEN RecUnfold `tree-secures` (-2)
          THEN Reduce (-2)
          THEN RecUnfold `tree-tensor` 0
          THEN Reduce 0
          THEN RepUR ``Wsup`` 0
          THEN RecUnfold `tree-secures` 0
          THEN Reduce 0) }

1
1. X : Type
2. f : X ⟶ wfd-tree(X)
3. ∀b:X. ∀q:wfd-tree(X).
     ∀[A,B:n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ]. ∀[R,S:0-aryRel(X)].
       (tree-secures(X;λm,s. ((A m s) ∨ ([[R]] m s));f b)
       ⇒ tree-secures(X;λm,s. ((B m s) ∨ ([[S]] m s));q)
       ⇒ tree-secures(X;λm,s. (((A m s) ∨ (B m s)) ∨ (([[R]] m s) ∧ ([[S]] m s)));tree-tensor(0;f b;q)))
4. q : wfd-tree(X)
5. [A] : n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ
6. [B] : n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ
7. [R] : 0-aryRel(X)
8. [S] : 0-aryRel(X)
9. ∀x:X. tree-secures(X;λm,s. ((A m s) ∨ ([[R]] m s))[x];f x)
10. tree-secures(X;λm,s. ((B m s) ∨ ([[S]] m s));q)
⊢ ∀x:X. tree-secures(X;λm,s. (((A m s) ∨ (B m s)) ∨ (([[R]] m s) ∧ ([[S]] m s)))[x];tree-tensor(0;f x;q))

---

Latex:

---

Latex:

1.  X  :  Type
\mvdash{}  \mforall{}f:X  {}\mrightarrow{}  wfd-tree(X)
        ((\mforall{}b:X.  \mforall{}q:wfd-tree(X).
                \mforall{}[A,B:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  X)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[R,S:0-aryRel(X)].
                    (tree-secures(X;\mlambda{}m,s.  ((A  m  s)  \mvee{}  ([[R]]  m  s));f  b)
                    {}\mRightarrow{}  tree-secures(X;\mlambda{}m,s.  ((B  m  s)  \mvee{}  ([[S]]  m  s));q)
                    {}\mRightarrow{}  tree-secures(X;\mlambda{}m,s.  (((A  m  s)  \mvee{}  (B  m  s))
                                                                  \mvee{}  (([[R]]  m  s)  \mwedge{}  ([[S]]  m  s)));tree-tensor(0;f  b;q))))
        {}\mRightarrow{}  (\mforall{}q:wfd-tree(X)
                    \mforall{}[A,B:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  X)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[R,S:0-aryRel(X)].
                        (tree-secures(X;\mlambda{}m,s.  ((A  m  s)  \mvee{}  ([[R]]  m  s));Wsup(ff;f))
                        {}\mRightarrow{}  tree-secures(X;\mlambda{}m,s.  ((B  m  s)  \mvee{}  ([[S]]  m  s));q)
                        {}\mRightarrow{}  tree-secures(X;\mlambda{}m,s.  (((A  m  s)  \mvee{}  (B  m  s))
                                                                      \mvee{}  (([[R]]  m  s)  \mwedge{}  ([[S]]  m  s)));tree-tensor(0;Wsup(ff;f);q)))))


By

---

Latex:
TACTIC:(Auto
                THEN  Try  ((Unfold  `wfd-tree`  0  THEN  Auto))
                THEN  RepUR  ``Wsup``  -2
                THEN  RecUnfold  `tree-secures`  (-2)
                THEN  Reduce  (-2)
                THEN  RecUnfold  `tree-tensor`  0
                THEN  Reduce  0
                THEN  RepUR  ``Wsup``  0
                THEN  RecUnfold  `tree-secures`  0
                THEN  Reduce  0)

---

Home Index