---

Step * of Lemma cs-possible-state-reachable

∀[V:Type]. ∀[A:Id List]. ∀[W:{a:Id| (a ∈ A)}  List List]. ∀[v:V].
  (∀[L:{a:Id| (a ∈ A)}  List]
     (<λa.<0, if a ∈b L) then 0 : v else ⊗ fi >, λa.mk_fpf(A;λb.<0, ff>)>
      ∈ ts-reachable(consensus-ts5(V;A;W)))) supposing 
     (two-intersection(A;W) and 
     1 < ||W||)
BY
{ (Intros THEN Unhide THEN Unfold `ts-reachable` 0 THEN MemTypeCD) }

1
1. V : Type
2. A : Id List
3. W : {a:Id| (a ∈ A)}  List List
4. v : V
5. 1 < ||W||
6. two-intersection(A;W)
7. L : {a:Id| (a ∈ A)}  List
⊢ <λa.<0, if a ∈b L) then 0 : v else ⊗ fi >, λa.mk_fpf(A;λb.<0, ff>)> ∈ ts-type(consensus-ts5(V;A;W))

2
.....set predicate..... 
1. V : Type
2. A : Id List
3. W : {a:Id| (a ∈ A)}  List List
4. v : V
5. 1 < ||W||
6. two-intersection(A;W)
7. L : {a:Id| (a ∈ A)}  List
⊢ ts-init(consensus-ts5(V;A;W)) 
  (ts-rel(consensus-ts5(V;A;W))^*) 
  <λa.<0, if a ∈b L) then 0 : v else ⊗ fi >, λa.mk_fpf(A;λb.<0, ff>)>

3
.....wf..... 
1. V : Type
2. A : Id List
3. W : {a:Id| (a ∈ A)}  List List
4. v : V
5. 1 < ||W||
6. two-intersection(A;W)
7. L : {a:Id| (a ∈ A)}  List
8. s : ts-type(consensus-ts5(V;A;W))
⊢ ts-init(consensus-ts5(V;A;W)) (ts-rel(consensus-ts5(V;A;W))^*) s ∈ Type

---

Latex:


\mforall{}[V:Type].  \mforall{}[A:Id  List].  \mforall{}[W:\{a:Id|  (a  \mmember{}  A)\}    List  List].  \mforall{}[v:V].
    (\mforall{}[L:\{a:Id|  (a  \mmember{}  A)\}    List]
          (<\mlambda{}a.ɘ,  if  a  \mmember{}\msubb{}  L)  then  0  :  v  else  \motimes{}  fi  >,  \mlambda{}a.mk\_fpf(A;\mlambda{}b.ɘ,  ff>)>
            \mmember{}  ts-reachable(consensus-ts5(V;A;W))))  supposing 
          (two-intersection(A;W)  and 
          1  <  ||W||)


By

(Intros  THEN  Unhide  THEN  Unfold  `ts-reachable`  0  THEN  MemTypeCD)

---

Home Index