---

Step * 1 of Lemma Veldman-Ramsey


1. T : Type@i'
2. n : ℕ@i
3. [R] : n-aryRel(T)
4. [S] : n-aryRel(T)
5. p : wfd-tree(T)@i
6. tree-secures(T;[[R]];p)@i
7. p1 : wfd-tree(T)@i
8. tree-secures(T;[[S]];p1)@i
⊢ almost-full(T;n;R ∧ S)
BY
{ (InstLemma `Veldman-Coquand` [⌜T⌝;⌜n⌝;⌜p⌝;⌜p1⌝;⌜λn,s. False⌝;⌜λn,s. False⌝;⌜R⌝;⌜S⌝]⋅
   THENA (Auto THEN TreeSecuresFunctionality THEN Reduce 0 THEN Auto)
   ) }

1
1. T : Type@i'
2. n : ℕ@i
3. [R] : n-aryRel(T)
4. [S] : n-aryRel(T)
5. p : wfd-tree(T)@i
6. tree-secures(T;[[R]];p)@i
7. p1 : wfd-tree(T)@i
8. tree-secures(T;[[S]];p1)@i
9. tree-secures(T;λm,s. ((((λn,s. False) m s) ∨ ((λn,s. False) m s)) ∨ (([[R]] m s) ∧ ([[S]] m s)));tree-tensor(n;p;p1))
⊢ almost-full(T;n;R ∧ S)

---

Latex:

---

Latex:

1.  T  :  Type@i'
2.  n  :  \mBbbN{}@i
3.  [R]  :  n-aryRel(T)
4.  [S]  :  n-aryRel(T)
5.  p  :  wfd-tree(T)@i
6.  tree-secures(T;[[R]];p)@i
7.  p1  :  wfd-tree(T)@i
8.  tree-secures(T;[[S]];p1)@i
\mvdash{}  almost-full(T;n;R  \mwedge{}  S)


By

---

Latex:
(InstLemma  `Veldman-Coquand`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}p1\mkleeneclose{};\mkleeneopen{}\mlambda{}n,s.  False\mkleeneclose{};\mkleeneopen{}\mlambda{}n,s.  False\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{};\mkleeneopen{}S\mkleeneclose{}]\mcdot{}
  THENA  (Auto  THEN  TreeSecuresFunctionality  THEN  Reduce  0  THEN  Auto)
  )

---

Home Index