---

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

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

---

Latex:

---

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


By

---

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

---

Home Index