Nuprl Lemma : picomm-pre_wf

[v:pi_term()]. picomm-pre(v) ∈ pi_prefix() supposing ↑picomm?(v)


Proof




Definitions occuring in Statement :  picomm-pre: picomm-pre(v) picomm?: picomm?(v) pi_term: pi_term() pi_prefix: pi_prefix() assert: b uimplies: supposing a uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a member: t ∈ T ext-eq: A ≡ B and: P ∧ Q subtype_rel: A ⊆B all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) sq_type: SQType(T) guard: {T} eq_atom: =a y ifthenelse: if then else fi  picomm?: picomm?(v) pi1: fst(t) assert: b bfalse: ff false: False exists: x:A. B[x] prop: or: P ∨ Q bnot: ¬bb picomm-pre: picomm-pre(v) pi2: snd(t)

Latex:
\mforall{}[v:pi\_term()].  picomm-pre(v)  \mmember{}  pi\_prefix()  supposing  \muparrow{}picomm?(v)



Date html generated: 2016_05_17-AM-11_21_31
Last ObjectModification: 2015_12_29-PM-06_55_20

Theory : event-logic-applications


Home Index