---

Step * 4 2 1 of Lemma Veldman-Coquand


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)))
5. f : X ⟶ wfd-tree(X)
6. ∀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)))
7. f1 : X ⟶ wfd-tree(X)
8. ∀b: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));f1 b)
       ⇒ tree-secures(X;λm,s. (((A m s) ∨ (B m s)) ∨ (([[R]] m s) ∧ ([[S]] m s)));tree-tensor(n;Wsup(ff;f);f1 b)))
⊢ ∀[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));Wsup(ff;f1))
    ⇒ tree-secures(X;λm,s. (((A m s) ∨ (B m s)) ∨ (([[R]] m s) ∧ ([[S]] m s)));tree-tensor(n;Wsup(ff;f);Wsup(ff;f1))))
BY
{ (RepeatFor 4 ((OnConcl D THENA Auto))
   THEN OnConcl (RecUnfold_o tree-tensor)
   THEN OnConcl (RepUR_o [ Obid: Wsup]⋅)
   THEN (OnConcl (Subst ⌜(n =z 0) ~ ff⌝)⋅ THENA AutoBoolCase ⌜(n =z 0)⌝⋅)
   THEN OnConcl (RecUnfold_o tree-secures)
   THEN OnConcl Reduce
   THEN RenameVar `p' 5
   THEN RenameVar `q' 7
   THEN Auto) }

1
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)))
5. p : X ⟶ wfd-tree(X)
6. ∀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));p 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;p b;q)))
7. q : X ⟶ wfd-tree(X)
8. ∀b:X
     ∀[A,B:n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ]. ∀[R,S:n-aryRel(X)].
       (tree-secures(X;λm,s. ((A m s) ∨ ([[R]] m s));Wsup(ff;p))
       ⇒ tree-secures(X;λm,s. ((B m s) ∨ ([[S]] m s));q b)
       ⇒ tree-secures(X;λm,s. (((A m s) ∨ (B m s)) ∨ (([[R]] m s) ∧ ([[S]] m s)));tree-tensor(n;Wsup(ff;p);q b)))
9. [A] : n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ
10. [B] : n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ
11. [R] : n-aryRel(X)
12. [S] : n-aryRel(X)
13. ∀x:X. tree-secures(X;λm,s. ((A m s) ∨ ([[R]] m s))[x];p x)
14. ∀x:X. tree-secures(X;λm,s. ((B m s) ∨ ([[S]] m s))[x];q x)
15. x : X
⊢ tree-secures(X;λm,s. (((A m s) ∨ (B m s)) ∨ (([[R]] m s) ∧ ([[S]] m s)))[x];tree-tensor(n - 1;tree-tensor(n;p x;<ff, q\000C>);tree-tensor(n;<ff, p>;q x)))

---

Latex:

---

Latex:

1.  X  :  Type
2.  n  :  \mBbbZ{}
3.  [\%1]  :  0  <  n
4.  \mforall{}p,q:wfd-tree(X).
          \mforall{}[A,B:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  X)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[R,S:n  -  1-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 
                    -  1;p;q)))
5.  f  :  X  {}\mrightarrow{}  wfd-tree(X)
6.  \mforall{}b:X.  \mforall{}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));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(n;f 
                                                                                                                                                                                          b;q)))
7.  f1  :  X  {}\mrightarrow{}  wfd-tree(X)
8.  \mforall{}b: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));Wsup(ff;f))
              {}\mRightarrow{}  tree-secures(X;\mlambda{}m,s.  ((B  m  s)  \mvee{}  ([[S]]  m  s));f1  b)
              {}\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;Wsup(ff;f);f1  b)))
\mvdash{}  \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));Wsup(ff;f))
        {}\mRightarrow{}  tree-secures(X;\mlambda{}m,s.  ((B  m  s)  \mvee{}  ([[S]]  m  s));Wsup(ff;f1))
        {}\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;Wsup(ff;f);Wsup(ff;f1))))


By

---

Latex:
(RepeatFor  4  ((OnConcl  D  THENA  Auto))
  THEN  OnConcl  (RecUnfold\_o  tree-tensor)
  THEN  OnConcl  (RepUR\_o  [  Obid:  Wsup]\mcdot{})
  THEN  (OnConcl  (Subst  \mkleeneopen{}(n  =\msubz{}  0)  \msim{}  ff\mkleeneclose{})\mcdot{}  THENA  AutoBoolCase  \mkleeneopen{}(n  =\msubz{}  0)\mkleeneclose{}\mcdot{})
  THEN  OnConcl  (RecUnfold\_o  tree-secures)
  THEN  OnConcl  Reduce
  THEN  RenameVar  `p'  5
  THEN  RenameVar  `q'  7
  THEN  Auto)

---

Home Index