Step
*
of Lemma
archive-condition-single
∀[V:Type]. ∀[A:Id List]. ∀[t:ℕ+]. ∀[f:(V List) ─→ V]. ∀[L:consensus-rcv(V;A) List]. ∀[n:ℤ]. ∀[v:V].
∀[L1:consensus-rcv(V;A) List]. ∀[v1:V]. (¬archive-condition(V;A;t;f;n;v1;L1)) supposing L1 < L
supposing archive-condition(V;A;t;f;n;v;L)
BY
{ (Auto THEN (D 0 THENA Auto) THEN FLemma `archive-condition-innings` [-1;-5] THEN Auto) }
Latex:
\mforall{}[V:Type]. \mforall{}[A:Id List]. \mforall{}[t:\mBbbN{}\msupplus{}]. \mforall{}[f:(V List) {}\mrightarrow{} V]. \mforall{}[L:consensus-rcv(V;A) List]. \mforall{}[n:\mBbbZ{}]. \mforall{}[v:V].
\mforall{}[L1:consensus-rcv(V;A) List]. \mforall{}[v1:V]. (\mneg{}archive-condition(V;A;t;f;n;v1;L1)) supposing L1 < L
supposing archive-condition(V;A;t;f;n;v;L)
By
(Auto THEN (D 0 THENA Auto) THEN FLemma `archive-condition-innings` [-1;-5] THEN Auto)
Home
Index