---

Step * of Lemma nc-e-comp-nc-0

∀[I:fset(ℕ)]. ∀[i,j:{j:ℕ| ¬j ∈ I} ].  ((i0) = e(i;j) ⋅ (j0) ∈ I ⟶ I+i)
BY
{ (InstLemma `nc-e-comp-nc-p` []
   THEN RepeatFor 3 (ParallelLast')
   THEN InstHyp [⌜0⌝] (-1)⋅
   THEN Auto
   THEN RWO "nc-0-as-nc-p<" (-1)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[i,j:\{j:\mBbbN{}|  \mneg{}j  \mmember{}  I\}  ].    ((i0)  =  e(i;j)  \mcdot{}  (j0))


By

---

Latex:
(InstLemma  `nc-e-comp-nc-p`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  (-1)\mcdot{}
  THEN  Auto
  THEN  RWO  "nc-0-as-nc-p<"  (-1)
  THEN  Auto)

---

Home Index