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