---

Comment: EventML spec properties
exports:                 []
prefix:                  new_23_sig:s
name:                    new-23-sig.esh:s

Comment: ------ new_23_sig - headers ------
⋅

Definition: new_23_sig_headers
new_23_sig_headers(notify;propose) ==
  [``new_23_sig vote``; ``new_23_sig retry``; ``new_23_sig decided``; notify; propose]

Lemma: new_23_sig_headers_wf
∀[notify,propose:Atom List].  (new_23_sig_headers(notify;propose) ∈ Name List)

Definition: new_23_sig_headers_no_rep
new_23_sig_headers_no_rep(notify;propose) ==  no_repeats(Name;new_23_sig_headers(notify;propose))

Lemma: new_23_sig_headers_no_rep_wf
∀[notify,propose:Atom List].  (new_23_sig_headers_no_rep(notify;propose) ∈ ℙ)

Definition: new_23_sig_headers_fun
new_23_sig_headers_fun(Cmd;notify;propose) ==
  λhdr.if name_eq(hdr;``new_23_sig vote``) then ℤ × ℤ × Cmd × Id
       if name_eq(hdr;``new_23_sig retry``) then ℤ × ℤ × Cmd
       if name_eq(hdr;``new_23_sig decided``) then ℤ × Cmd
       if name_eq(hdr;notify) then ℤ × Cmd
       if name_eq(hdr;propose) then ℤ × Cmd
       else Top
       fi 

Lemma: new_23_sig_headers_fun_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List].  (new_23_sig_headers_fun(Cmd;notify;propose) ∈ Name ─→ Type)

Definition: new_23_sig_headers_type
new_23_sig_headers_type{i:l}(Cmd;notify;propose) ==
  {f:Name ─→ ValueAllType| 
   new_23_sig_headers_no_rep(notify;propose)
   ∧ (∀hdr∈new_23_sig_headers(notify;propose).(f hdr) = (new_23_sig_headers_fun(Cmd;notify;propose) hdr))} 

Lemma: new_23_sig_headers_type_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List].  (new_23_sig_headers_type{i:l}(Cmd;notify;propose) ∈ ℙ')

Comment: ------ new_23_sig - specification ------
⋅

Definition: new_23_sig_vote'base
new_23_sig_vote'base(Cmd;notify;propose;f) ==  Base(``new_23_sig vote``)

Lemma: new_23_sig_vote'base_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_vote'base(Cmd;notify;propose;f) ∈ EClass(ℤ × ℤ × Cmd × Id))

Definition: new_23_sig_vote'base-program
new_23_sig_vote'base-program(Cmd;notify;propose;f) ==  base-class-program(``new_23_sig vote``)

Lemma: new_23_sig_vote'base-program_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_vote'base-program(Cmd;notify;propose;f) ∈ LocalClass(new_23_sig_vote'base(Cmd;notify;propose;f)))

Definition: new_23_sig_vote'broadcast
new_23_sig_vote'broadcast(Cmd;notify;propose;f) ==
  λlocs,z. bag-map(λl.mk-msg-interface(l;make-Msg(``new_23_sig vote``;z));locs)

Lemma: new_23_sig_vote'broadcast_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_vote'broadcast(Cmd;notify;propose;f) ∈ bag(Id) ─→ (ℤ × ℤ × Cmd × Id) ─→ bag(Interface))

Definition: new_23_sig_retry'base
new_23_sig_retry'base(Cmd;notify;propose;f) ==  Base(``new_23_sig retry``)

Lemma: new_23_sig_retry'base_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_retry'base(Cmd;notify;propose;f) ∈ EClass(ℤ × ℤ × Cmd))

Definition: new_23_sig_retry'base-program
new_23_sig_retry'base-program(Cmd;notify;propose;f) ==  base-class-program(``new_23_sig retry``)

Lemma: new_23_sig_retry'base-program_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_retry'base-program(Cmd;notify;propose;f) ∈ LocalClass(new_23_sig_retry'base(Cmd;notify;propose;f)))

Definition: new_23_sig_retry'send
new_23_sig_retry'send(Cmd;notify;propose;f) ==  λl,z. mk-msg-interface(l;make-Msg(``new_23_sig retry``;z))

Lemma: new_23_sig_retry'send_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_retry'send(Cmd;notify;propose;f) ∈ Id ─→ (ℤ × ℤ × Cmd) ─→ Interface)

Definition: new_23_sig_decided'base
new_23_sig_decided'base(Cmd;notify;propose;f) ==  Base(``new_23_sig decided``)

Lemma: new_23_sig_decided'base_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_decided'base(Cmd;notify;propose;f) ∈ EClass(ℤ × Cmd))

Definition: new_23_sig_decided'base-program
new_23_sig_decided'base-program(Cmd;notify;propose;f) ==  base-class-program(``new_23_sig decided``)

Lemma: new_23_sig_decided'base-program_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_decided'base-program(Cmd;notify;propose;f) ∈ LocalClass(new_23_sig_decided'base(Cmd;notify;propose;f)))

Definition: new_23_sig_decided'broadcast
new_23_sig_decided'broadcast(Cmd;notify;propose;f) ==
  λlocs,z. bag-map(λl.mk-msg-interface(l;make-Msg(``new_23_sig decided``;z));locs)

Lemma: new_23_sig_decided'broadcast_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_decided'broadcast(Cmd;notify;propose;f) ∈ bag(Id) ─→ (ℤ × Cmd) ─→ bag(Interface))

Definition: new_23_sig_notify'broadcast
new_23_sig_notify'broadcast(Cmd;notify;propose;f) ==  λlocs,z. bag-map(λl.mk-msg-interface(l;make-Msg(notify;z));locs)

Lemma: new_23_sig_notify'broadcast_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_notify'broadcast(Cmd;notify;propose;f) ∈ bag(Id) ─→ (ℤ × Cmd) ─→ bag(Interface))

Definition: new_23_sig_propose'base
new_23_sig_propose'base(Cmd;notify;propose;f) ==  Base(propose)

Lemma: new_23_sig_propose'base_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_propose'base(Cmd;notify;propose;f) ∈ EClass(ℤ × Cmd))

Definition: new_23_sig_propose'base-program
new_23_sig_propose'base-program(Cmd;notify;propose;f) ==  base-class-program(propose)

Lemma: new_23_sig_propose'base-program_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_propose'base-program(Cmd;notify;propose;f) ∈ LocalClass(new_23_sig_propose'base(Cmd;notify;propose;f)))

Definition: new_23_sig_roundout
new_23_sig_roundout(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ==
  λloc,za,z. let zb,sender = za 
             in let zc,c = zb 
                in let n,i = zc 
                   in let cmds,locs = z 
                      in if (||cmds|| =z coeff * flrs)
                         then let k,x = poss-maj(cmdeq;[c / cmds];c) 
                              in if (k =z (coeff * flrs) + 1)
                                 then new_23_sig_decided'broadcast(Cmd;notify;propose;f) reps <n, x>
                                 else {new_23_sig_retry'send(Cmd;notify;propose;f) loc <<n, i + 1>, x>}
                                 fi 
                         else {}
                         fi 

Lemma: new_23_sig_roundout_wf
∀[Cmd:ValueAllType]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List]. ∀[reps:bag(Id)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_roundout(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ∈ Id
   ─→ (ℤ × ℤ × Cmd × Id)
   ─→ (Cmd List × (Id List))
   ─→ bag(Interface))

Definition: new_23_sig_newvote
new_23_sig_newvote(Cmd) ==
  λni,zd,z. let ze,sender = zd 
            in let ni',c = ze 
               in let cmds,locs = z 
                  in (product-deq(ℤ;ℤ;IntDeq;IntDeq) ni ni') ∧b (¬bsender ∈b locs))

Lemma: new_23_sig_newvote_wf
∀[Cmd:ValueAllType]. (new_23_sig_newvote(Cmd) ∈ (ℤ × ℤ) ─→ (ℤ × ℤ × Cmd × Id) ─→ (Cmd List × (Id List)) ─→ 𝔹)

Definition: new_23_sig_addvote
new_23_sig_addvote(Cmd) ==
  λzf,z. let zg,sender = zf in let ni,c = zg in let cmds,locs = z in <[c / cmds], [sender / locs]>

Lemma: new_23_sig_addvote_wf
∀[Cmd:ValueAllType]. (new_23_sig_addvote(Cmd) ∈ (ℤ × ℤ × Cmd × Id) ─→ (Cmd List × (Id List)) ─→ (Cmd List × (Id List)))

Definition: new_23_sig_add_to_quorum
new_23_sig_add_to_quorum(Cmd) ==
  λni,loc,vt,state. if new_23_sig_newvote(Cmd) ni vt state then new_23_sig_addvote(Cmd) vt state else state fi 

Lemma: new_23_sig_add_to_quorum_wf
∀[Cmd:ValueAllType]
  (new_23_sig_add_to_quorum(Cmd) ∈ (ℤ × ℤ)
   ─→ Id
   ─→ (ℤ × ℤ × Cmd × Id)
   ─→ (Cmd List × (Id List))
   ─→ (Cmd List × (Id List)))

Definition: new_23_sig_when_quorum
new_23_sig_when_quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ==
  λni,loc,vt,state. if new_23_sig_newvote(Cmd) ni vt state
                   then new_23_sig_roundout(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) loc vt state
                   else {}
                   fi 

Lemma: new_23_sig_when_quorum_wf
∀[Cmd:ValueAllType]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List]. ∀[reps:bag(Id)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_when_quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ∈ (ℤ × ℤ)
   ─→ Id
   ─→ (ℤ × ℤ × Cmd × Id)
   ─→ (Cmd List × (Id List))
   ─→ bag(Interface))

Definition: new_23_sig_QuorumState
new_23_sig_QuorumState(Cmd;notify;propose;f) ==
  λni.memory-class1(initially λloc.<[], []>
                    applying new_23_sig_add_to_quorum(Cmd) ni
                    on new_23_sig_vote'base(Cmd;notify;propose;f))

Lemma: new_23_sig_QuorumState_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_QuorumState(Cmd;notify;propose;f) ∈ (ℤ × ℤ) ─→ EClass(Cmd List × (Id List)))

Lemma: new_23_sig_QuorumState-functional
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[x:ℤ × ℤ].
  new_23_sig_QuorumState(Cmd;notify;propose;f) x is functional

Definition: new_23_sig_QuorumStateFun
new_23_sig_QuorumStateFun(Cmd;notify;propose;f;x;es;e) ==  new_23_sig_QuorumState(Cmd;notify;propose;f) x(e)

Lemma: new_23_sig_QuorumStateFun_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[x:ℤ × ℤ].
  (new_23_sig_QuorumStateFun(Cmd;notify;propose;f;x;es;e) ∈ Cmd List × (Id List))

Lemma: new_23_sig_QuorumState-classrel
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  ∀es:EO+(Message(f)). ∀e:E. ∀x:ℤ × ℤ. ∀v:Cmd List × (Id List).
    (v ∈ new_23_sig_QuorumState(Cmd;notify;propose;f) x(e)
    ⇐⇒ v = new_23_sig_QuorumStateFun(Cmd;notify;propose;f;x;es;e))

Definition: new_23_sig_QuorumState-program
new_23_sig_QuorumState-program(Cmd;notify;propose;f) ==
  λni.memory-class1-program(λloc.<[], []>;new_23_sig_add_to_quorum(Cmd) 
                                          ni;new_23_sig_vote'base-program(Cmd;notify;propose;f))

Lemma: new_23_sig_QuorumState-program_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_QuorumState-program(Cmd;notify;propose;f) ∈ ∀x:ℤ × ℤ
                                                            LocalClass(new_23_sig_QuorumState(Cmd;notify;propose;f) x))

Definition: new_23_sig_Quorum
new_23_sig_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ==
  λni.((new_23_sig_when_quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ni o
       new_23_sig_vote'base(Cmd;notify;propose;f)) o new_23_sig_QuorumState(Cmd;notify;propose;f) ni)

Lemma: new_23_sig_Quorum_wf
∀[Cmd:ValueAllType]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List]. ∀[reps:bag(Id)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ∈ (ℤ × ℤ) ─→ EClass(Interface))

Definition: new_23_sig_Quorum-program
new_23_sig_Quorum-program(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ==
  λni.eclass1-program(new_23_sig_when_quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ni;
                      new_23_sig_vote'base-program(Cmd;notify;propose;f))
      o new_23_sig_QuorumState-program(Cmd;notify;propose;f) ni

Lemma: new_23_sig_Quorum-program_wf
∀[Cmd:ValueAllType]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List]. ∀[reps:bag(Id)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_Quorum-program(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f)
   ∈ ∀x:ℤ × ℤ. LocalClass(new_23_sig_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) x))

Lemma: new_23_sig_quorum_invariant
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e1:E. ∀ni:ℤ × ℤ. ∀z:Cmd List × (Id List).
  (z ∈ new_23_sig_QuorumState(Cmd;notify;propose;f) ni(e1)
  ⇒ let cmds,locs = z 
     in no_repeats(Id;locs) ∧ (||locs|| = ||cmds||))

Lemma: new_23_sig_quorum_fseg
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e1,e2:E. ∀ni:ℤ × ℤ. ∀zh,z:Cmd List × (Id List).
  ((e1 <loc e2)
  ⇒ zh ∈ new_23_sig_QuorumState(Cmd;notify;propose;f) ni(e1)
  ⇒ z ∈ new_23_sig_QuorumState(Cmd;notify;propose;f) ni(e2)
  ⇒ let cmds1,locs1 = zh 
     in let cmds2,locs2 = z 
        in fseg(Cmd;cmds1;cmds2) ∧ fseg(Id;locs1;locs2))

Definition: new_23_sig_Round
new_23_sig_Round(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ==
  λz.let ni,c = z 
     in return-loc-bag-class(λloc.(new_23_sig_vote'broadcast(Cmd;notify;propose;f) reps 
                                   <<ni, c>, loc>)) || (new_23_sig_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) 
                                                        ni once)

Lemma: new_23_sig_Round_wf
∀[Cmd:ValueAllType]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List]. ∀[reps:bag(Id)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_Round(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ∈ (ℤ × ℤ × Cmd) ─→ EClass(Interface))

Definition: new_23_sig_Round-program
new_23_sig_Round-program(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ==
  λz.let ni,c = z 
     in return-loc-bag-class-program(λloc.(new_23_sig_vote'broadcast(Cmd;notify;propose;f) reps 
                                           <<ni, c>, loc>))
        || once-class-program(new_23_sig_Quorum-program(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ni)

Lemma: new_23_sig_Round-program_wf
∀[Cmd:ValueAllType]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List]. ∀[reps:bag(Id)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_Round-program(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f)
   ∈ ∀x:ℤ × ℤ × Cmd. LocalClass(new_23_sig_Round(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) x))

Definition: new_23_sig_vote2retry
new_23_sig_vote2retry(Cmd) ==  λloc,z. let z,sender = z in let ni,c = z in {<ni, c>}

Lemma: new_23_sig_vote2retry_wf
∀[Cmd:ValueAllType]. (new_23_sig_vote2retry(Cmd) ∈ Id ─→ (ℤ × ℤ × Cmd × Id) ─→ bag(ℤ × ℤ × Cmd))

Definition: new_23_sig_RoundInfo
new_23_sig_RoundInfo(Cmd;notify;propose;f) ==
  new_23_sig_retry'base(Cmd;notify;propose;f)
  || (new_23_sig_vote2retry(Cmd) o new_23_sig_vote'base(Cmd;notify;propose;f))

Lemma: new_23_sig_RoundInfo_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_RoundInfo(Cmd;notify;propose;f) ∈ EClass(ℤ × ℤ × Cmd))

Definition: new_23_sig_RoundInfo-program
new_23_sig_RoundInfo-program(Cmd;notify;propose;f) ==
  new_23_sig_retry'base-program(Cmd;notify;propose;f)
  || eclass0-program(new_23_sig_vote2retry(Cmd);new_23_sig_vote'base-program(Cmd;notify;propose;f))

Lemma: new_23_sig_RoundInfo-program_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_RoundInfo-program(Cmd;notify;propose;f) ∈ LocalClass(new_23_sig_RoundInfo(Cmd;notify;propose;f)))

Definition: new_23_sig_update_round
new_23_sig_update_round(Cmd) ==
  λn,loc,z,round. let z,c = z in let m,i = z in if (n =z m) ∧b round <z i then i else round fi 

Lemma: new_23_sig_update_round_wf
∀[Cmd:ValueAllType]. (new_23_sig_update_round(Cmd) ∈ ℤ ─→ Id ─→ (ℤ × ℤ × Cmd) ─→ ℤ ─→ ℤ)

Definition: new_23_sig_when_new_round
new_23_sig_when_new_round(Cmd) ==
  λn,loc,z,round. let z,c = z in let m,i = z in if (n =z m) ∧b round <z i then {<<m, i>, c>} else {} fi 

Lemma: new_23_sig_when_new_round_wf
∀[Cmd:ValueAllType]. (new_23_sig_when_new_round(Cmd) ∈ ℤ ─→ Id ─→ (ℤ × ℤ × Cmd) ─→ ℤ ─→ bag(ℤ × ℤ × Cmd))

Definition: new_23_sig_NewRoundsState
new_23_sig_NewRoundsState(Cmd;notify;propose;f) ==
  λn.memory-class1(initially λloc.0
                   applying new_23_sig_update_round(Cmd) n
                   on new_23_sig_RoundInfo(Cmd;notify;propose;f))

Lemma: new_23_sig_NewRoundsState_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_NewRoundsState(Cmd;notify;propose;f) ∈ ℤ ─→ EClass(ℤ))

Lemma: new_23_sig_NewRoundsState-functional
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[x:ℤ].
  new_23_sig_NewRoundsState(Cmd;notify;propose;f) x is functional

Definition: new_23_sig_NewRoundsStateFun
new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;x;es;e) ==  new_23_sig_NewRoundsState(Cmd;notify;propose;f) x(e)

Lemma: new_23_sig_NewRoundsStateFun_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[x:ℤ].
  (new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;x;es;e) ∈ ℤ)

Lemma: new_23_sig_NewRoundsState-classrel
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  ∀es:EO+(Message(f)). ∀e:E. ∀x,v:ℤ.
    (v ∈ new_23_sig_NewRoundsState(Cmd;notify;propose;f) x(e)
    ⇐⇒ v = new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;x;es;e))

Definition: new_23_sig_NewRoundsState-program
new_23_sig_NewRoundsState-program(Cmd;notify;propose;f) ==
  λn.memory-class1-program(λloc.0;new_23_sig_update_round(Cmd) n;new_23_sig_RoundInfo-program(Cmd;notify;propose;f))

Lemma: new_23_sig_NewRoundsState-program_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_NewRoundsState-program(Cmd;notify;propose;f)
   ∈ ∀x:ℤ. LocalClass(new_23_sig_NewRoundsState(Cmd;notify;propose;f) x))

Definition: new_23_sig_NewRounds
new_23_sig_NewRounds(Cmd;notify;propose;f) ==
  λn.((new_23_sig_when_new_round(Cmd) n o new_23_sig_RoundInfo(Cmd;notify;propose;f)) o
     new_23_sig_NewRoundsState(Cmd;notify;propose;f) n)

Lemma: new_23_sig_NewRounds_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_NewRounds(Cmd;notify;propose;f) ∈ ℤ ─→ EClass(ℤ × ℤ × Cmd))

Definition: new_23_sig_NewRounds-program
new_23_sig_NewRounds-program(Cmd;notify;propose;f) ==
  λn.eclass1-program(new_23_sig_when_new_round(Cmd) n;new_23_sig_RoundInfo-program(Cmd;notify;propose;f))
     o new_23_sig_NewRoundsState-program(Cmd;notify;propose;f) n

Lemma: new_23_sig_NewRounds-program_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_NewRounds-program(Cmd;notify;propose;f) ∈ ∀x:ℤ. LocalClass(new_23_sig_NewRounds(Cmd;notify;propose;f) x))

Lemma: new_23_sig_rounds_pos
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e1:E. ∀n,round:ℤ.
  (round ∈ new_23_sig_NewRoundsState(Cmd;notify;propose;f) n(e1) ⇒ (0 ≤ round))

Lemma: new_23_sig_rounds_inc
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e1,e2:E. ∀n,round1,round2:ℤ.
  ((e1 <loc e2)
  ⇒ round1 ∈ new_23_sig_NewRoundsState(Cmd;notify;propose;f) n(e1)
  ⇒ round2 ∈ new_23_sig_NewRoundsState(Cmd;notify;propose;f) n(e2)
  ⇒ (round1 ≤ round2))

Lemma: new_23_sig_rounds_strict_inc
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e1,e2:E. ∀n,round1,round2:ℤ.
  ((∃z:ℤ × ℤ × Cmd
     ∃round:ℤ
      ∃e:E
       (e1 ≤loc e 
       ∧ (e <loc e2)
       ∧ z ∈ new_23_sig_RoundInfo(Cmd;notify;propose;f)(e)
       ∧ round ∈ new_23_sig_NewRoundsState(Cmd;notify;propose;f) n(e)
       ∧ let z,cmd = z 
         in let n',round' = z 
            in (n' = n) ∧ round < round'))
  ⇒ (e1 <loc e2)
  ⇒ round1 ∈ new_23_sig_NewRoundsState(Cmd;notify;propose;f) n(e1)
  ⇒ round2 ∈ new_23_sig_NewRoundsState(Cmd;notify;propose;f) n(e2)
  ⇒ round1 < round2)

Lemma: new_23_sig_rounds_mem
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e1,e2:E. ∀n,round1,round2:ℤ. ∀z:ℤ × ℤ × Cmd.
  ((e1 <loc e2)
  ⇒ z ∈ new_23_sig_RoundInfo(Cmd;notify;propose;f)(e1)
  ⇒ round1 ∈ new_23_sig_NewRoundsState(Cmd;notify;propose;f) n(e1)
  ⇒ round2 ∈ new_23_sig_NewRoundsState(Cmd;notify;propose;f) n(e2)
  ⇒ let z,cmd = z 
     in let n',round' = z 
        in (n = n') ⇒ (round' ≤ round2))

Definition: new_23_sig_decision
new_23_sig_decision(Cmd;clients;notify;propose;f) ==
  λn,loc,z. let m,c = z in if (m =z n) then new_23_sig_notify'broadcast(Cmd;notify;propose;f) clients <m, c> else {} fi 

Lemma: new_23_sig_decision_wf
∀[Cmd:ValueAllType]. ∀[clients:bag(Id)]. ∀[notify,propose:Atom List].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_decision(Cmd;clients;notify;propose;f) ∈ ℤ ─→ Id ─→ (ℤ × Cmd) ─→ bag(Interface))

Definition: new_23_sig_Notify
new_23_sig_Notify(Cmd;clients;notify;propose;f) ==
  λn.((new_23_sig_decision(Cmd;clients;notify;propose;f) n o new_23_sig_decided'base(Cmd;notify;propose;f)) once)

Lemma: new_23_sig_Notify_wf
∀[Cmd:ValueAllType]. ∀[clients:bag(Id)]. ∀[notify,propose:Atom List].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_Notify(Cmd;clients;notify;propose;f) ∈ ℤ ─→ EClass(Interface))

Definition: new_23_sig_Notify-program
new_23_sig_Notify-program(Cmd;clients;notify;propose;f) ==
  λn.once-class-program(eclass0-program(new_23_sig_decision(Cmd;clients;notify;propose;f) n;
                        new_23_sig_decided'base-program(Cmd;notify;propose;f)))

Lemma: new_23_sig_Notify-program_wf
∀[Cmd:ValueAllType]. ∀[clients:bag(Id)]. ∀[notify,propose:Atom List].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_Notify-program(Cmd;clients;notify;propose;f)
   ∈ ∀x:ℤ. LocalClass(new_23_sig_Notify(Cmd;clients;notify;propose;f) x))

Definition: new_23_sig_Rounds
new_23_sig_Rounds(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ==
  λzi.let n,c = zi 
      in new_23_sig_Round(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) 
         <<n, 0>, c> || new_23_sig_NewRounds(Cmd;notify;propose;f) n
                         >z> new_23_sig_Round(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) z

Lemma: new_23_sig_Rounds_wf
∀[Cmd:ValueAllType]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List]. ∀[reps:bag(Id)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_Rounds(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ∈ (ℤ × Cmd) ─→ EClass(Interface))

Definition: new_23_sig_Rounds-program
new_23_sig_Rounds-program(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ==
  λzi.let n,c = zi 
      in new_23_sig_Round-program(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) 
         <<n, 0>, c> || new_23_sig_NewRounds-program(Cmd;notify;propose;f) n
                         >>= λz.(new_23_sig_Round-program(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) z)

Lemma: new_23_sig_Rounds-program_wf
∀[Cmd:ValueAllType]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List]. ∀[reps:bag(Id)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_Rounds-program(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f)
   ∈ ∀x:ℤ × Cmd. LocalClass(new_23_sig_Rounds(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) x))

Definition: new_23_sig_Voter
new_23_sig_Voter(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;f) ==
  λz.let n,c = z 
     in (new_23_sig_Rounds(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) <n, c> until new_23_sig_Notify(Cmd;clients;notify\000C;propose;f) n)
        || new_23_sig_Notify(Cmd;clients;notify;propose;f) n

Lemma: new_23_sig_Voter_wf
∀[Cmd:ValueAllType]. ∀[clients:bag(Id)]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List].
∀[reps:bag(Id)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_Voter(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;f) ∈ (ℤ × Cmd) ─→ EClass(Interface))

Definition: new_23_sig_Voter-program
new_23_sig_Voter-program(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;f) ==
  λz.let n,c = z 
     in until-class-program(new_23_sig_Rounds-program(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) <n, c>;new_23_sig_Noti\000Cfy-program(Cmd;clients;notify;propose;f) n)
        || new_23_sig_Notify-program(Cmd;clients;notify;propose;f) n

Lemma: new_23_sig_Voter-program_wf
∀[Cmd:ValueAllType]. ∀[clients:bag(Id)]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List].
∀[reps:bag(Id)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_Voter-program(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;f)
   ∈ ∀x:ℤ × Cmd. LocalClass(new_23_sig_Voter(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;f) x))

Definition: new_23_sig_vote2prop
new_23_sig_vote2prop(Cmd) ==  λloc,z. let z,loc' = z in let z,c = z in let n,i = z in {<n, c>}

Lemma: new_23_sig_vote2prop_wf
∀[Cmd:ValueAllType]. (new_23_sig_vote2prop(Cmd) ∈ Id ─→ (ℤ × ℤ × Cmd × Id) ─→ bag(ℤ × Cmd))

Definition: new_23_sig_Proposal
new_23_sig_Proposal(Cmd;notify;propose;f) ==
  new_23_sig_propose'base(Cmd;notify;propose;f)
  || (new_23_sig_vote2prop(Cmd) o new_23_sig_vote'base(Cmd;notify;propose;f))

Lemma: new_23_sig_Proposal_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_Proposal(Cmd;notify;propose;f) ∈ EClass(ℤ × Cmd))

Definition: new_23_sig_Proposal-program
new_23_sig_Proposal-program(Cmd;notify;propose;f) ==
  new_23_sig_propose'base-program(Cmd;notify;propose;f)
  || eclass0-program(new_23_sig_vote2prop(Cmd);new_23_sig_vote'base-program(Cmd;notify;propose;f))

Lemma: new_23_sig_Proposal-program_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_Proposal-program(Cmd;notify;propose;f) ∈ LocalClass(new_23_sig_Proposal(Cmd;notify;propose;f)))

Definition: new_23_sig_update_replica
new_23_sig_update_replica(Cmd;slots) ==  λloc,zj,z. let n,c = zj in set-sig-add(slots) n z

Lemma: new_23_sig_update_replica_wf
∀[Cmd:ValueAllType]. ∀[slots:set-sig{i:l}(ℤ)].
  (new_23_sig_update_replica(Cmd;slots) ∈ Id ─→ (ℤ × Cmd) ─→ set-sig-set(slots) ─→ set-sig-set(slots))

Definition: new_23_sig_when_new_proposal
new_23_sig_when_new_proposal(Cmd;slots) ==
  λloc,zk,z. let n,c = zk in if set-sig-member(slots) n z then {} else {<n, c>} fi 

Lemma: new_23_sig_when_new_proposal_wf
∀[Cmd:ValueAllType]. ∀[slots:set-sig{i:l}(ℤ)].
  (new_23_sig_when_new_proposal(Cmd;slots) ∈ Id ─→ (ℤ × Cmd) ─→ set-sig-set(slots) ─→ bag(ℤ × Cmd))

Definition: new_23_sig_ReplicaState
new_23_sig_ReplicaState(Cmd;notify;propose;slots;f) ==
  memory-class1(initially λloc.set-sig-empty(slots)
                applying new_23_sig_update_replica(Cmd;slots)
                on new_23_sig_Proposal(Cmd;notify;propose;f))

Lemma: new_23_sig_ReplicaState_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[slots:set-sig{i:l}(ℤ)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_ReplicaState(Cmd;notify;propose;slots;f) ∈ EClass(set-sig-set(slots)))

Lemma: new_23_sig_ReplicaState-functional
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[slots:set-sig{i:l}(ℤ)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))].
  new_23_sig_ReplicaState(Cmd;notify;propose;slots;f) is functional

Definition: new_23_sig_ReplicaStateFun
new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e) ==  new_23_sig_ReplicaState(Cmd;notify;propose;slots;f)(e)

Lemma: new_23_sig_ReplicaStateFun_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[slots:set-sig{i:l}(ℤ)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))]. ∀[e:E].
  (new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e) ∈ set-sig-set(slots))

Lemma: new_23_sig_ReplicaState-classrel
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[slots:set-sig{i:l}(ℤ)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  ∀es:EO+(Message(f)). ∀e:E. ∀v:set-sig-set(slots).
    (v ∈ new_23_sig_ReplicaState(Cmd;notify;propose;slots;f)(e)
    ⇐⇒ v = new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e))

Definition: new_23_sig_ReplicaState-program
new_23_sig_ReplicaState-program(Cmd;notify;propose;slots;f) ==
  memory-class1-program(λloc.set-sig-empty(slots);new_23_sig_update_replica(Cmd;slots);...)

Lemma: new_23_sig_ReplicaState-program_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[slots:set-sig{i:l}(ℤ)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_ReplicaState-program(Cmd;notify;propose;slots;f)
   ∈ LocalClass(new_23_sig_ReplicaState(Cmd;notify;propose;slots;f)))

Definition: new_23_sig_NewVoters
new_23_sig_NewVoters(Cmd;notify;propose;slots;f) ==
  ((new_23_sig_when_new_proposal(Cmd;slots) o new_23_sig_Proposal(Cmd;notify;propose;f)) o
  new_23_sig_ReplicaState(Cmd;notify;propose;slots;f))

Lemma: new_23_sig_NewVoters_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[slots:set-sig{i:l}(ℤ)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_NewVoters(Cmd;notify;propose;slots;f) ∈ EClass(ℤ × Cmd))

Definition: new_23_sig_NewVoters-program
new_23_sig_NewVoters-program(Cmd;notify;propose;slots;f) ==
  eclass1-program(new_23_sig_when_new_proposal(Cmd;slots);new_23_sig_Proposal-program(Cmd;notify;propose;f))
  o new_23_sig_ReplicaState-program(Cmd;notify;propose;slots;f)

Lemma: new_23_sig_NewVoters-program_wf
∀[Cmd:ValueAllType]. ∀[notify,propose:Atom List]. ∀[slots:set-sig{i:l}(ℤ)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_NewVoters-program(Cmd;notify;propose;slots;f)
   ∈ LocalClass(new_23_sig_NewVoters(Cmd;notify;propose;slots;f)))

Lemma: new_23_sig_increasing_max
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀slots:set-sig{i:l}(ℤ).
∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀slots1,slots2:set-sig-set(slots).
  ((e1 <loc e2)
  ⇒ slots1 ∈ new_23_sig_ReplicaState(Cmd;notify;propose;slots;f)(e1)
  ⇒ slots2 ∈ new_23_sig_ReplicaState(Cmd;notify;propose;slots;f)(e2)
  ⇒ (∀x:ℤ. ((↑(set-sig-member(slots) x slots1)) ⇒ (↑(set-sig-member(slots) x slots2)))))

Lemma: new_23_sig_replica_state_mem
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀slots:set-sig{i:l}(ℤ).
∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀slots1,slots2:set-sig-set(slots).
∀z:ℤ × Cmd.
  ((e1 <loc e2)
  ⇒ z ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e1)
  ⇒ slots1 ∈ new_23_sig_ReplicaState(Cmd;notify;propose;slots;f)(e1)
  ⇒ slots2 ∈ new_23_sig_ReplicaState(Cmd;notify;propose;slots;f)(e2)
  ⇒ let n,cmd = z 
     in ↑(set-sig-member(slots) n slots2))

Definition: new_23_sig_Replica
new_23_sig_Replica(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f) ==
  new_23_sig_NewVoters(Cmd;notify;propose;slots;f)
   >z> new_23_sig_Voter(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;f) z

Lemma: new_23_sig_Replica_wf
∀[Cmd:ValueAllType]. ∀[clients:bag(Id)]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List].
∀[reps:bag(Id)]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_Replica(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f) ∈ EClass(Interface))

Definition: new_23_sig_Replica-program
new_23_sig_Replica-program(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f) ==
  new_23_sig_NewVoters-program(Cmd;notify;propose;slots;f)
   >>= λz.(new_23_sig_Voter-program(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;f) z)

Lemma: new_23_sig_Replica-program_wf
∀[Cmd:ValueAllType]. ∀[clients:bag(Id)]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List].
∀[reps:bag(Id)]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_Replica-program(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f)
   ∈ LocalClass(new_23_sig_Replica(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f)))

Definition: new_23_sig_main
new_23_sig_main() ==  new_23_sig_Replica(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f)@reps

Lemma: new_23_sig_main_wf
∀[Cmd:ValueAllType]. ∀[clients:bag(Id)]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List].
∀[reps:bag(Id)]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_main() ∈ EClass(Interface))

Definition: new_23_sig_main-program
new_23_sig_main-program(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f) ==
  (new_23_sig_Replica-program(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f))@reps

Lemma: new_23_sig_main-program_wf
∀[Cmd:ValueAllType]. ∀[clients:bag(Id)]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List].
∀[reps:bag(Id)]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_main-program(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f) ∈ LocalClass(new_23_sig_main()))

Comment: ------ new_23_sig - extra ------
⋅

Definition: new_23_sig_headers_internal
new_23_sig_headers_internal() ==  [``new_23_sig vote``; ``new_23_sig retry``; ``new_23_sig decided``]

Lemma: new_23_sig_headers_internal_wf
new_23_sig_headers_internal() ∈ Name List

Definition: new_23_sig_headers_no_inputs
new_23_sig_headers_no_inputs(notify) ==  [``new_23_sig vote``; ``new_23_sig retry``; ``new_23_sig decided``; notify]

Lemma: new_23_sig_headers_no_inputs_wf
∀[notify:Atom List]. (new_23_sig_headers_no_inputs(notify) ∈ Name List)

Definition: new_23_sig_headers_no_inputs_types
new_23_sig_headers_no_inputs_types(Cmd;notify) ==
  [<``new_23_sig vote``, ℤ × ℤ × Cmd × Id>; <``new_23_sig retry``, ℤ × ℤ × Cmd>; <``new_23_sig decided``, ℤ × Cmd>; <not\000Cify, ℤ × Cmd>]

Lemma: new_23_sig_headers_no_inputs_types_wf
∀[Cmd:ValueAllType]. ∀[notify:Atom List].  (new_23_sig_headers_no_inputs_types(Cmd;notify) ∈ (Name × Type) List)

Definition: new_23_sig_message-constraint
new_23_sig_message-constraint{i:l}(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f) ==
  msg-interface-constraint{i:l}(new_23_sig_main();new_23_sig_headers_internal();f)

Lemma: new_23_sig_message-constraint_wf
∀[Cmd:ValueAllType]. ∀[clients:bag(Id)]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List].
∀[reps:bag(Id)]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_message-constraint{i:l}(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f) ∈ ℙ')

Definition: new_23_sig_messages-delivered
new_23_sig_messages-delivered{i:l}(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f) ==
  msgs-interface-delivered{i:l}(new_23_sig_main();f)

Lemma: new_23_sig_messages-delivered_wf
∀[Cmd:ValueAllType]. ∀[clients:bag(Id)]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List].
∀[reps:bag(Id)]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
  (new_23_sig_messages-delivered{i:l}(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f) ∈ ℙ')

Lemma: new_23_sig-ilf
(∀[z1:ℤ]. ∀[propose,notify:Atom List]. ∀[clients:bag(Id)]. ∀[Cmd:{T:Type| valueall-type(T)} ].
 ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id]. ∀[m:Message(f)].
   {<d, i, m> ∈ new_23_sig_Notify(Cmd;clients;notify;propose;f) z1(e)
   ⇐⇒ (no (new_23_sig_decision(Cmd;clients;notify;propose;f) 
            z1 o new_23_sig_decided'base(Cmd;notify;propose;f)) prior to e)
       ∧ <d, i, m> ∈
          {(new_23_sig_decision(Cmd;clients;notify;propose;f) z1 o new_23_sig_decided'base(Cmd;notify;propose;f))}(e)})
∧ (∀[z6,z1:ℤ]. ∀[reps:bag(Id)]. ∀[propose,notify:Atom List]. ∀[flrs,coeff:ℤ]. ∀[Cmd:{T:Type| valueall-type(T)} ].
   ∀[cmdeq:EqDecider(Cmd)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))]. ∀[e:E].
   ∀[d:ℤ]. ∀[i:Id]. ∀[m:Message(f)].
     {<d, i, m> ∈ new_23_sig_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) <z1, z6>(e)
     ⇐⇒ ((header(e) = ``new_23_sig vote``) ∧ has-es-info-type(es;e;f;ℤ × ℤ × Cmd × Id))
         ∧ (↑(new_23_sig_newvote(Cmd) <z1, z6> msgval(e) new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es;e)))
         ∧ (||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es;e))|| = (coeff * flrs))
         ∧ (d = 0)
         ∧ (↓(((fst(poss-maj(cmdeq;[snd(fst(msgval(e))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;e\000Cs;e)))];snd(fst(msgval(e)))))) = ((coeff * flrs) + 1))
             ∧ i ↓∈ reps
             ∧ (m
               = make-Msg(``new_23_sig decided``;<fst(fst(fst(msgval(e))))
                                                 , snd(poss-maj(cmdeq;[snd(fst(msgval(e))) / 
                                                                       (fst(new_23_sig_QuorumStateFun(Cmd;...;...;f;<z1
                                                                                                                    , z6
                                                                                                                    >;es\000C;e)))];snd(fst(msgval(e)))))
                                                 >)))
             ∨ ((¬((fst(poss-maj(cmdeq;[snd(fst(msgval(e))) / 
                                        (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es;e)))];snd(fst(ms\000Cgval(e))))))
                = ((coeff * flrs) + 1)))
               ∧ (i = loc(e))
               ∧ (m
                 = make-Msg(``new_23_sig retry``;<<fst(fst(fst(msgval(e)))), (snd(fst(fst(msgval(e))))) + 1>
                                                 , snd(poss-maj(cmdeq;[snd(fst(msgval(e))) / 
                                                                       (fst(new_23_sig_QuorumStateFun(Cmd;...;...;f;<z1
                                                                                                                    , z6
                                                                                                                    >;es\000C;e)))];snd(fst(msgval(e)))))
                                                 >))))})
∧ (∀[z1:ℤ]. ∀[propose,notify:Atom List]. ∀[clients:bag(Id)]. ∀[Cmd:{T:Type| valueall-type(T)} ].
   ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id].
   ∀[m:Message(f)].
     {<d, i, m> ∈
       (new_23_sig_decision(Cmd;clients;notify;propose;f) z1 o new_23_sig_decided'base(Cmd;notify;propose;f))(e)
     ⇐⇒ (header(e) = ``new_23_sig decided``)
         ∧ has-es-info-type(es;e;f;ℤ × Cmd)
         ∧ ((fst(msgval(e))) = z1)
         ∧ i ↓∈ clients
         ∧ (d = 0)
         ∧ (m = make-Msg(notify;msgval(e)))})
∧ (∀[Cmd:{T:Type| valueall-type(T)} ]. ∀[clients:bag(Id)]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ].
   ∀[notify,propose:Atom List]. ∀[reps:bag(Id)]. ∀[slots:set-sig{i:l}(ℤ)].
   ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id].
   ∀[m:Message(f)].
     {<d, i, m> ∈ new_23_sig_main()(e)
     ⇐⇒ loc(e) ↓∈ reps
         ∧ (↓∃e':{e':E| e' ≤loc e } 
              ∃z1:ℤ
               ∃z2:Cmd
                (((((header(e') = propose) ∧ has-es-info-type(es;e';f;ℤ × Cmd) ∧ (<z1, z2> = msgval(e')))
                ∨ ((header(e') = ``new_23_sig vote``)
                  ∧ has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)
                  ∧ (z1 = (fst(fst(fst(msgval(e'))))))
                  ∧ (z2 = (snd(fst(msgval(e')))))))
                ∧ (¬↑(set-sig-member(slots) z1 new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))))
                ∧ (((no new_23_sig_Notify(Cmd;clients;notify;propose;f) z1 between e' and e)
                  ∧ ((((i ↓∈ reps ∧ (d = 0) ∧ (m = make-Msg(``new_23_sig vote``;<<<z1, 0>, z2>, loc(e)>))) ∧ (e = e'))
                    ∨ ((no new_23_sig_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) <z1, 0> between e' and e)
                      ∧ <d, i, m> ∈ {new_23_sig_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) <z1, 0>}(e)))
                    ∨ (∃e1:{e1:E| e1 ≤loc e } 
                        ∃z6:ℤ
                         ∃z7:Cmd
                          (new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;z1;es.e';e1) < z6
                          ∧ (((header(e1) = ``new_23_sig retry``)
                            ∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd)
                            ∧ (<<z1, z6>, z7> = msgval(e1)))
                            ∨ ((header(e1) = ``new_23_sig vote``)
                              ∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd × Id)
                              ∧ (<<z1, z6>, z7> = (fst(msgval(e1))))))
                          ∧ (((i ↓∈ reps ∧ (d = 0) ∧ (m = make-Msg(``new_23_sig vote``;<<<z1, z6>, z7>, loc(e)>))) ∧ (e \000C= e1))
                            ∨ ((no new_23_sig_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ... between ... and
                                ...)
                              ∧ ...))))))
                  ∨ ...)))})

Lemma: new_23_sig-vote
∀[Cmd:{T:Type| valueall-type(T)} ]. ∀[clients:bag(Id)]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ].
∀[notify,propose:Atom List]. ∀[reps:bag(Id)]. ∀[slots:set-sig{i:l}(ℤ)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id]. ∀[auth:𝔹].
∀[k,k1:ℤ]. ∀[v:Cmd]. ∀[i1:Id].
  (<d, i, mk-msg(auth;``new_23_sig vote``;<<<k, k1>, v>, i1>)> ∈ new_23_sig_main()(e)
  ⇐⇒ loc(e) ↓∈ reps
      ∧ (↓∃e':{e':E| e' ≤loc e } 
           ∃z2:Cmd
            (((((header(e') = propose) ∧ has-es-info-type(es;e';f;ℤ × Cmd) ∧ (<k, z2> = msgval(e')))
             ∨ ((header(e') = ``new_23_sig vote``)
               ∧ has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)
               ∧ (k = (fst(fst(fst(msgval(e'))))))
               ∧ (z2 = (snd(fst(msgval(e')))))))
             ∧ (¬↑(set-sig-member(slots) k new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))))
            ∧ (no new_23_sig_Notify(Cmd;clients;notify;propose;f) k between e' and e)
            ∧ i ↓∈ reps
            ∧ (d = 0)
            ∧ auth = ff
            ∧ (i1 = loc(e))
            ∧ (((k1 = 0) ∧ (v = z2) ∧ (e = e'))
              ∨ (new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;k;es.e';e) < k1
                ∧ (((header(e) = ``new_23_sig retry``)
                  ∧ has-es-info-type(es;e;f;ℤ × ℤ × Cmd)
                  ∧ (<<k, k1>, v> = msgval(e)))
                  ∨ ((header(e) = ``new_23_sig vote``)
                    ∧ has-es-info-type(es;e;f;ℤ × ℤ × Cmd × Id)
                    ∧ (<<k, k1>, v> = (fst(msgval(e)))))))))))

Lemma: new_23_sig-retry
∀[Cmd:{T:Type| valueall-type(T)} ]. ∀[clients:bag(Id)]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ].
∀[notify,propose:Atom List]. ∀[reps:bag(Id)]. ∀[slots:set-sig{i:l}(ℤ)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id]. ∀[auth:𝔹].
∀[k,k1:ℤ]. ∀[v:Cmd].
  (<d, i, mk-msg(auth;``new_23_sig retry``;<<k, k1>, v>)> ∈ new_23_sig_main()(e)
  ⇐⇒ loc(e) ↓∈ reps
      ∧ (↓∃e':{e':E| e' ≤loc e } 
           ∃z1:ℤ
            ∃z2:Cmd
             (((((header(e') = propose) ∧ has-es-info-type(es;e';f;ℤ × Cmd) ∧ (<z1, z2> = msgval(e')))
              ∨ ((header(e') = ``new_23_sig vote``)
                ∧ has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)
                ∧ (z1 = (fst(fst(fst(msgval(e'))))))
                ∧ (z2 = (snd(fst(msgval(e')))))))
              ∧ (¬↑(set-sig-member(slots) z1 new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))))
             ∧ (no new_23_sig_Notify(Cmd;clients;notify;propose;f) z1 between e' and e)
             ∧ (((no new_23_sig_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) <z1, 0> between e' and e)
               ∧ ((header(e) = ``new_23_sig vote``) ∧ has-es-info-type(es;e;f;ℤ × ℤ × Cmd × Id))
               ∧ (↑(new_23_sig_newvote(Cmd) <z1, 0> msgval(e) new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.\000Ce';e)))
               ∧ (||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e';e))|| = (coeff * flrs))
               ∧ (d = 0)
               ∧ (¬((fst(poss-maj(cmdeq;[snd(fst(msgval(e))) / 
                                         (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e';e)))];snd(fst\000C(msgval(e))))))
                 = ((coeff * flrs) + 1)))
               ∧ (i = loc(e))
               ∧ auth = ff
               ∧ ((k = (fst(fst(fst(msgval(e)))))) ∧ (k1 = ((snd(fst(fst(msgval(e))))) + 1)))
               ∧ (v
                 = (snd(poss-maj(cmdeq;[snd(fst(msgval(e))) / 
                                        (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e';e)))];snd(fst(\000Cmsgval(e))))))))
               ∨ (∃e1:{e1:E| e1 ≤loc e } 
                   ∃z6:ℤ
                    ∃z7:Cmd
                     (new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;z1;es.e';e1) < z6
                     ∧ (((header(e1) = ``new_23_sig retry``)
                       ∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd)
                       ∧ (<<z1, z6>, z7> = msgval(e1)))
                       ∨ ((header(e1) = ``new_23_sig vote``)
                         ∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd × Id)
                         ∧ (<<z1, z6>, z7> = (fst(msgval(e1))))))
                     ∧ (no new_23_sig_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) <z1, z6> between e1 and e)
                     ∧ ((header(e) = ``new_23_sig vote``) ∧ has-es-info-type(es;e;f;ℤ × ℤ × Cmd × Id))
                     ∧ (↑(new_23_sig_newvote(Cmd) <z1, z6> msgval(e) new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1,\000C z6>;es.e1;e)))
                     ∧ (||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e1;e))|| = (coeff * flrs))
                     ∧ (d = 0)
                     ∧ (¬((fst(poss-maj(cmdeq;[snd(fst(msgval(e))) / 
                                               (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e1;e)))];\000Csnd(fst(msgval(e))))))
                       = ((coeff * flrs) + 1)))
                     ∧ (i = loc(e))
                     ∧ auth = ff
                     ∧ ((k = (fst(fst(fst(msgval(e)))))) ∧ (k1 = ((snd(fst(fst(msgval(e))))) + 1)))
                     ∧ (v
                       = (snd(poss-maj(cmdeq;[snd(fst(msgval(e))) / 
                                              (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e1;e)))];s\000Cnd(fst(msgval(e)))))))))))))

Lemma: new_23_sig-decided
∀[Cmd:{T:Type| valueall-type(T)} ]. ∀[clients:bag(Id)]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ].
∀[notify,propose:Atom List]. ∀[reps:bag(Id)]. ∀[slots:set-sig{i:l}(ℤ)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id]. ∀[auth:𝔹].
∀[k:ℤ]. ∀[v:Cmd].
  (<d, i, mk-msg(auth;``new_23_sig decided``;<k, v>)> ∈ new_23_sig_main()(e)
  ⇐⇒ loc(e) ↓∈ reps
      ∧ (↓∃e':{e':E| e' ≤loc e } 
           ∃z1:ℤ
            ∃z2:Cmd
             (((((header(e') = propose) ∧ has-es-info-type(es;e';f;ℤ × Cmd) ∧ (<z1, z2> = msgval(e')))
              ∨ ((header(e') = ``new_23_sig vote``)
                ∧ has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)
                ∧ (z1 = (fst(fst(fst(msgval(e'))))))
                ∧ (z2 = (snd(fst(msgval(e')))))))
              ∧ (¬↑(set-sig-member(slots) z1 new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))))
             ∧ (no new_23_sig_Notify(Cmd;clients;notify;propose;f) z1 between e' and e)
             ∧ (((no new_23_sig_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) <z1, 0> between e' and e)
               ∧ ((header(e) = ``new_23_sig vote``) ∧ has-es-info-type(es;e;f;ℤ × ℤ × Cmd × Id))
               ∧ (↑(new_23_sig_newvote(Cmd) <z1, 0> msgval(e) new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.\000Ce';e)))
               ∧ (||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e';e))|| = (coeff * flrs))
               ∧ (d = 0)
               ∧ ((fst(poss-maj(cmdeq;[snd(fst(msgval(e))) / (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>\000C;es.e';e)))];snd(fst(msgval(e)))))) = ((coeff * flrs) + 1))
               ∧ i ↓∈ reps
               ∧ auth = ff
               ∧ (k = (fst(fst(fst(msgval(e))))))
               ∧ (v
                 = (snd(poss-maj(cmdeq;[snd(fst(msgval(e))) / 
                                        (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, 0>;es.e';e)))];snd(fst(\000Cmsgval(e))))))))
               ∨ (∃e1:{e1:E| e1 ≤loc e } 
                   ∃z6:ℤ
                    ∃z7:Cmd
                     (new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;z1;es.e';e1) < z6
                     ∧ (((header(e1) = ``new_23_sig retry``)
                       ∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd)
                       ∧ (<<z1, z6>, z7> = msgval(e1)))
                       ∨ ((header(e1) = ``new_23_sig vote``)
                         ∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd × Id)
                         ∧ (<<z1, z6>, z7> = (fst(msgval(e1))))))
                     ∧ (no new_23_sig_Quorum(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) <z1, z6> between e1 and e)
                     ∧ ((header(e) = ``new_23_sig vote``) ∧ has-es-info-type(es;e;f;ℤ × ℤ × Cmd × Id))
                     ∧ (↑(new_23_sig_newvote(Cmd) <z1, z6> msgval(e) new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1,\000C z6>;es.e1;e)))
                     ∧ (||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e1;e))|| = (coeff * flrs))
                     ∧ (d = 0)
                     ∧ ((fst(poss-maj(cmdeq;[snd(fst(msgval(e))) / 
                                             (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e1;e)))];sn\000Cd(fst(msgval(e))))))
                       = ((coeff * flrs) + 1))
                     ∧ i ↓∈ reps
                     ∧ auth = ff
                     ∧ (k = (fst(fst(fst(msgval(e))))))
                     ∧ (v
                       = (snd(poss-maj(cmdeq;[snd(fst(msgval(e))) / 
                                              (fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<z1, z6>;es.e1;e)))];s\000Cnd(fst(msgval(e)))))))))))))

Lemma: new_23_sig-notify
∀[Cmd:{T:Type| valueall-type(T)} ]. ∀[clients:bag(Id)]. ∀[cmdeq:EqDecider(Cmd)]. ∀[coeff,flrs:ℤ].
∀[notify,propose:Atom List]. ∀[reps:bag(Id)]. ∀[slots:set-sig{i:l}(ℤ)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id]. ∀[auth:𝔹].
∀[k:ℤ]. ∀[v:Cmd].
  (<d, i, mk-msg(auth;notify;<k, v>)> ∈ new_23_sig_main()(e)
  ⇐⇒ loc(e) ↓∈ reps
      ∧ (↓∃z2:Cmd
           ∃e':{e':E| e' ≤loc e } 
            ((header(e) = ``new_23_sig decided``)
            ∧ has-es-info-type(es;e;f;ℤ × Cmd)
            ∧ i ↓∈ clients
            ∧ (d = 0)
            ∧ auth = ff
            ∧ (<k, v> = msgval(e))
            ∧ (((header(e') = propose) ∧ has-es-info-type(es;e';f;ℤ × Cmd) ∧ (<fst(msgval(e)), z2> = msgval(e')))
              ∨ ((header(e') = ``new_23_sig vote``)
                ∧ has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)
                ∧ ((fst(msgval(e))) = (fst(fst(fst(msgval(e'))))))
                ∧ (z2 = (snd(fst(msgval(e')))))))
            ∧ (¬↑(set-sig-member(slots) (fst(msgval(e))) new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e')))
            ∧ (no (new_23_sig_decision(Cmd;clients;notify;propose;f) 
                   (fst(msgval(e))) o new_23_sig_decided'base(Cmd;notify;propose;f)) between e' and e))))

Lemma: new_23_sig_replica_state_mem_fun
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀slots:set-sig{i:l}(ℤ).
∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀n:ℤ. ∀c:Cmd.
  ((e1 <loc e2)
  ⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e1)
  ⇒ (↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e2))))

Lemma: new_23_sig_rounds_pos_fun
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e:E. ∀n:ℤ.
  (0 ≤ new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;n;es;e))

Lemma: new_23_sig_rounds_mem_fun
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e1,e2:E. ∀n,round:ℤ. ∀cmd:Cmd.
  ((e1 <loc e2)
  ⇒ <<n, round>, cmd> ∈ new_23_sig_RoundInfo(Cmd;notify;propose;f)(e1)
  ⇒ (round ≤ new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;n;es;e2)))

Lemma: new_23_sig_quorum_invariant_fun
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e:E. ∀ni:ℤ × ℤ.
  (no_repeats(Id;snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e)))
  ∧ (||snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e))||
    = ||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e))||))

Lemma: new_23_sig_quorum_inv_vote
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e:E. ∀ni:ℤ × ℤ. ∀p:Cmd List × (Id List).
  (p ∈ new_23_sig_QuorumState(Cmd;notify;propose;f) ni(e)
  ⇒ let cmds,locs = p 
     in no_repeats(Id;locs)
        ∧ (||locs|| = ||cmds||)
        ∧ (∀i:ℕ||locs||
             (↓∃e':E. ((e' <loc e) ∧ <<ni, cmds[i]>, locs[i]> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e')))))

Lemma: new_23_sig_quorum_inv_vote_fun
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e:E. ∀ni:ℤ × ℤ. ∀i:ℕ||snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e))||.
  (↓∃e':E
     ((e' <loc e)
     ∧ <<ni, fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e))[i]>
       , snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e))[i]
       > ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e')))

Lemma: new_23_sig_quorum_mem
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e1,e2:E. ∀ni:ℤ × ℤ. ∀s1,s2:Cmd List × (Id List). ∀v:ℤ × ℤ × Cmd × Id.
  ((e1 <loc e2)
  ⇒ v ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e1)
  ⇒ s1 ∈ new_23_sig_QuorumState(Cmd;notify;propose;f) ni(e1)
  ⇒ s2 ∈ new_23_sig_QuorumState(Cmd;notify;propose;f) ni(e2)
  ⇒ let cmds1,locs1 = s1 
     in let cmds2,locs2 = s2 
        in let x,i = v 
           in let ni',c = x 
              in (ni = ni') ⇒ ((i ∈ locs2) ∧ ((¬(i ∈ locs1)) ⇒ (c ∈ cmds2))))

Lemma: new_23_sig_quorum_inv_vote2
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e:E. ∀ni:ℤ × ℤ. ∀p:Cmd List × (Id List).
  (p ∈ new_23_sig_QuorumState(Cmd;notify;propose;f) ni(e)
  ⇒ let cmds,locs = p 
     in no_repeats(Id;locs)
        ∧ (||locs|| = ||cmds||)
        ∧ (∀i:ℕ||locs||
             (↓∃e':E
                ((e' <loc e)
                ∧ <<ni, cmds[i]>, locs[i]> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e')
                ∧ (∀e''∈[es-init(es;e);e').∀c:Cmd
                                             (¬<<ni, c>, locs[i]> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(
                                                                    e'')))))))

Lemma: new_23_sig_quorum_inv_vote2_fun
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e:E. ∀ni:ℤ × ℤ.
  (no_repeats(Id;snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e)))
  ∧ (||snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e))||
    = ||fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e))||)
  ∧ (∀i:ℕ||snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e))||
       (↓∃e':E
          ((e' <loc e)
          ∧ <<ni, fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e))[i]>
            , snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e))[i]
            > ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e')
          ∧ (∀e''∈[es-init(es;e);e').∀c:Cmd
                                       (¬<<ni, c>, snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e))[i]> ∈
                                          new_23_sig_vote'base(Cmd;notify;propose;f)(e'')))))))

Lemma: new_23_sig_replica_state_from_proposal
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e:E. ∀slots:set-sig{i:l}(ℤ). ∀s:set-sig-set(slots).
  (s ∈ new_23_sig_ReplicaState(Cmd;notify;propose;slots;f)(e)
  ⇒ (∀n:ℤ
        ((↑(set-sig-member(slots) n s))
        ⇒ (∃e':E
             ∃c:Cmd
              ((e' <loc e)
              ∧ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e')
              ∧ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))))))))

Lemma: new_23_sig_replica_state_from_proposal_fun
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e:E. ∀slots:set-sig{i:l}(ℤ). ∀n:ℤ.
  ((↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
  ⇒ (∃e':E
       ∃c:Cmd
        ((e' <loc e)
        ∧ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e')
        ∧ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))))))

Lemma: new_23_sig_voter_start_unique
∀Cmd:ValueAllType. ∀propose,notify:Atom List. ∀slots:set-sig{i:l}(ℤ).
∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)). ∀n:ℤ. ∀e1,e2:E. ∀c1,c2:Cmd.
  ((¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e1)))
  ⇒ <n, c1> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e1)
  ⇒ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e2)))
  ⇒ <n, c2> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e2)
  ⇒ (loc(e1) = loc(e2))
  ⇒ (e1 = e2))

Lemma: new_23_sig_votes_consistent
∀[Cmd:ValueAllType]. ∀[cmdeq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List].
∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))].
  (new_23_sig_message-constraint{i:l}(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f)
  ⇒ (∀e1,e2:E. ∀n,r:ℤ. ∀sender,l1,l2:Id. ∀c1,c2:Cmd. ∀d1,d2:ℤ.
        (<d1, l1, make-Msg(``new_23_sig vote``;<<<n, r>, c1>, sender>)> ∈ new_23_sig_main()(e1)
        ⇒ <d2, l2, make-Msg(``new_23_sig vote``;<<<n, r>, c2>, sender>)> ∈ new_23_sig_main()(e2)
        ⇒ (c1 = c2))))

Lemma: new_23_sig_assert_newvote
∀[Cmd:ValueAllType]
  ∀ni:ℤ × ℤ. ∀vote:ℤ × ℤ × Cmd × Id. ∀quorum:Cmd List × (Id List).
    (↑(new_23_sig_newvote(Cmd) ni vote quorum) ⇐⇒ (ni = (fst(fst(vote)))) ∧ (¬(snd(vote) ∈ snd(quorum))))

Lemma: new_23_sig_decided_property
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff,flrs:ℤ]. ∀[propose,notify:Atom List].
∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))].
  (new_23_sig_message-constraint{i:l}(Cmd;clients;eq;coeff;flrs;notify;propose;reps;slots;f)
  ⇒ (∀e:E. ∀c:Cmd. ∀n:ℤ.
        (<n, c> ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e)
        ⇒ (↓∃x:Id
              ∃rnd:ℕ
               ∃L:Id List
                (no_repeats(Id;L)
                ∧ (||L|| = ((coeff * flrs) + 1))
                ∧ (∀vtr∈L.↓∃e':E. mk-msg-interface(x;make-Msg(``new_23_sig vote``;<<<n, rnd>, c>, vtr>)) ∈ new_23_sig_ma\000Cin()(e')))))))

Lemma: new_23_sig_retry_property
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff,flrs:ℕ]. ∀[propose,notify:Atom List].
∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))].
  (new_23_sig_message-constraint{i:l}(Cmd;clients;eq;coeff;flrs;notify;propose;reps;slots;f)
  ⇒ (∀e:E. ∀c:Cmd. ∀n,r:ℤ.
        (<<n, r + 1>, c> ∈ new_23_sig_retry'base(Cmd;notify;propose;f)(e)
        ⇒ (↓∃x:Id
              ∃cs:Cmd List+
               ∃L:Id List
                ((no_repeats(Id;L) ∧ (||L|| = ((coeff * flrs) + 1)) ∧ (||cs|| = ||L||))
                ∧ (∀i:ℕ||L||. ((↓∃e':E. mk-msg-interface(x;make-Msg(``new_23_sig vote``;<<<n, r>, cs[i]>, L[i]>)) ∈ new_\000C23_sig_main()(e')) ∧ L[i] ↓∈ reps))
                ∧ (c = (snd(poss-maj(eq;cs;hd(cs))))))))))

Lemma: new_23_sig_proposal_classrel
∀[Cmd:ValueAllType]
  ∀propose:Atom List
    ∀[notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
      ∀es:EO+(Message(f)). ∀e:E.
        ∀[nc:ℤ × Cmd]
          uiff(nc ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e);nc ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e)
          ∨ nc ∈ (new_23_sig_vote2prop(Cmd) o new_23_sig_vote'base(Cmd;notify;propose;f))(e))

Lemma: new_23_sig_proposal_classrel2
∀[Cmd:ValueAllType]
  ∀propose:Atom List
    ∀[notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
      ∀es:EO+(Message(f)). ∀e:E.
        ∀[nc:ℤ × Cmd]
          uiff(nc ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e);((header(e) = propose) ∧ nc = body(e))
          ∨ (has-es-info-type(es;e;f;ℤ × ℤ × Cmd × Id)
            ∧ (header(e) = ``new_23_sig vote``)
            ∧ ((fst(nc)) = (fst(fst(fst(msgval(e))))))
            ∧ ((snd(nc)) = (snd(fst(msgval(e)))))))

Lemma: new_23_sig_proposal_if_vote
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd]. ∀[r:ℤ]. ∀[i:Id].
  <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e) 
  supposing <<<n, r>, c>, i> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e)

Lemma: new_23_sig_proposal_has_header
∀[Cmd:ValueAllType]
  ∀propose:Atom List
    ∀[notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
      ∀es:EO+(Message(f)). ∀e:E.
        ∀[nc:ℤ × Cmd]
          (header(e) = propose) ∨ (header(e) = ``new_23_sig vote``) 
          supposing nc ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)

Lemma: new_23_sig_round_info_classrel2
∀[Cmd:ValueAllType]
  ∀propose:Atom List
    ∀[notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
      ∀es:EO+(Message(f)). ∀e:E.
        ∀[nrc:ℤ × ℤ × Cmd]
          uiff(nrc ∈ new_23_sig_RoundInfo(Cmd;notify;propose;f)(e);((header(e) = ``new_23_sig retry``) ∧ nrc = body(e))
          ∨ (has-es-info-type(es;e;f;ℤ × ℤ × Cmd × Id)
            ∧ (header(e) = ``new_23_sig vote``)
            ∧ ((fst(fst(nrc))) = (fst(fst(fst(msgval(e))))))
            ∧ ((snd(fst(nrc))) = (snd(fst(fst(msgval(e))))))
            ∧ ((snd(nrc)) = (snd(fst(msgval(e)))))))

Lemma: new_23_sig_quorum_state_fun_eq
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e:E. ∀nr:ℤ × ℤ.
  (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 )

Lemma: new_23_sig_RoundInfo-single-val
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))].
  single-valued-classrel(es;new_23_sig_RoundInfo(Cmd;notify;propose;f);ℤ × ℤ × Cmd)

Lemma: new_23_sig_agreement
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))].
  (new_23_sig_message-constraint{i:l}(Cmd;clients;eq;coeff;flrs;notify;propose;reps;slots;f)
  ⇒ bag-no-repeats(Id;reps)
  ⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
  ⇒ any v1,v2 from new_23_sig_decided'base(Cmd;notify;propose;f) satisfy
     ((fst(v1)) = (fst(v2))) ⇒ ((snd(v1)) = (snd(v2))))

Lemma: new_23_sig_validity
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))].
  (new_23_sig_message-constraint{i:l}(Cmd;clients;eq;coeff;flrs;notify;propose;reps;slots;f)
  ⇒ for every p1 in new_23_sig_decided'base(Cmd;notify;propose;f) there is an
     earlier event  with info=m such that
     (msg-header(m) = propose) ∧ (p1 = msg-body(m)))

Definition: new_23_sig_vote_with_ballot
new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r) ==
  e ∈b new_23_sig_vote'base(Cmd;notify;propose;f) ∧b (fst(fst(fst(msgval(e)))) =z n) ∧b (snd(fst(fst(msgval(e)))) =z r)

Lemma: new_23_sig_vote_with_ballot_wf
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ].
  (new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r) ∈ 𝔹)

Lemma: new_23_sig_vote_with_ballot-assert-type
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ].
  has-es-info-type(es;e;f;ℤ × ℤ × Cmd × Id) supposing ↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r)

Lemma: new_23_sig_vote_with_ballot-assert-classrel
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ].
  <<<n, r>, snd(fst(msgval(e)))>, snd(msgval(e))> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e) 
  supposing ↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r)

Lemma: new_23_sig_vote_with_ballot-header
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ].
  header(e) = ``new_23_sig vote`` supposing ↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r)

Lemma: new_23_sig_vote_with_ballot-if-classrel
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ]. ∀[c:Cmd]. ∀[i:Id].
  ↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r) 
  supposing <<<n, r>, c>, i> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e)

Lemma: new_23_sig_vote_with_ballot-forward
∀[f:Name ─→ Type]. ∀[es:EO+(Message(f))]. ∀[start:E]. ∀[Cmd,propose,notify,e,n,r:Top].
  (new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es.start;e;n;r) 
  ~ new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r))

Definition: new_23_sig_vote_with_ballot_and_id
new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e;n;r;i) ==
  e ∈b new_23_sig_vote'base(Cmd;notify;propose;f)
  ∧b (fst(fst(fst(msgval(e)))) =z n)
  ∧b (snd(fst(fst(msgval(e)))) =z r)
  ∧b snd(msgval(e)) = i

Lemma: new_23_sig_vote_with_ballot_and_id_wf
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ]. ∀[i:Id].
  (new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e;n;r;i) ∈ 𝔹)

Lemma: new_23_sig_vote_with_ballot_and_id-implies
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ]. ∀[i:Id].
  ↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r) 
  supposing ↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e;n;r;i)

Lemma: new_23_sig_vote_with_ballot_and_id-if-classrel
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ]. ∀[c:Cmd]. ∀[i:Id].
  ↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e;n;r;i) 
  supposing <<<n, r>, c>, i> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e)

Lemma: new_23_sig_vote_with_ballot_and_id-assert-type
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ]. ∀[i:Id].
  has-es-info-type(es;e;f;ℤ × ℤ × Cmd × Id) 
  supposing ↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e;n;r;i)

Lemma: new_23_sig_vote_with_ballot_and_id-assert-classrel
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ]. ∀[i:Id].
  <<<n, r>, snd(fst(msgval(e)))>, i> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e) 
  supposing ↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e;n;r;i)

Lemma: new_23_sig_vote_with_ballot_and_id-snd
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ]. ∀[i:Id].
  (snd(msgval(e))) = i supposing ↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e;n;r;i)

Lemma: new_23_sig_vote_with_ballot_and_id-if-snd
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ]. ∀[i:Id].
  (↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e;n;r;i)) supposing 
     (((snd(msgval(e))) = i) and 
     (↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r)))

Lemma: new_23_sig_vote_with_ballot_and_id-forward
∀[f:Name ─→ Type]. ∀[es:EO+(Message(f))]. ∀[start:E]. ∀[Cmd,propose,notify,e,n,r,i:Top].
  (new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es.start;e;n;r;i) 
  ~ new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e;n;r;i))

Definition: new_23_sig_vote_with_ballot_first
new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r) ==
  new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r)
  ∧b (∀e'∈[es-init(es;e);e).¬bnew_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;r;snd(msgval(e))))_b

Lemma: new_23_sig_vote_with_ballot_first_wf
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ].
  (new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r) ∈ 𝔹)

Lemma: new_23_sig_vote_with_ballot_first-assert
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ].
  ↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r) 
  supposing ↑new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r)

Lemma: new_23_sig_vote_with_ballot_first-assert-type
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ].
  has-es-info-type(es;e;f;ℤ × ℤ × Cmd × Id) supposing ↑new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r)

Definition: new_23_sig_commands_from_votes
new_23_sig_commands_from_votes(Cmd;notify;propose;f;es;e;e';n;r) ==
  mapfilter(λe.(snd(fst(msgval(e))));λe'.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.e;e';n;r);[e, e'])

Lemma: new_23_sig_commands_from_votes_wf
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[e':{e':E| e ≤loc e' } ]. ∀[n,r:ℤ].
  (new_23_sig_commands_from_votes(Cmd;notify;propose;f;es;e;e';n;r) ∈ Cmd List)

Lemma: new_23_sig_vote_with_ballot_first-not
∀Cmd:ValueAllType. ∀propose,notify:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e:E. ∀n,r:ℤ.
  ((∃e'∈[es-init(es;e);e). ↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;r;snd(...)))) supposing 
     ((¬↑new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r)) and 
     (↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r)))

Lemma: new_23_sig_vote_with_ballot_first-not2
∀Cmd:ValueAllType. ∀propose,notify:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e:E. ∀n,r:ℤ. ∀i:Id.
  ((∃e'∈[es-init(es;e);e). (↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;r;i))
     ∧ (↑new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e';n;r)))) supposing 
     ((¬↑new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r)) and 
     (↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e;n;r;i)))

Lemma: new_23_sig_vote_with_ballot_first-forward
∀Cmd:ValueAllType. ∀propose,notify:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e,start:E. ∀n,r:ℤ.
  (start ≤loc e 
  ⇒ (new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.start;e;n;r) 
     ~ new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r)
     ∧b (∀e'∈[start;e).¬bnew_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;r;snd(msgval(e))))_b))

Lemma: new_23_sig_vote_with_ballot_first-assert-forward
∀Cmd:ValueAllType. ∀propose,notify:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e,start:E. ∀n,r:ℤ.
  (start ≤loc e 
  ⇒ (↑new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.start;e;n;r)
     ⇐⇒ (↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r))
         ∧ (↑(∀e'∈[start;e).¬bnew_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;r;snd(msgval(e))))_b)))

Lemma: new_23_sig_vote_with_ballot_first-assert-forward2
∀Cmd:ValueAllType. ∀propose,notify:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e,start:E. ∀n,r:ℤ.
  (start ≤loc e 
  ⇒ (↑new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.start;e;n;r)
     ⇐⇒ (↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r))
         ∧ (∀e'∈[start;e).¬↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;r;snd(msgval(e))))))

Definition: new_23_sig_vote_with_ballot_first_alt
new_23_sig_vote_with_ballot_first_alt(Cmd;notify;propose;f;es;e;e';n;r;a) ==
  new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;a;n;r)
  ∧b (¬b(∃x∈[e, e'].new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;x;n;r)
           ∧b es-blocl(es;x;a)
           ∧b (IdDeq (snd(msgval(x))) (snd(msgval(a)))))_b)

Lemma: new_23_sig_vote_with_ballot_first_alt_wf
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e,e':E]. ∀[n,r:ℤ]. ∀[a:E].
  (new_23_sig_vote_with_ballot_first_alt(Cmd;notify;propose;f;es;e;e';n;r;a) ∈ 𝔹)

Definition: new_23_sig_decided_with_id
new_23_sig_decided_with_id(Cmd;notify;propose;f;es;e;n) ==
  e ∈b new_23_sig_decided'base(Cmd;notify;propose;f) ∧b (fst(msgval(e)) =z n)

Lemma: new_23_sig_decided_with_id_wf
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ].
  (new_23_sig_decided_with_id(Cmd;notify;propose;f;es;e;n) ∈ 𝔹)

Lemma: new_23_sig_decided_with_id-assert-type
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ].
  has-es-info-type(es;e;f;ℤ × Cmd) supposing ↑new_23_sig_decided_with_id(Cmd;notify;propose;f;es;e;n)

Lemma: new_23_sig_decided_with_id-assert-classrel
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ].
  <n, snd(msgval(e))> ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e) 
  supposing ↑new_23_sig_decided_with_id(Cmd;notify;propose;f;es;e;n)

Lemma: new_23_sig_quorum_state_eq1
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e:E. ∀n,r:ℤ.
  (new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<n, r>;es;e)
  = <rev(mapfilter(λe.(snd(fst(msgval(e))));
                   λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r);
                   [es-init(es;e);e)))
    , rev(mapfilter(λe.(snd(msgval(e)));
                    λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r);
                    [es-init(es;e);e)))
    >)

Lemma: new_23_sig_quorum_state_eq1-forward
∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e,start:E. ∀n,r:ℤ.
  (start ≤loc e 
  ⇒ (new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<n, r>;es.start;e)
     = <rev(mapfilter(λe.(snd(fst(msgval(e))));
                      λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.start;e;n;r);
                      [start;e)))
       , rev(mapfilter(λe.(snd(msgval(e)));
                       λe.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.start;e;n;r);
                       [start;e)))
       >))

Lemma: new_23_sig_voter_start
∀[Cmd:ValueAllType]. ∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)].
∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd].
  (<n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
  ⇒ (↓∃e':E
        ∃c':Cmd
         (e' ≤loc e 
         ∧ <n, c'> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e')
         ∧ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))))))

Lemma: filter-vote-with-ballot-lemma
∀Cmd:{T:Type| valueall-type(T)} . ∀propose,notify:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose).
∀es:EO+(Message(f)). ∀e:E. ∀n:ℤ. ∀e':E.
  (filter(λa.new_23_sig_vote_with_ballot_first_alt(Cmd;notify;propose;f;es;e;e';n;0;a);[e, e']) 
  ~ filter(λe'.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.e;e';n;0);[e, e']))

Lemma: new_23_sig_progress-step1
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)].
  (msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
  ⇒ bag-no-repeats(Id;reps)
  ⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
  ⇒ loc(e) ↓∈ reps
  ⇒ (¬loc(e) ↓∈ faulty)
  ⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
  ⇒ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
  ⇒ b_all(Id;reps;i.mk-msg-interface(i;make-Msg(``new_23_sig vote``;<<<n, 0>, c>, loc(e)>)) ∈ new_23_sig_main()(e)))

Lemma: new_23_sig_progress-step2
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)].
  (msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
  ⇒ bag-no-repeats(Id;reps)
  ⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
  ⇒ loc(e) ↓∈ reps
  ⇒ (¬loc(e) ↓∈ faulty)
  ⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
  ⇒ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
  ⇒ b_all(Id;reps;i.↓∃e':E
                       ((e < e')
                       ∧ (loc(e') = i)
                       ∧ <<<n, 0>, c>, loc(e)> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e'))))

Lemma: new_23_sig_progress-step3
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)].
  (msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
  ⇒ bag-no-repeats(Id;reps)
  ⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
  ⇒ loc(e) ↓∈ reps
  ⇒ (¬loc(e) ↓∈ faulty)
  ⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
  ⇒ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
  ⇒ b_all(Id;reps;i.↓∃e':E
                       ∃c':Cmd. ((loc(e') = i) ∧ mk-msg-interface(loc(e);make-Msg(``new_23_sig vote``;<<<n, 0>, c'>, i>)\000C) ∈ new_23_sig_main()(e'))))

Lemma: new_23_sig_progress-step4
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)].
  (msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
  ⇒ bag-no-repeats(Id;reps)
  ⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
  ⇒ loc(e) ↓∈ reps
  ⇒ (¬loc(e) ↓∈ faulty)
  ⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
  ⇒ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
  ⇒ b_all(Id;[x∈reps|¬bbag-deq-member(IdDeq;x;faulty)];i.↓∃e':E
                                                            ∃c':Cmd
                                                             ((loc(e') = loc(e))
                                                             ∧ <<<n, 0>, c'>, i> ∈
                                                                new_23_sig_vote'base(Cmd;notify;propose;f)(e'))))

Lemma: new_23_sig_progress-step5
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)].
  (msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
  ⇒ bag-no-repeats(Id;reps)
  ⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
  ⇒ loc(e) ↓∈ reps
  ⇒ (¬loc(e) ↓∈ faulty)
  ⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
  ⇒ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
  ⇒ (↓∃bs:(Id × E × Cmd) List
        ((bag-map(λi.(fst(i));bs) = [x∈reps|¬bbag-deq-member(IdDeq;x;faulty)])
        ∧ (∀x∈bs.(loc(fst(snd(x))) = loc(e))
             ∧ <<<n, 0>, snd(snd(x))>, fst(x)> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(fst(snd(x)))))))

Lemma: new_23_sig_progress-step6
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)].
  (msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
  ⇒ bag-no-repeats(Id;reps)
  ⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
  ⇒ loc(e) ↓∈ reps
  ⇒ (¬loc(e) ↓∈ faulty)
  ⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
  ⇒ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
  ⇒ (↓∃bs:(Id × E × Cmd) List
        ((bag-map(λi.(fst(i));bs) = [x∈reps|¬bbag-deq-member(IdDeq;x;faulty)])
        ∧ (∀x∈bs.(loc(fst(snd(x))) = loc(e))
             ∧ <<<n, 0>, snd(snd(x))>, fst(x)> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(fst(snd(x))))
        ∧ l-ordered(Id × E × Cmd;x,y.(fst(snd(x)) <loc fst(snd(y)));bs))))

Lemma: new_23_sig_progress-step7
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)].
  (msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
  ⇒ bag-no-repeats(Id;reps)
  ⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
  ⇒ loc(e) ↓∈ reps
  ⇒ (¬loc(e) ↓∈ faulty)
  ⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
  ⇒ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
  ⇒ (↓∃bs:(Id × E × Cmd) List
        ((bag-map(λi.(fst(i));bs) = [x∈reps|¬bbag-deq-member(IdDeq;x;faulty)])
        ∧ (∀x∈bs.(loc(fst(snd(x))) = loc(e))
             ∧ <<<n, 0>, snd(snd(x))>, fst(x)> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(fst(snd(x))))
        ∧ l-ordered(Id × E × Cmd;x,y.(fst(snd(x)) <loc fst(snd(y)));bs)
        ∧ (∀x∈bs.e ≤loc fst(snd(x)) )
        ∧ (((coeff * flrs) + 1) ≤ ||bs||))))

Lemma: new_23_sig_progress-step8
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)].
  (msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
  ⇒ bag-no-repeats(Id;reps)
  ⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
  ⇒ loc(e) ↓∈ reps
  ⇒ (¬loc(e) ↓∈ faulty)
  ⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
  ⇒ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
  ⇒ (↓∃bs:(Id × E × Cmd) List
        ((((coeff * flrs) + 1) ≤ ||bs||)
        ∧ (∀x∈bs.(loc(fst(snd(x))) = loc(e))
             ∧ e ≤loc fst(snd(x)) 
             ∧ <<<n, 0>, snd(snd(x))>, fst(x)> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(fst(snd(x))))
        ∧ l-ordered(Id × E × Cmd;x,y.(fst(snd(x)) <loc fst(snd(y)));bs)
        ∧ (∀e'∈[e, fst(snd(last(bs)))].(↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e';n;0))
              ⇒ (e' ∈ map(λx.(fst(snd(x)));bs)))
        ∧ b_all(Id;[x∈reps|¬bbag-deq-member(IdDeq;x;faulty)];i.(i ∈ map(λi.(fst(i));bs))))))

Lemma: new_23_sig_progress-step8-v2
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)].
  (msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
  ⇒ bag-no-repeats(Id;reps)
  ⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
  ⇒ loc(e) ↓∈ reps
  ⇒ (¬loc(e) ↓∈ faulty)
  ⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
  ⇒ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
  ⇒ (↓∃bs:(Id × E × Cmd) List
        ((((coeff * flrs) + 1) ≤ ||bs||)
        ∧ (∀x∈bs.(loc(fst(snd(x))) = loc(e))
             ∧ e ≤loc fst(snd(x)) 
             ∧ <<<n, 0>, snd(snd(x))>, fst(x)> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(fst(snd(x))))
        ∧ l-ordered(Id × E × Cmd;x,y.(fst(snd(x)) <loc fst(snd(y)));bs)
        ∧ (∀e'∈[e, fst(snd(last(bs)))].(↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e';n;0))
              ⇒ (e' ∈ map(λx.(fst(snd(x)));bs)))
        ∧ b_all(Id;[x∈reps|¬bbag-deq-member(IdDeq;x;faulty)];i.(i ∈ map(λi.(fst(i));bs)))
        ∧ (bs
          = mapfilter(λe.<snd(msgval(e)), e, snd(fst(msgval(e)))>;
                      λe.new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;0);
                      [e, fst(snd(last(bs)))])))))

Lemma: new_23_sig_progress-step8-v3
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)].
  (msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
  ⇒ bag-no-repeats(Id;reps)
  ⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
  ⇒ loc(e) ↓∈ reps
  ⇒ (¬loc(e) ↓∈ faulty)
  ⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
  ⇒ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
  ⇒ (↓∃e':E
        (b_all(Id;[x∈reps|
                   ¬bbag-deq-member(IdDeq;x;faulty)];i.(i
                                                         ∈ mapfilter(λe.(snd(msgval(e)));
                                                                     λe....;
                                                                     [e, e'])))
        ∧ (((coeff * flrs) + 1) ≤ ||mapfilter(λe.<snd(msgval(e)), e, snd(fst(msgval(e)))>;
                                              λe.new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;0);
                                              [e, e'])||))))

Lemma: new_23_sig_progress-step9
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)].
  (msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
  ⇒ bag-no-repeats(Id;reps)
  ⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
  ⇒ loc(e) ↓∈ reps
  ⇒ (¬loc(e) ↓∈ faulty)
  ⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
  ⇒ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
  ⇒ (↓∃bs:(Id × E × Cmd) List
        ((((coeff * flrs) + 1) = ||bs||)
        ∧ (∀x∈bs.(loc(fst(snd(x))) = loc(e))
             ∧ e ≤loc fst(snd(x)) 
             ∧ <<<n, 0>, snd(snd(x))>, fst(x)> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(fst(snd(x)))
             ∧ (∀e'∈[e;fst(snd(x))).¬↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;0;fst(x))))
        ∧ l-ordered(Id × E × Cmd;x,y.(fst(snd(x)) <loc fst(snd(y)));bs)
        ∧ (∀e'∈[e, fst(snd(last(bs)))].
              ∀i:Id
                ((↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;0;i))
                ⇒ (∀e''∈[e;e').¬↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e'';n;0;i))
                ⇒ (e' ∈ map(λx.(fst(snd(x)));bs))))
        ∧ no_repeats(Id;map(λx.(fst(x));bs)))))

Lemma: new_23_sig_progress-step9-v2
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)].
  (msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
  ⇒ bag-no-repeats(Id;reps)
  ⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
  ⇒ loc(e) ↓∈ reps
  ⇒ (¬loc(e) ↓∈ faulty)
  ⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
  ⇒ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
  ⇒ (↓∃e':E
        (((coeff * flrs) + 1)
        = ||mapfilter(λe.<snd(msgval(e)), e, snd(fst(msgval(e)))>;
                      λe'.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.e;e';n;0);
                      [e, e'])||)))

Lemma: new_23_sig_progress-step9-v3
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)].
  (msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
  ⇒ bag-no-repeats(Id;reps)
  ⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
  ⇒ loc(e) ↓∈ reps
  ⇒ (¬loc(e) ↓∈ faulty)
  ⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
  ⇒ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
  ⇒ (↓∃e':E
        ((((coeff * flrs) + 1)
         = ||mapfilter(λe.<snd(msgval(e)), e, snd(fst(msgval(e)))>;
                       λe'.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.e;e';n;0);
                       [e, e'])||)
        ∧ e ≤loc e' 
        ∧ (↑new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.e;e';n;0)))))

Lemma: new_23_sig_progress-step10
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)].
  (msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
  ⇒ bag-no-repeats(Id;reps)
  ⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
  ⇒ loc(e) ↓∈ reps
  ⇒ (¬loc(e) ↓∈ faulty)
  ⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
  ⇒ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
  ⇒ (↓∃e':E
        ∃c':Cmd
         ((e <loc e')
         ∧ (<n, c'> ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e')
           ∨ (∃r:ℕ+. <<n, r>, c'> ∈ new_23_sig_retry'base(Cmd;notify;propose;f)(e'))))))

Lemma: new_23_sig_progress1
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)].
  (msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
  ⇒ bag-no-repeats(Id;reps)
  ⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
  ⇒ loc(e) ↓∈ reps
  ⇒ (¬loc(e) ↓∈ faulty)
  ⇒ <n, c> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e)
  ⇒ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e)))
  ⇒ (↓∃e':E
        ∃c':Cmd
         ((e <loc e')
         ∧ (<n, c'> ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e')
           ∨ (∃r:ℕ+. <<n, r>, c'> ∈ new_23_sig_retry'base(Cmd;notify;propose;f)(e'))))))

Lemma: new_23_sig_progress2-step1
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)]. ∀[e':E]. ∀[c':Cmd].
  (msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
  ⇒ bag-no-repeats(Id;reps)
  ⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
  ⇒ loc(e) ↓∈ reps
  ⇒ (¬loc(e) ↓∈ faulty)
  ⇒ (e' ≤loc e 
     ∧ <n, c'> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e')
     ∧ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e')))
     ∧ (no new_23_sig_Notify(Cmd;clients;notify;propose;f) n between e' and e))
  ⇒ <<n, r>, c> ∈ new_23_sig_RoundInfo(Cmd;notify;propose;f)(e)
  ⇒ new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;n;es.e';e) < r
  ⇒ b_all(Id;reps;i.mk-msg-interface(i;make-Msg(``new_23_sig vote``;<<<n, r>, c>, loc(e)>)) ∈ new_23_sig_main()(e)))

Lemma: new_23_sig_progress2-step2
∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))]. ∀[e:E]. ∀[n,r:ℤ]. ∀[c:Cmd]. ∀[faulty:bag(Id)]. ∀[e':E]. ∀[c':Cmd].
  (msgs-interface-delivered-with-omissions(f;es;new_23_sig_main();faulty;flrs;reps)
  ⇒ bag-no-repeats(Id;reps)
  ⇒ (#(reps) = ((coeff * flrs) + flrs + 1))
  ⇒ loc(e) ↓∈ reps
  ⇒ (¬loc(e) ↓∈ faulty)
  ⇒ (e' ≤loc e 
     ∧ <n, c'> ∈ new_23_sig_Proposal(Cmd;notify;propose;f)(e')
     ∧ (¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e')))
     ∧ (no new_23_sig_Notify(Cmd;clients;notify;propose;f) n between e' and e))
  ⇒ <<n, r>, c> ∈ new_23_sig_RoundInfo(Cmd;notify;propose;f)(e)
  ⇒ new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;n;es.e';e) < r
  ⇒ b_all(Id;reps;i.↓∃e1:E
                       ((e < e1)
                       ∧ (loc(e1) = i)
                       ∧ <<<n, r>, c>, loc(e)> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e1))))



Home Index