Step
*
1
2
of Lemma
consensus-ts5_wf
.....subterm..... T:t
2:n
1. V : Type
2. A : Id List
3. W : {a:Id| (a ∈ A)} List List
⊢ <<λa.<0, ⊗>, λa.mk_fpf(A;λb.<0, inr ⋅ >)>
, λx,y. consensus-rel-knowledge(V;A;W;x;y)
, λx.∃v:V
∀a:{a:Id| (a ∈ A)}
((Inning(fst(x);a) = 0 ∈ ℤ)
∧ (Estimate(fst(x);a) = 0 : v ∈ i:ℤ fp-> V)
∧ (Knowledge(snd(x);a) = mk_fpf(A;λb.<0, inr ⋅ >) ∈ b:Id fp-> ℤ × (ℤ × V + Top)))>
∈ init:ConsensusState × Knowledge(ConsensusState)
× R:(ConsensusState × Knowledge(ConsensusState)) ─→ (ConsensusState × Knowledge(ConsensusState)) ─→ ℙ
× ({s:ConsensusState × Knowledge(ConsensusState)| init (R^*) s} ─→ ℙ)
BY
{ MemCD }
1
.....subterm..... T:t
1:n
1. V : Type
2. A : Id List
3. W : {a:Id| (a ∈ A)} List List
⊢ <λa.<0, ⊗>, λa.mk_fpf(A;λb.<0, inr ⋅ >)> ∈ ConsensusState × Knowledge(ConsensusState)
2
.....subterm..... T:t
2:n
1. V : Type
2. A : Id List
3. W : {a:Id| (a ∈ A)} List List
⊢ <λx,y. consensus-rel-knowledge(V;A;W;x;y)
, λx.∃v:V
∀a:{a:Id| (a ∈ A)}
((Inning(fst(x);a) = 0 ∈ ℤ)
∧ (Estimate(fst(x);a) = 0 : v ∈ i:ℤ fp-> V)
∧ (Knowledge(snd(x);a) = mk_fpf(A;λb.<0, inr ⋅ >) ∈ b:Id fp-> ℤ × (ℤ × V + Top)))
> ∈ R:(ConsensusState × Knowledge(ConsensusState)) ─→ (ConsensusState × Knowledge(ConsensusState)) ─→ ℙ
× ({s:ConsensusState × Knowledge(ConsensusState)| <λa.<0, ⊗>, λa.mk_fpf(A;λb.<0, inr ⋅ >)> (R^*) s} ─→ ℙ)
3
.....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} ─→ ℙ) ∈ 𝕌'
Latex:
.....subterm..... T:t
2:n
1. V : Type
2. A : Id List
3. W : \{a:Id| (a \mmember{} A)\} List List
\mvdash{} <<\mlambda{}a.ɘ, \motimes{}>, \mlambda{}a.mk\_fpf(A;\mlambda{}b.ɘ, inr \mcdot{} >)>
, \mlambda{}x,y. consensus-rel-knowledge(V;A;W;x;y)
, \mlambda{}x.\mexists{}v:V
\mforall{}a:\{a:Id| (a \mmember{} A)\}
((Inning(fst(x);a) = 0)
\mwedge{} (Estimate(fst(x);a) = 0 : v)
\mwedge{} (Knowledge(snd(x);a) = mk\_fpf(A;\mlambda{}b.ɘ, inr \mcdot{} >)))>
\mmember{} init:ConsensusState \mtimes{} Knowledge(ConsensusState)
\mtimes{} R:(ConsensusState \mtimes{} Knowledge(ConsensusState))
{}\mrightarrow{} (ConsensusState \mtimes{} Knowledge(ConsensusState))
{}\mrightarrow{} \mBbbP{}
\mtimes{} (\{s:ConsensusState \mtimes{} Knowledge(ConsensusState)|
init (R\^{}*) s\} {}\mrightarrow{} \mBbbP{})
By
MemCD
Home
Index