Nuprl Lemma : csm-sends_wf
∀[V:Type]. ∀[sm:CSM(V)]. ∀[i,j:V]. ∀[a:Type(sm;i)]. ∀[b:csm-aux(sm;i)]. ∀[c:Cmd(sm) + Msg(sm)].
(csm-sends(sm;i;j;a;b;c) ∈ 𝔹)
Proof
Definitions occuring in Statement :
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),
bool: 𝔹,
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,
csm-sends: csm-sends(sm;i;j;a;b;c),
csm: CSM(V),
spreadn: spread8,
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],
implies: P ⇒ Q,
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
band: p ∧b q,
ifthenelse: if b then t else f fi ,
uiff: uiff(P;Q),
and: P ∧ Q,
uimplies: b supposing a,
prop: ℙ,
subtype_rel: A ⊆r B,
so_lambda: λ2x.t[x],
so_apply: x[s],
top: Top,
bfalse: ff
Lemmas referenced :
bool_wf,
eqtt_to_assert,
can-apply_wf,
assert_wf,
subtype_rel_dep_function,
top_wf,
subtype_rel_union,
equal_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,
applyEquality,
functionExtensionality,
hypothesisEquality,
cumulativity,
hypothesis,
extract_by_obid,
lambdaFormation,
unionElimination,
equalityElimination,
isectElimination,
independent_isectElimination,
unionEquality,
because_Cache,
dependent_set_memberEquality,
lambdaEquality,
isect_memberEquality,
voidElimination,
voidEquality,
equalityTransitivity,
equalitySymmetry,
dependent_functionElimination,
independent_functionElimination,
axiomEquality,
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-sends(sm;i;j;a;b;c) \mmember{} \mBbbB{})
Date html generated:
2018_05_21-PM-07_48_53
Last ObjectModification:
2017_07_26-PM-05_26_40
Theory : general
Home
Index