---

Step * 1 of Lemma archive-condition-nil


1. V : Type
2. A : Id List@i
3. t : ℕ@i
4. f : (V List) ─→ V@i
5. n : ℤ@i
6. v : V@i
7. archive-condition(V;A;t;f;n;v;[])@i
⊢ False
BY
{ ((D -1 THEN ExRepD) THEN D -4 THEN All Reduce⋅ THEN AutoSimpHyp Auto (-2)) }

---

Latex:



1.  V  :  Type
2.  A  :  Id  List@i
3.  t  :  \mBbbN{}@i
4.  f  :  (V  List)  {}\mrightarrow{}  V@i
5.  n  :  \mBbbZ{}@i
6.  v  :  V@i
7.  archive-condition(V;A;t;f;n;v;[])@i
\mvdash{}  False


By

((D  -1  THEN  ExRepD)  THEN  D  -4  THEN  All  Reduce\mcdot{}  THEN  AutoSimpHyp  Auto  (-2))

---

Home Index