---

Step * 2 1 of Lemma Veldman-Coquand


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))
BY
{ TACTIC:(ParallelOp -2 THEN (InstHyp [⌜x⌝;⌜q⌝;⌜A[x]⌝;⌜B⌝;⌜R⌝;⌜S⌝] 3⋅ THENA Auto)) }

1
.....antecedent..... 
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)
11. x : X
12. tree-secures(X;λm,s. ((A m s) ∨ ([[R]] m s))[x];f x)
⊢ tree-secures(X;λm,s. ((A[x] m s) ∨ ([[R]] m s));f x)

2
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)
11. x : X
12. tree-secures(X;λm,s. ((A m s) ∨ ([[R]] m s))[x];f x)
13. tree-secures(X;λm,s. (((A[x] m s) ∨ (B m s)) ∨ (([[R]] m s) ∧ ([[S]] m s)));tree-tensor(0;f x;q))
⊢ 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
2.  f  :  X  {}\mrightarrow{}  wfd-tree(X)
3.  \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)))
4.  q  :  wfd-tree(X)
5.  [A]  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  X)  {}\mrightarrow{}  \mBbbP{}
6.  [B]  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  X)  {}\mrightarrow{}  \mBbbP{}
7.  [R]  :  0-aryRel(X)
8.  [S]  :  0-aryRel(X)
9.  \mforall{}x:X.  tree-secures(X;\mlambda{}m,s.  ((A  m  s)  \mvee{}  ([[R]]  m  s))[x];f  x)
10.  tree-secures(X;\mlambda{}m,s.  ((B  m  s)  \mvee{}  ([[S]]  m  s));q)
\mvdash{}  \mforall{}x:X
        tree-secures(X;\mlambda{}m,s.  (((A  m  s)  \mvee{}  (B  m  s))  \mvee{}  (([[R]]  m  s)  \mwedge{}  ([[S]]  m  s)))[x];tree-tensor(0;f  x;q)\000C)


By

---

Latex:
TACTIC:(ParallelOp  -2  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}A[x]\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{};\mkleeneopen{}S\mkleeneclose{}]  3\mcdot{}  THENA  Auto))

---

Home Index