Nuprl Lemma : system-equiv-implies-equal
∀[M:Type ⟶ Type]
∀[S1,S2:System(P.M[P])]. S1 = S2 ∈ (Top × LabeledDAG(pInTransit(P.M[P]))) supposing system-equiv(P.M[P];S1;S2)
supposing Continuous+(P.M[P])
Proof
Definitions occuring in Statement :
system-equiv: system-equiv(T.M[T];S1;S2),
System: System(P.M[P]),
pInTransit: pInTransit(P.M[P]),
ldag: LabeledDAG(T),
strong-type-continuous: Continuous+(T.F[T]),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
top: Top,
so_apply: x[s],
function: x:A ⟶ B[x],
product: x:A × B[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
System: System(P.M[P]),
top: Top,
system-equiv: system-equiv(T.M[T];S1;S2),
and: P ∧ Q,
prop: ℙ,
so_lambda: λ2x.t[x],
so_apply: x[s]
Latex:
\mforall{}[M:Type {}\mrightarrow{} Type]
\mforall{}[S1,S2:System(P.M[P])]. S1 = S2 supposing system-equiv(P.M[P];S1;S2)
supposing Continuous+(P.M[P])
Date html generated:
2016_05_17-AM-10_37_06
Last ObjectModification:
2015_12_29-PM-05_26_13
Theory : process-model
Home
Index