Nuprl Lemma : pv11_p1_on_propose_wf

[Cmd:ValueAllType]
  (pv11_p1_on_propose(Cmd) ∈ Id
   ⟶ (ℤ × Cmd)
   ⟶ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))
   ⟶ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)))


Proof




Definitions occuring in Statement :  pv11_p1_on_propose: pv11_p1_on_propose(Cmd) pv11_p1_Ballot_Num: pv11_p1_Ballot_Num() Id: Id list: List vatype: ValueAllType bool: 𝔹 uall: [x:A]. B[x] member: t ∈ T function: x:A ⟶ B[x] product: x:A × B[x] int:
Definitions unfolded in proof :  vatype: ValueAllType uall: [x:A]. B[x] member: t ∈ T pv11_p1_on_propose: pv11_p1_on_propose(Cmd) spreadn: spread3 so_lambda: λ2x.t[x] so_apply: x[s] all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  bfalse: ff uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a exists: x:A. B[x] prop: or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b false: False subtype_rel: A ⊆B

Latex:
\mforall{}[Cmd:ValueAllType]
    (pv11\_p1\_on\_propose(Cmd)  \mmember{}  Id
      {}\mrightarrow{}  (\mBbbZ{}  \mtimes{}  Cmd)
      {}\mrightarrow{}  (pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbB{}  \mtimes{}  ((\mBbbZ{}  \mtimes{}  Cmd)  List))
      {}\mrightarrow{}  (pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbB{}  \mtimes{}  ((\mBbbZ{}  \mtimes{}  Cmd)  List)))



Date html generated: 2016_05_17-PM-02_56_09
Last ObjectModification: 2015_12_29-PM-11_24_24

Theory : paxos!synod


Home Index