---

Step * of Lemma rat-cube-face-decider_wf

∀k:ℕ. ∀c,d:ℚCube(k).  (rat-cube-face-decider(k;c;d) ∈ Dec(c ≤ d))
BY
{ (Auto
   THEN (Subst' rat-cube-face-decider(k;c;d) ~ TERMOF{decidable__rat-cube-face-ext:o, \\v:l} k c d 0 THENA Computation)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}c,d:\mBbbQ{}Cube(k).    (rat-cube-face-decider(k;c;d)  \mmember{}  Dec(c  \mleq{}  d))


By

---

Latex:
(Auto
  THEN  (Subst'  rat-cube-face-decider(k;c;d)  \msim{}  TERMOF\{decidable\_\_rat-cube-face-ext:o,  \mbackslash{}\mbackslash{}v:l\}  k  c  d  0
              THENA  Computation
              )
  THEN  Auto)

---

Home Index