Nuprl Lemma : norm-intransit_wf
∀[M:Type ⟶ Type]. ∀[intr:pInTransit(P.M[P])].
(norm-intransit(intr) ∈ {intr':pInTransit(P.M[P])| intr' = intr ∈ pInTransit(P.M[P])} )
Proof
Definitions occuring in Statement :
norm-intransit: norm-intransit(intr),
pInTransit: pInTransit(P.M[P]),
uall: ∀[x:A]. B[x],
so_apply: x[s],
member: t ∈ T,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
so_lambda: λ2x.t[x],
so_apply: x[s],
pInTransit: pInTransit(P.M[P]),
norm-intransit: norm-intransit(intr),
spreadn: spread3,
has-value: (a)↓,
uimplies: b supposing a,
all: ∀x:A. B[x],
implies: P ⇒ Q,
pCom: pCom(P.M[P]),
Com: Com(P.M[P]),
tagged+: T |+ z:B,
and: P ∧ Q,
cand: A c∧ B,
tag-case: z:T
Latex:
\mforall{}[M:Type {}\mrightarrow{} Type]. \mforall{}[intr:pInTransit(P.M[P])].
(norm-intransit(intr) \mmember{} \{intr':pInTransit(P.M[P])| intr' = intr\} )
Date html generated:
2016_05_17-AM-10_25_23
Last ObjectModification:
2016_01_18-AM-00_18_12
Theory : process-model
Home
Index