---

Step * of Lemma pv11_p1_acc_state_fun_eq

∀[Cmd:ValueAllType]. ∀[f:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[ldrs_uid:Id ⟶ ℤ].
  (pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e)
  = if e ∈b pv11_p1_p1a'base(Cmd;f) (+) pv11_p1_p2a'base(Cmd;f)
      then if first(e)
           then pv11_p1_on_p1a(Cmd;ldrs_uid) + pv11_p1_on_p2a(Cmd;ldrs_uid) loc(e) 
                pv11_p1_p1a'base(Cmd;f) (+) pv11_p1_p2a'base(Cmd;f)@e 
                pv11_p1_init_acceptor(Cmd)
           else pv11_p1_on_p1a(Cmd;ldrs_uid) + pv11_p1_on_p2a(Cmd;ldrs_uid) loc(e) 
                pv11_p1_p1a'base(Cmd;f) (+) pv11_p1_p2a'base(Cmd;f)@e 
                pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;pred(e))
           fi 
    if first(e) then pv11_p1_init_acceptor(Cmd)
    else pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;pred(e))
    fi 
  ∈ (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)))
BY
{ (StartEmlProof
   THEN RepUR ``pv11_p1_AcceptorStateFun pv11_p1_AcceptorState state-class2`` 0
   THEN RW (AddrC [2] (LemmaC `loop-class-state-fun-eq`)) 0
   THEN Reduce 0
   THEN Try (Complete ((Auto THEN ProveSingleVal THEN ProveEncodesMsgType)))
   THEN Try (Complete ((Fold `member` 0 THEN Auto THEN ProveFunctional THEN Try (ProveEncodesMsgType) THEN Auto)))
   THEN (RWO "member-parallel-class-bool" 0 THENA Try (CompleteAuto))
   THEN (RWO "member-disjoint-union-comb-bool" 0 THENA Try (CompleteAuto))
   THEN (RWO "member-eclass-eclass1" 0 THENA Try (CompleteAuto))
   THEN Repeat (AutoSplit)
   THEN Try ((Fold `member` 0 THEN Auto THEN ProveFunctional THEN Try (ProveEncodesMsgType) THEN Auto))
   THEN RWO "classfun-res-disjoint-union-comb-as-parallel-eclass1" 0
   THEN Auto
   THEN ProveFunctional
   THEN Try (ProveEncodesMsgType)
   THEN Auto
   THEN (RWO "member-parallel-class-bool" 0 THENA Auto)
   THEN RWO "member-eclass-eclass1" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Cmd:ValueAllType].  \mforall{}[f:pv11\_p1\_headers\_type\{i:l\}(Cmd)].  \mforall{}[es:EO+(Message(f))].  \mforall{}[e:E].
\mforall{}[ldrs$_{uid}$:Id  {}\mrightarrow{}  \mBbbZ{}].
    (pv11\_p1\_AcceptorStateFun(Cmd;ldrs$_{uid}$;f;es;e)
    =  if  e  \mmember{}\msubb{}  pv11\_p1\_p1a'base(Cmd;f)  (+)  pv11\_p1\_p2a'base(Cmd;f)
            then  if  first(e)
                      then  pv11\_p1\_on\_p1a(Cmd;ldrs$_{uid}$)  +  pv11\_p1\_on\_p2a(Cmd;ldrs$\mbackslash{}\000Cff5f{uid}$)  loc(e) 
                                pv11\_p1\_p1a'base(Cmd;f)  (+)  pv11\_p1\_p2a'base(Cmd;f)@e 
                                pv11\_p1\_init\_acceptor(Cmd)
                      else  pv11\_p1\_on\_p1a(Cmd;ldrs$_{uid}$)  +  pv11\_p1\_on\_p2a(Cmd;ldrs$\mbackslash{}\000Cff5f{uid}$)  loc(e) 
                                pv11\_p1\_p1a'base(Cmd;f)  (+)  pv11\_p1\_p2a'base(Cmd;f)@e 
                                pv11\_p1\_AcceptorStateFun(Cmd;ldrs$_{uid}$;f;es;pred(e))
                      fi 
        if  first(e)  then  pv11\_p1\_init\_acceptor(Cmd)
        else  pv11\_p1\_AcceptorStateFun(Cmd;ldrs$_{uid}$;f;es;pred(e))
        fi  )


By

---

Latex:
(StartEmlProof
  THEN  RepUR  ``pv11\_p1\_AcceptorStateFun  pv11\_p1\_AcceptorState  state-class2``  0
  THEN  RW  (AddrC  [2]  (LemmaC  `loop-class-state-fun-eq`))  0
  THEN  Reduce  0
  THEN  Try  (Complete  ((Auto  THEN  ProveSingleVal  THEN  ProveEncodesMsgType)))
  THEN  Try  (Complete  ((Fold  `member`  0
                                            THEN  Auto
                                            THEN  ProveFunctional
                                            THEN  Try  (ProveEncodesMsgType)
                                            THEN  Auto)))
  THEN  (RWO  "member-parallel-class-bool"  0  THENA  Try  (CompleteAuto))
  THEN  (RWO  "member-disjoint-union-comb-bool"  0  THENA  Try  (CompleteAuto))
  THEN  (RWO  "member-eclass-eclass1"  0  THENA  Try  (CompleteAuto))
  THEN  Repeat  (AutoSplit)
  THEN  Try  ((Fold  `member`  0
                        THEN  Auto
                        THEN  ProveFunctional
                        THEN  Try  (ProveEncodesMsgType)
                        THEN  Auto))
  THEN  RWO  "classfun-res-disjoint-union-comb-as-parallel-eclass1"  0
  THEN  Auto
  THEN  ProveFunctional
  THEN  Try  (ProveEncodesMsgType)
  THEN  Auto
  THEN  (RWO  "member-parallel-class-bool"  0  THENA  Auto)
  THEN  RWO  "member-eclass-eclass1"  0
  THEN  Auto)

---

Home Index