---

Step * 1 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
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)
BY
{ (Reduce (-1)
   THEN (Assert R ∧ S ∈ n-aryRel(T) BY
               (RepUR ``nary-rel prop_and`` 0 THEN Auto))
   THEN With ⌜tree-tensor(n;p;p1)⌝ (D 0)⋅
   THEN Auto
   THEN TreeSecuresFunctionality
   THEN Reduce 0
   THEN Auto
   THEN SplitOrHyps
   THEN Auto
   THEN All (RepUR ``nary-rel-predicate prop_and``)
   THEN Auto) }

---

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
9.  tree-secures(T;\mlambda{}m,s.  ((((\mlambda{}n,s.  False)  m  s)  \mvee{}  ((\mlambda{}n,s.  False)  m  s))
                                              \mvee{}  (([[R]]  m  s)  \mwedge{}  ([[S]]  m  s)));tree-tensor(n;p;p1))
\mvdash{}  almost-full(T;n;R  \mwedge{}  S)


By

---

Latex:
(Reduce  (-1)
  THEN  (Assert  R  \mwedge{}  S  \mmember{}  n-aryRel(T)  BY
                          (RepUR  ``nary-rel  prop\_and``  0  THEN  Auto))
  THEN  With  \mkleeneopen{}tree-tensor(n;p;p1)\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  TreeSecuresFunctionality
  THEN  Reduce  0
  THEN  Auto
  THEN  SplitOrHyps
  THEN  Auto
  THEN  All  (RepUR  ``nary-rel-predicate  prop\_and``)
  THEN  Auto)

---

Home Index