---

Step * of Lemma pv11_p1_ldr_fun_ord

∀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_LeaderStateFun(Cmd;ldrs_uid;f;es;e1))) 
        (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e2))))))
BY
{ (StartEmlProof
   THEN InstLemma `pv11_p1_ldr_ord` [⌜Cmd⌝;⌜ldrs_uid⌝;⌜f⌝;⌜es⌝;⌜e1⌝;⌜e2⌝;⌜pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1)⌝;
   ⌜pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e2)⌝]⋅
   THEN Auto
   THEN Try (Complete ((BLemma `pv11_p1_LeaderState-classrel` THEN Auto)))
   THEN (Subst ⌜pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1) ~ <fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1))
                                                               , fst(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1)))
                                                               , snd(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1)))>\000C⌝ (-1)⋅
         THENA RepeatFor 2 ((RWO "pair-eta<" 0 THEN Auto))
         )
   THEN (Subst ⌜pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e2) ~ <fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e2))
                                                               , fst(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e2)))
                                                               , snd(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e2)))>\000C⌝ (-1)⋅
         THENA RepeatFor 2 ((RWO "pair-eta<" 0 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  <loc  e2)
    {}\mRightarrow{}  (\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}$)  (fst(pv11\_p1\_LeaderStateFun(Cmd;ldrs$\000C_{uid}$;f;es;e1))) 
                (fst(pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e2))))))


By

---

Latex:
(StartEmlProof
  THEN  InstLemma  `pv11\_p1\_ldr\_ord`  [\mkleeneopen{}Cmd\mkleeneclose{};\mkleeneopen{}ldrs$_{uid}$\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{};
  \mkleeneopen{}pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e1)\mkleeneclose{};\mkleeneopen{}pv11\_p1\_LeaderStateFun(Cmd;\000Cldrs$_{uid}$;f;es;e2)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  (Complete  ((BLemma  `pv11\_p1\_LeaderState-classrel`  THEN  Auto)))
  THEN  (Subst  \mkleeneopen{}pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e1) 
                            \msim{}  <fst(pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e1))
                                ,  fst(snd(pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e1)))
                                ,  snd(snd(pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e1)))>\mkleeneclose{}  (\000C-1)\mcdot{}
              THENA  RepeatFor  2  ((RWO  "pair-eta<"  0  THEN  Auto))
              )
  THEN  (Subst  \mkleeneopen{}pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e2) 
                            \msim{}  <fst(pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e2))
                                ,  fst(snd(pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e2)))
                                ,  snd(snd(pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e2)))>\mkleeneclose{}  (\000C-1)\mcdot{}
              THENA  RepeatFor  2  ((RWO  "pair-eta<"  0  THEN  Auto))
              )
  THEN  Reduce  (-1)
  THEN  Auto)

---

Home Index