Step
*
of Lemma
int_consensus_init_wf
∀[T1,T:Type].  (int_consensus_init() ∈ 𝔹 × ℤ × T List × T1 List × ℤ)
BY
{ ProveWfLemma }
Latex:
\mforall{}[T1,T:Type].    (int\_consensus\_init()  \mmember{}  \mBbbB{}  \mtimes{}  \mBbbZ{}  \mtimes{}  T  List  \mtimes{}  T1  List  \mtimes{}  \mBbbZ{})
By
ProveWfLemma
Home
Index