Step
*
1
2
3
of Lemma
consensus-ts5_wf
.....eq aux.....
1. V : Type
2. A : Id List
3. W : {a:Id| (a ∈ A)} List List
4. init : ConsensusState × Knowledge(ConsensusState)
⊢ R:(ConsensusState × Knowledge(ConsensusState)) ─→ (ConsensusState × Knowledge(ConsensusState)) ─→ ℙ
× ({s:ConsensusState × Knowledge(ConsensusState)| init (R^*) s} ─→ ℙ) ∈ 𝕌'
BY
{ Auto }
Latex:
.....eq aux.....
1. V : Type
2. A : Id List
3. W : \{a:Id| (a \mmember{} A)\} List List
4. init : ConsensusState \mtimes{} Knowledge(ConsensusState)
\mvdash{} R:(ConsensusState \mtimes{} Knowledge(ConsensusState))
{}\mrightarrow{} (ConsensusState \mtimes{} Knowledge(ConsensusState))
{}\mrightarrow{} \mBbbP{} \mtimes{} (\{s:ConsensusState \mtimes{} Knowledge(ConsensusState)|
init (R\^{}*) s\} {}\mrightarrow{} \mBbbP{}) \mmember{} \mBbbU{}'
By
Auto
Home
Index