---

Step * of Lemma pv11_p1_headers-property

∀[Cmd:ValueAllType]
  ∀f:pv11_p1_headers_type{i:l}(Cmd)
    (((f ``pv11_p1 p1a``) = (Id × pv11_p1_Ballot_Num()) ∈ Type)
    ∧ ((f ``pv11_p1 p1b``)
      = (Id × pv11_p1_Ballot_Num() × pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
      ∈ Type)
    ∧ ((f ``pv11_p1 p2a``) = (Id × pv11_p1_Ballot_Num() × ℤ × Cmd) ∈ Type)
    ∧ ((f ``pv11_p1 p2b``) = (Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num()) ∈ Type)
    ∧ ((f ``pv11_p1 preempted``) = pv11_p1_Ballot_Num() ∈ Type)
    ∧ ((f ``pv11_p1 adopted``) = (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)) ∈ Type)
    ∧ ((f [propose]) = (ℤ × Cmd) ∈ Type)
    ∧ ((f [decision]) = (ℤ × Cmd) ∈ Type))
BY
{ (Auto
   THEN D 2
   THEN Auto
   THEN ((InstLemmaUp `l_all_iff` [⌜Name⌝]⋅ THENA Auto)
         THEN (RWO "-1" 4 THENA Auto)
         THEN Thin (-1)
         THEN RWO "4" 0
         THEN Auto
         THEN RepUR ``pv11_p1_headers pv11_p1_headers_fun`` 0
         THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[Cmd:ValueAllType]
    \mforall{}f:pv11\_p1\_headers\_type\{i:l\}(Cmd)
        (((f  ``pv11\_p1  p1a``)  =  (Id  \mtimes{}  pv11\_p1\_Ballot\_Num()))
        \mwedge{}  ((f  ``pv11\_p1  p1b``)
            =  (Id
                \mtimes{}  pv11\_p1\_Ballot\_Num()
                \mtimes{}  pv11\_p1\_Ballot\_Num()
                \mtimes{}  ((pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List)))
        \mwedge{}  ((f  ``pv11\_p1  p2a``)  =  (Id  \mtimes{}  pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd))
        \mwedge{}  ((f  ``pv11\_p1  p2b``)  =  (Id  \mtimes{}  pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  pv11\_p1\_Ballot\_Num()))
        \mwedge{}  ((f  ``pv11\_p1  preempted``)  =  pv11\_p1\_Ballot\_Num())
        \mwedge{}  ((f  ``pv11\_p1  adopted``)  =  (pv11\_p1\_Ballot\_Num()  \mtimes{}  ((pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List)))
        \mwedge{}  ((f  [propose])  =  (\mBbbZ{}  \mtimes{}  Cmd))
        \mwedge{}  ((f  [decision])  =  (\mBbbZ{}  \mtimes{}  Cmd)))


By

---

Latex:
(Auto
  THEN  D  2
  THEN  Auto
  THEN  ((InstLemmaUp  `l\_all\_iff`  [\mkleeneopen{}Name\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (RWO  "-1"  4  THENA  Auto)
              THEN  Thin  (-1)
              THEN  RWO  "4"  0
              THEN  Auto
              THEN  RepUR  ``pv11\_p1\_headers  pv11\_p1\_headers\_fun``  0
              THEN  Auto)\mcdot{})

---

Home Index