Step * 1 of Lemma null-mklist


1. n : ℤ
2. f : Top
3. n ≤ 0
⊢ null(mklist(n;f)) ~ tt
BY
{ RepeatFor 2 ((Computation THEN AutoSplit)) }


Latex:


Latex:

1.  n  :  \mBbbZ{}
2.  f  :  Top
3.  n  \mleq{}  0
\mvdash{}  null(mklist(n;f))  \msim{}  tt


By


Latex:
RepeatFor  2  ((Computation  THEN  AutoSplit))




Home Index