Step
*
1
1
2
1
1
2
1
1
of Lemma
committed-inning0-reachable
1. V : Type
2. A : Id List
3. W : {a:Id| (a ∈ A)} List List
4. ||W|| ≥ 1
5. v : V
6. u : Id@i
7. v1 : Id List@i
8. (u ∈ A)
9. v1 ⊆ A
10. ¬(u ∈ v1)
11. λa.if u = a ∨ba ∈b v1 then <0, ⊗> else <-1, ⊗> fi ∈ ConsensusState
12. λa.if a ∈b v1 then <0, ⊗> else <-1, ⊗> fi ∈ ConsensusState
⊢ (λa.if a ∈b v1 then <0, ⊗> else <-1, ⊗> fi ) (λx,y. CR[x,y]) (λa.if u = a ∨ba ∈b v1 then <0, ⊗> else <-1, ⊗> fi )
BY
{ (RepUR ``infix_ap consensus-rel cs-inning cs-estimate`` 0⋅ THEN InstConcl [⌜u⌝]⋅)⋅ }
1
.....wf.....
1. V : Type
2. A : Id List
3. W : {a:Id| (a ∈ A)} List List
4. ||W|| ≥ 1
5. v : V
6. u : Id@i
7. v1 : Id List@i
8. (u ∈ A)
9. v1 ⊆ A
10. ¬(u ∈ v1)
11. λa.if u = a ∨ba ∈b v1 then <0, ⊗> else <-1, ⊗> fi ∈ ConsensusState
12. λa.if a ∈b v1 then <0, ⊗> else <-1, ⊗> fi ∈ ConsensusState
⊢ u ∈ {a:Id| (a ∈ A)}
2
1. V : Type
2. A : Id List
3. W : {a:Id| (a ∈ A)} List List
4. ||W|| ≥ 1
5. v : V
6. u : Id@i
7. v1 : Id List@i
8. (u ∈ A)
9. v1 ⊆ A
10. ¬(u ∈ v1)
11. λa.if u = a ∨ba ∈b v1 then <0, ⊗> else <-1, ⊗> fi ∈ ConsensusState
12. λa.if a ∈b v1 then <0, ⊗> else <-1, ⊗> fi ∈ ConsensusState
⊢ (∀b:{a:Id| (a ∈ A)}
((¬(b = u ∈ Id))
⇒ (((fst(if u = b ∨bb ∈b v1 then <0, ⊗> else <-1, ⊗> fi )) = (fst(if b ∈b v1 then <0, ⊗> else <-1, ⊗> fi )) ∈ ℤ)
∧ ((snd(if u = b ∨bb ∈b v1 then <0, ⊗> else <-1, ⊗> fi ))
= (snd(if b ∈b v1 then <0, ⊗> else <-1, ⊗> fi ))
∈ i:ℤ fp-> V))))
∧ ((((fst(if u = u ∨bu ∈b v1 then <0, ⊗> else <-1, ⊗> fi )) = ((fst(if u ∈b v1 then <0, ⊗> else <-1, ⊗> fi )) + 1) ∈ ℤ)
∧ ((snd(if u = u ∨bu ∈b v1 then <0, ⊗> else <-1, ⊗> fi ))
= (snd(if u ∈b v1 then <0, ⊗> else <-1, ⊗> fi ))
∈ i:ℤ fp-> V))
∨ (((fst(if u = u ∨bu ∈b v1 then <0, ⊗> else <-1, ⊗> fi )) = (fst(if u ∈b v1 then <0, ⊗> else <-1, ⊗> fi )) ∈ ℤ)
∧ (¬(fst(if u ∈b v1 then <0, ⊗> else <-1, ⊗> fi ) ∈ fpf-domain(snd(if u ∈b v1 then <0, ⊗> else <-1, ⊗> fi ))))
∧ (∃v:V
(state λa.if a ∈b v1 then <0, ⊗> else <-1, ⊗> fi may consider v in inning fst(if u ∈b v1
then <0, ⊗>
else <-1, ⊗>
fi )
∧ ((snd(if u = u ∨bu ∈b v1 then <0, ⊗> else <-1, ⊗> fi ))
= snd(if u ∈b v1 then <0, ⊗> else <-1, ⊗> fi ) ⊕ fst(if u ∈b v1 then <0, ⊗> else <-1, ⊗> fi ) : v
∈ i:ℤ fp-> V)))))
3
.....wf.....
1. V : Type
2. A : Id List
3. W : {a:Id| (a ∈ A)} List List
4. ||W|| ≥ 1
5. v : V
6. u : Id@i
7. v1 : Id List@i
8. (u ∈ A)
9. v1 ⊆ A
10. ¬(u ∈ v1)
11. λa.if u = a ∨ba ∈b v1 then <0, ⊗> else <-1, ⊗> fi ∈ ConsensusState
12. λa.if a ∈b v1 then <0, ⊗> else <-1, ⊗> fi ∈ ConsensusState
13. a : {a:Id| (a ∈ A)}
⊢ (∀b:{a:Id| (a ∈ A)}
((¬(b = a ∈ Id))
⇒ (((fst(if u = b ∨bb ∈b v1 then <0, ⊗> else <-1, ⊗> fi )) = (fst(if b ∈b v1 then <0, ⊗> else <-1, ⊗> fi )) ∈ ℤ)
∧ ((snd(if u = b ∨bb ∈b v1 then <0, ⊗> else <-1, ⊗> fi ))
= (snd(if b ∈b v1 then <0, ⊗> else <-1, ⊗> fi ))
∈ i:ℤ fp-> V))))
∧ ((((fst(if u = a ∨ba ∈b v1 then <0, ⊗> else <-1, ⊗> fi ))
= ((fst(if a ∈b v1 then <0, ⊗> else <-1, ⊗> fi )) + 1)
∈ ℤ)
∧ ((snd(if u = a ∨ba ∈b v1 then <0, ⊗> else <-1, ⊗> fi ))
= (snd(if a ∈b v1 then <0, ⊗> else <-1, ⊗> fi ))
∈ i:ℤ fp-> V))
∨ (((fst(if u = a ∨ba ∈b v1 then <0, ⊗> else <-1, ⊗> fi )) = (fst(if a ∈b v1 then <0, ⊗> else <-1, ⊗> fi )) ∈ ℤ)
∧ (¬(fst(if a ∈b v1 then <0, ⊗> else <-1, ⊗> fi ) ∈ fpf-domain(snd(if a ∈b v1 then <0, ⊗> else <-1, ⊗> fi ))))
∧ (∃v:V
(state λa.if a ∈b v1 then <0, ⊗> else <-1, ⊗> fi may consider v in inning fst(if a ∈b v1
then <0, ⊗>
else <-1, ⊗>
fi )
∧ ((snd(if u = a ∨ba ∈b v1 then <0, ⊗> else <-1, ⊗> fi ))
= snd(if a ∈b v1 then <0, ⊗> else <-1, ⊗> fi ) ⊕ fst(if a ∈b v1 then <0, ⊗> else <-1, ⊗> fi ) : v
∈ i:ℤ fp-> V))))) ∈ ℙ
Latex:
Latex:
1. V : Type
2. A : Id List
3. W : \{a:Id| (a \mmember{} A)\} List List
4. ||W|| \mgeq{} 1
5. v : V
6. u : Id@i
7. v1 : Id List@i
8. (u \mmember{} A)
9. v1 \msubseteq{} A
10. \mneg{}(u \mmember{} v1)
11. \mlambda{}a.if u = a \mvee{}\msubb{}a \mmember{}\msubb{} v1 then ɘ, \motimes{}> else <-1, \motimes{}> fi \mmember{} ConsensusState
12. \mlambda{}a.if a \mmember{}\msubb{} v1 then ɘ, \motimes{}> else <-1, \motimes{}> fi \mmember{} ConsensusState
\mvdash{} (\mlambda{}a.if a \mmember{}\msubb{} v1 then ɘ, \motimes{}> else <-1, \motimes{}> fi )
(\mlambda{}x,y. CR[x,y])
(\mlambda{}a.if u = a \mvee{}\msubb{}a \mmember{}\msubb{} v1 then ɘ, \motimes{}> else <-1, \motimes{}> fi )
By
Latex:
(RepUR ``infix\_ap consensus-rel cs-inning cs-estimate`` 0\mcdot{} THEN InstConcl [\mkleeneopen{}u\mkleeneclose{}]\mcdot{})\mcdot{}
Home
Index