---

Step * 1 of Lemma new_23_sig_quorum_state_fun_eq


1. Cmd : {T:Type| valueall-type(T)} @i'
2. notify : Atom List@i
3. propose : Atom List@i
4. f : new_23_sig_headers_type{i:l}(Cmd;notify;propose)@i'
5. (f propose) = (ℤ × Cmd) ∈ Type
6. (f notify) = (ℤ × Cmd) ∈ Type
7. (f ``new_23_sig decided``) = (ℤ × Cmd) ∈ Type
8. (f ``new_23_sig retry``) = (ℤ × ℤ × Cmd) ∈ Type
9. (f ``new_23_sig vote``) = (ℤ × ℤ × Cmd × Id) ∈ Type
10. f ∈ Name ─→ Type
11. es : EO+(Message(f))@i'
12. e : E@i
13. nr : ℤ × ℤ@i
⊢ new_23_sig_QuorumStateFun(Cmd;notify;propose;f;nr;es;e)
= if first(e) then <[], []>
  if pred(e) ∈b new_23_sig_vote'base(Cmd;notify;propose;f)
    then new_23_sig_add_to_quorum(Cmd) nr loc(e) new_23_sig_vote'base(Cmd;notify;propose;f)@pred(e) 
         new_23_sig_QuorumStateFun(Cmd;notify;propose;f;nr;es;pred(e))
  else new_23_sig_QuorumStateFun(Cmd;notify;propose;f;nr;es;pred(e))
  fi 
∈ (Cmd List × (Id List))
BY
{ (RepUR ``new_23_sig_QuorumStateFun new_23_sig_QuorumState memory-class1`` 0
   THEN (RW (AddrC [2] (LemmaC `loop-class-memory-fun-eq`)) 0 THENA (AllReduce THEN Auto))
   THEN Try (Complete (ProveSingleVal))
   THEN Try ((BLemma `loop-class-memory-functional` THEN AllReduce THEN Auto THEN ProveSingleVal))
   THEN Reduce 0
   THEN Fold `classfun-res` 0
   THEN Repeat (AutoSplit)
   THEN Try ((RWO "classfun-res-eclass1" 0 THEN Auto))
   THEN Try ((RWO "es-loc-pred" 0 THENA Auto))
   THEN ProveSingleVal
   THEN Try ((BLemma `loop-class-memory-member` THEN Reduce 0 THEN Auto))
   THEN Try (Complete ((RWO "member-eclass-eclass1" (-1) THEN Auto)))
   THEN Try (Complete ((D (-2) THEN RWO "member-eclass-eclass1" 0 THEN Auto)))
   THEN Try (Complete ((Auto THEN ProveSingleVal THEN BLemma `loop-class-memory-member` THEN Reduce 0 THEN Auto)))) }

---

Latex:

---

Latex:

1.  Cmd  :  \{T:Type|  valueall-type(T)\}  @i'
2.  notify  :  Atom  List@i
3.  propose  :  Atom  List@i
4.  f  :  new\_23\_sig\_headers\_type\{i:l\}(Cmd;notify;propose)@i'
5.  (f  propose)  =  (\mBbbZ{}  \mtimes{}  Cmd)
6.  (f  notify)  =  (\mBbbZ{}  \mtimes{}  Cmd)
7.  (f  ``new\_23\_sig  decided``)  =  (\mBbbZ{}  \mtimes{}  Cmd)
8.  (f  ``new\_23\_sig  retry``)  =  (\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)
9.  (f  ``new\_23\_sig  vote``)  =  (\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)
10.  f  \mmember{}  Name  {}\mrightarrow{}  Type
11.  es  :  EO+(Message(f))@i'
12.  e  :  E@i
13.  nr  :  \mBbbZ{}  \mtimes{}  \mBbbZ{}@i
\mvdash{}  new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;nr;es;e)
=  if  first(e)  then  <[],  []>
    if  pred(e)  \mmember{}\msubb{}  new\_23\_sig\_vote'base(Cmd;notify;propose;f)
        then  new\_23\_sig\_add\_to\_quorum(Cmd)  nr  loc(e)  new\_23\_sig\_vote'base(Cmd;notify;propose;f)@pred(e) 
                  new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;nr;es;pred(e))
    else  new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;nr;es;pred(e))
    fi 


By

---

Latex:
(RepUR  ``new\_23\_sig\_QuorumStateFun  new\_23\_sig\_QuorumState  memory-class1``  0
  THEN  (RW  (AddrC  [2]  (LemmaC  `loop-class-memory-fun-eq`))  0  THENA  (AllReduce  THEN  Auto))
  THEN  Try  (Complete  (ProveSingleVal))
  THEN  Try  ((BLemma  `loop-class-memory-functional`  THEN  AllReduce  THEN  Auto  THEN  ProveSingleVal))
  THEN  Reduce  0
  THEN  Fold  `classfun-res`  0
  THEN  Repeat  (AutoSplit)
  THEN  Try  ((RWO  "classfun-res-eclass1"  0  THEN  Auto))
  THEN  Try  ((RWO  "es-loc-pred"  0  THENA  Auto))
  THEN  ProveSingleVal
  THEN  Try  ((BLemma  `loop-class-memory-member`  THEN  Reduce  0  THEN  Auto))
  THEN  Try  (Complete  ((RWO  "member-eclass-eclass1"  (-1)  THEN  Auto)))
  THEN  Try  (Complete  ((D  (-2)  THEN  RWO  "member-eclass-eclass1"  0  THEN  Auto)))
  THEN  Try  (Complete  ((Auto
                                            THEN  ProveSingleVal
                                            THEN  BLemma  `loop-class-memory-member`
                                            THEN  Reduce  0
                                            THEN  Auto))))

---

Home Index