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
Lemmas :
system-equiv_wf,
System_wf,
strong-type-continuous_wf
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:
2015_07_23-AM-11_08_15
Last ObjectModification:
2015_01_29-AM-00_09_03
Home
Index