---

Step * of Lemma Veldman-Coquand

∀X:Type. ∀n:ℕ. ∀p,q:wfd-tree(X).
  ∀[A,B:n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ]. ∀[R,S:n-aryRel(X)].
    (tree-secures(X;λm,s. ((A m s) ∨ ([[R]] m s));p)
    ⇒ 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(n;p;q)))
BY
{ (InductionOnNat THEN (BLemma `wfd-tree-induction` THENA Auto)) }

1
1. X : Type
⊢ ∀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(tt;⋅))
      ⇒ 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(tt;⋅);q)))

2
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)))))

3
1. X : Type
2. n : ℤ
3. [%1] : 0 < n
4. ∀p,q:wfd-tree(X).
     ∀[A,B:n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ]. ∀[R,S:n - 1-aryRel(X)].
       (tree-secures(X;λm,s. ((A m s) ∨ ([[R]] m s));p)
       ⇒ 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(n - 1;p;q)))
⊢ ∀q:wfd-tree(X)
    ∀[A,B:n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ]. ∀[R,S:n-aryRel(X)].
      (tree-secures(X;λm,s. ((A m s) ∨ ([[R]] m s));Wsup(tt;⋅))
      ⇒ 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(n;Wsup(tt;⋅);q)))

4
1. X : Type
2. n : ℤ
3. [%1] : 0 < n
4. ∀p,q:wfd-tree(X).
     ∀[A,B:n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ]. ∀[R,S:n - 1-aryRel(X)].
       (tree-secures(X;λm,s. ((A m s) ∨ ([[R]] m s));p)
       ⇒ 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(n - 1;p;q)))
⊢ ∀f:X ⟶ wfd-tree(X)
    ((∀b:X. ∀q:wfd-tree(X).
        ∀[A,B:n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ]. ∀[R,S:n-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(n;f b;q))))
    ⇒ (∀q:wfd-tree(X)
          ∀[A,B:n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ]. ∀[R,S:n-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(n;Wsup(ff;f);q)))))

---

Latex:

---

Latex:
\mforall{}X:Type.  \mforall{}n:\mBbbN{}.  \mforall{}p,q:wfd-tree(X).
    \mforall{}[A,B:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  X)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[R,S:n-aryRel(X)].
        (tree-secures(X;\mlambda{}m,s.  ((A  m  s)  \mvee{}  ([[R]]  m  s));p)
        {}\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(n;p;q)))


By

---

Latex:
(InductionOnNat  THEN  (BLemma  `wfd-tree-induction`  THENA  Auto))

---

Home Index