Step * of Lemma s-comp-nc-1

[I:fset(ℕ)]. ∀[i:ℕ].  s ⋅ (i1) 1 ∈ I ⟶ supposing ¬i ∈ I
BY
(InstLemma  `nc-1-as-nc-p` [] THEN RepeatFor (ParallelLast) THEN RWO "-1" THEN EAuto 1) }


Latex:


Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[i:\mBbbN{}].    s  \mcdot{}  (i1)  =  1  supposing  \mneg{}i  \mmember{}  I


By


Latex:
(InstLemma    `nc-1-as-nc-p`  []  THEN  RepeatFor  2  (ParallelLast)  THEN  RWO  "-1"  0  THEN  EAuto  1)




Home Index