Step
*
of Lemma
s-comp-nc-0-new
No Annotations
∀[I:fset(ℕ)]. (s ⋅ (new-name(I)0) = 1 ∈ I ⟶ I)
BY
{ (Auto THEN RWO "s-comp-nc-0" 0 THEN Auto) }
Latex:
Latex:
No  Annotations
\mforall{}[I:fset(\mBbbN{})].  (s  \mcdot{}  (new-name(I)0)  =  1)
By
Latex:
(Auto  THEN  RWO  "s-comp-nc-0"  0  THEN  Auto)
Home
Index