Nuprl Lemma : csm-msg_wf
∀[V:Type]. ∀[sm:CSM(V)]. ∀[i,j:V]. ∀[a:Type(sm;i)]. ∀[b:csm-aux(sm;i)]. ∀[c:Cmd(sm) + Msg(sm)].
csm-msg(sm;i;j;a;b;c) ∈ Msg(sm) supposing ↑csm-sends(sm;i;j;a;b;c)
Proof
Definitions occuring in Statement :
csm-msg: csm-msg(sm;i;j;a;b;c),
csm-sends: csm-sends(sm;i;j;a;b;c),
csm-aux: csm-aux(sm;i),
csm-type: Type(sm;i),
csm-msgtype: Msg(sm),
csm-cmd: Cmd(sm),
csm: CSM(V),
assert: ↑b,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
member: t ∈ T,
union: left + right,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
csm-msg: csm-msg(sm;i;j;a;b;c),
spreadn: spread8,
csm: CSM(V),
csm-sends: csm-sends(sm;i;j;a;b;c),
csm-cmd: Cmd(sm),
pi1: fst(t),
csm-msgtype: Msg(sm),
pi2: snd(t),
csm-aux: csm-aux(sm;i),
csm-type: Type(sm;i),
all: ∀x:A. B[x],
or: P ∨ Q,
band: p ∧b q,
ifthenelse: if b then t else f fi ,
btrue: tt,
assert: ↑b,
true: True,
bfalse: ff,
false: False,
prop: ℙ
Lemmas referenced :
do-apply_wf,
bool_cases_sqequal,
assert_wf,
csm-sends_wf,
csm-cmd_wf,
csm-msgtype_wf,
csm-aux_wf,
csm-type_wf,
csm_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalRule,
sqequalHypSubstitution,
productElimination,
thin,
lemma_by_obid,
isectElimination,
unionEquality,
cumulativity,
hypothesisEquality,
because_Cache,
applyEquality,
dependent_functionElimination,
unionElimination,
hypothesis,
natural_numberEquality,
voidElimination,
dependent_set_memberEquality,
independent_isectElimination,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
isect_memberEquality,
universeEquality
Latex:
\mforall{}[V:Type]. \mforall{}[sm:CSM(V)]. \mforall{}[i,j:V]. \mforall{}[a:Type(sm;i)]. \mforall{}[b:csm-aux(sm;i)]. \mforall{}[c:Cmd(sm) + Msg(sm)].
csm-msg(sm;i;j;a;b;c) \mmember{} Msg(sm) supposing \muparrow{}csm-sends(sm;i;j;a;b;c)
Date html generated:
2016_05_15-PM-05_11_56
Last ObjectModification:
2015_12_27-PM-02_22_52
Theory : general
Home
Index