---

Step * 2 3 1 2 2 of Lemma cs-possible-state-reachable


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. u : {a:Id| (a ∈ A)} @i
8. v1 : {a:Id| (a ∈ A)}  List@i
9. ¬(u ∈ v1)
⊢ consensus-rel-knowledge-inning-step(V;A;W;λa.<0, if a ∈b v1 then 0 : v else ⊗ fi >;λa.mk_fpf(A;λb.<0, inr ⋅ >);
            λa.<0, if (IdDeq u a) ∨ba ∈b v1 then 0 : v else ⊗ fi >;λa.mk_fpf(A;λb.<0, inr ⋅ >);u)
∨ consensus-rel-knowledge-archive-step(V;A;W;λa.<0
                                                , if a ∈b v1 then 0 : v else ⊗ fi 
                                                >;λa.mk_fpf(A;λb.<0, inr ⋅ >);λa.<0
                                                                                 , if (IdDeq u a) ∨ba ∈b v1
                                                                                   then 0 : v
                                                                                   else ⊗
                                                                                   fi 
                                                                                 >;λa.mk_fpf(A;λb.<0, inr ⋅ >);u)
∨ consensus-rel-add-knowledge-step(V;A;W;λa.<0
                                            , if a ∈b v1 then 0 : v else ⊗ fi 
                                            >;λa.mk_fpf(A;λb.<0, inr ⋅ >);λa.<0
                                                                             , if (IdDeq u a) ∨ba ∈b v1
                                                                               then 0 : v
                                                                               else ⊗
                                                                               fi 
                                                                             >;λa.mk_fpf(A;λb.<0, inr ⋅ >);u)
BY
{ ((Sel 2 (D 0) THENA (Auto THEN RepUR ``consensus-state4 consensus-state5`` 0 THEN Auto))
   THEN D 0
   THEN RepUR ``cs-inning cs-estimate cs-knowledge cs-possible-state`` 0
   THEN DVar `u') }

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. u : Id@i
8. [%6] : (u ∈ A)@i
9. v1 : {a:Id| (a ∈ A)}  List@i
10. ¬(u ∈ v1)
⊢ (0 = 0 ∈ ℤ) ∧ (mk_fpf(A;λb.<0, inr ⋅ >) = mk_fpf(A;λb.<0, inr ⋅ >) ∈ b:Id fp-> ℤ × (ℤ × V + Top))

2
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. u : Id@i
8. [%6] : (u ∈ A)@i
9. v1 : {a:Id| (a ∈ A)}  List@i
10. ¬(u ∈ v1)
⊢ (¬(0 ∈ fpf-domain(if u ∈b v1 then 0 : v else ⊗ fi )))
∧ (∃v@0:V
    (may consider v@0 in inning 0 based on knowledge (mk_fpf(A;λb.<0, inr ⋅ >))
    ∧ (if (IdDeq u u) ∨bu ∈b v1 then 0 : v else ⊗ fi  = if u ∈b v1 then 0 : v else ⊗ fi  ⊕ 0 : v@0 ∈ i:ℤ fp-> V)))

---

Latex:

---

Latex:

1.  V  :  Type
2.  A  :  Id  List
3.  W  :  \{a:Id|  (a  \mmember{}  A)\}    List  List
4.  v  :  V
5.  1  <  ||W||
6.  two-intersection(A;W)
7.  u  :  \{a:Id|  (a  \mmember{}  A)\}  @i
8.  v1  :  \{a:Id|  (a  \mmember{}  A)\}    List@i
9.  \mneg{}(u  \mmember{}  v1)
\mvdash{}  consensus-rel-knowledge-inning-step(
                        V;A;W;\mlambda{}a.ɘ,  if  a  \mmember{}\msubb{}  v1  then  0  :  v  else  \motimes{}  fi  >\mlambda{}a.mk\_fpf(A;\mlambda{}b.ɘ,  inr  \mcdot{}  >);
                        \mlambda{}a.ɘ,  if  (IdDeq  u  a)  \mvee{}\msubb{}a  \mmember{}\msubb{}  v1  then  0  :  v  else  \motimes{}  fi  >\mlambda{}a.mk\_fpf(A;\mlambda{}b.ɘ,  inr  \mcdot{}  >);u)
\mvee{}  consensus-rel-knowledge-archive-step(V;A;W;\mlambda{}a.ɘ
                                                                                                ,  if  a  \mmember{}\msubb{}  v1  then  0  :  v  else  \motimes{}  fi 
                                                                                                >\mlambda{}a.mk\_fpf(A;
                                                                                                                        \mlambda{}b.ɘ
                                                                                                                              ,  inr  \mcdot{} 
                                                                                                                              >);\mlambda{}a.ɘ
                                                                                                                                          ,  if  (IdDeq  u  a)  \mvee{}\msubb{}a  \mmember{}\msubb{}  v1
                                                                                                                                              then  0  :  v
                                                                                                                                              else  \motimes{}
                                                                                                                                              fi 
                                                                                                                                          >\mlambda{}a.mk\_fpf(A;
                                                                                                                                                                  \mlambda{}b.ɘ,  inr  \mcdot{}  >);u)
\mvee{}  consensus-rel-add-knowledge-step(V;A;W;\mlambda{}a.ɘ
                                                                                        ,  if  a  \mmember{}\msubb{}  v1  then  0  :  v  else  \motimes{}  fi 
                                                                                        >\mlambda{}a.mk\_fpf(A;\mlambda{}b.ɘ,  inr  \mcdot{}  >);\mlambda{}a.ɘ
                                                                                                                                                          ,  if  (IdDeq  u  a)
                                                                                                                                                                    \mvee{}\msubb{}a  \mmember{}\msubb{}  v1
                                                                                                                                                              then  0  :  v
                                                                                                                                                              else  \motimes{}
                                                                                                                                                              fi 
                                                                                                                                                          >\mlambda{}a.mk\_fpf(A;
                                                                                                                                                                                  \mlambda{}b.ɘ
                                                                                                                                                                                        ,  inr  \mcdot{} 
                                                                                                                                                                                        >);u)


By

---

Latex:
((Sel  2  (D  0)  THENA  (Auto  THEN  RepUR  ``consensus-state4  consensus-state5``  0  THEN  Auto))
  THEN  D  0
  THEN  RepUR  ``cs-inning  cs-estimate  cs-knowledge  cs-possible-state``  0
  THEN  DVar  `u')

---

Home Index