---

Step * of Lemma tree-tensor_wf

∀[T:Type]. ∀[n:ℕ]. ∀[p,q:wfd-tree(T)].  (tree-tensor(n;p;q) ∈ wfd-tree(T))
BY
{ (Auto
   THEN RepeatFor 3 (MoveToConcl (-1))
   THEN CompleteInductionOnNat
   THEN Unfold `wfd-tree` 0
   THEN RepeatFor 2 (((D 0 THENA Auto) THEN WElim (-1)))
   THEN RecUnfold `tree-tensor` 0
   THEN RepUR ``Wsup`` 0
   THEN Fold `Wsup` 0
   THEN AutoBoolCase ⌜(n =z 0)⌝⋅) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[p,q:wfd-tree(T)].    (tree-tensor(n;p;q)  \mmember{}  wfd-tree(T))


By

---

Latex:
(Auto
  THEN  RepeatFor  3  (MoveToConcl  (-1))
  THEN  CompleteInductionOnNat
  THEN  Unfold  `wfd-tree`  0
  THEN  RepeatFor  2  (((D  0  THENA  Auto)  THEN  WElim  (-1)))
  THEN  RecUnfold  `tree-tensor`  0
  THEN  RepUR  ``Wsup``  0
  THEN  Fold  `Wsup`  0
  THEN  AutoBoolCase  \mkleeneopen{}(n  =\msubz{}  0)\mkleeneclose{}\mcdot{})

---

Home Index