---

Step * of Lemma pv11_p1_inc_acc_bnum_fun

∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀ldrs_uid:Id ⟶ ℤ.
  (e1 ≤loc e2 
  ⇒ (↑(pv11_p1_leq_bnum(ldrs_uid) (fst(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e1))) 
        (fst(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e2))))))
BY
{ (StartEmlProof
   THEN D (-1)
   THEN Try (Complete (((HypSubst' (-1) 0 THENA Auto) THEN BLemma `pv11_p1_leq_bnum_refl` THEN Auto)))
   THEN (InstLemma `pv11_p1_inc_acc` [⌜Cmd⌝;⌜ldrs_uid⌝;⌜f⌝;⌜es⌝;⌜e1⌝;⌜e2⌝;
         ⌜<fst(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e1)), snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e1))>⌝;
         ⌜<fst(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e2)), snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e2))>⌝]⋅
         THENA (Auto THEN (RWO "pair-eta<" 0 THENA Auto) THEN BLemma `pv11_p1_AcceptorState-classrel` THEN Auto)
         )
   THEN Reduce (-1)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}Cmd:ValueAllType.  \mforall{}f:pv11\_p1\_headers\_type\{i:l\}(Cmd).  \mforall{}es:EO+(Message(f)).  \mforall{}e1,e2:E.
\mforall{}ldrs$_{uid}$:Id  {}\mrightarrow{}  \mBbbZ{}.
    (e1  \mleq{}loc  e2 
    {}\mRightarrow{}  (\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}$)  (fst(pv11\_p1\_AcceptorStateFun(Cmd;ldrs\mbackslash{}ff\000C24_{uid}$;f;es;e1))) 
                (fst(pv11\_p1\_AcceptorStateFun(Cmd;ldrs$_{uid}$;f;es;e2))))))


By

---

Latex:
(StartEmlProof
  THEN  D  (-1)
  THEN  Try  (Complete  (((HypSubst'  (-1)  0  THENA  Auto)  THEN  BLemma  `pv11\_p1\_leq\_bnum\_refl`  THEN  Auto)))
  THEN  (InstLemma  `pv11\_p1\_inc\_acc`  [\mkleeneopen{}Cmd\mkleeneclose{};\mkleeneopen{}ldrs$_{uid}$\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{};
              \mkleeneopen{}<fst(pv11\_p1\_AcceptorStateFun(Cmd;ldrs$_{uid}$;f;es;e1))
                ,  snd(pv11\_p1\_AcceptorStateFun(Cmd;ldrs$_{uid}$;f;es;e1))
                >\mkleeneclose{};\mkleeneopen{}<fst(pv11\_p1\_AcceptorStateFun(Cmd;ldrs$_{uid}$;f;es;e2))
                        ,  snd(pv11\_p1\_AcceptorStateFun(Cmd;ldrs$_{uid}$;f;es;e2))
                        >\mkleeneclose{}]\mcdot{}
              THENA  (Auto
                            THEN  (RWO  "pair-eta<"  0  THENA  Auto)
                            THEN  BLemma  `pv11\_p1\_AcceptorState-classrel`
                            THEN  Auto)
              )
  THEN  Reduce  (-1)
  THEN  Auto)

---

Home Index