Nuprl Lemma : ts-transitive-stable
∀ts:transition-system{i:l}
∀[R:ts-type(ts) ⟶ ts-type(ts) ⟶ ℙ]
(Refl(ts-type(ts);x,y.R[x;y])
⇒ Trans(ts-type(ts);x,y.R[x;y])
⇒ ts-rel(ts) => λx,y. R[x;y]
⇒ ts-stable-rel(ts;x,y.R[x;y]))
Proof
Definitions occuring in Statement :
ts-stable-rel: ts-stable-rel(ts;x,y.R[x; y]),
ts-rel: ts-rel(ts),
ts-type: ts-type(ts),
transition-system: transition-system{i:l},
rel_implies: R1 => R2,
trans: Trans(T;x,y.E[x; y]),
refl: Refl(T;x,y.E[x; y]),
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s1;s2],
all: ∀x:A. B[x],
implies: P ⇒ Q,
lambda: λx.A[x],
function: x:A ⟶ B[x]
Definitions unfolded in proof :
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
ts-stable-rel: ts-stable-rel(ts;x,y.R[x; y]),
member: t ∈ T,
prop: ℙ,
infix_ap: x f y,
so_apply: x[s1;s2],
so_lambda: λ2x y.t[x; y],
ts-stable: ts-stable(ts;x.P[x]),
rel_implies: R1 => R2,
guard: {T},
trans: Trans(T;x,y.E[x; y]),
so_lambda: λ2x.t[x],
so_apply: x[s],
refl: Refl(T;x,y.E[x; y])
Lemmas referenced :
rel_star_wf,
ts-type_wf,
ts-rel_wf,
rel_implies_wf,
trans_wf,
refl_wf,
transition-system_wf,
ts-stable-star
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
isect_memberFormation,
applyEquality,
cut,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
lambdaEquality,
sqequalRule,
functionEquality,
cumulativity,
universeEquality,
dependent_functionElimination,
independent_functionElimination
Latex:
\mforall{}ts:transition-system\{i:l\}
\mforall{}[R:ts-type(ts) {}\mrightarrow{} ts-type(ts) {}\mrightarrow{} \mBbbP{}]
(Refl(ts-type(ts);x,y.R[x;y])
{}\mRightarrow{} Trans(ts-type(ts);x,y.R[x;y])
{}\mRightarrow{} ts-rel(ts) => \mlambda{}x,y. R[x;y]
{}\mRightarrow{} ts-stable-rel(ts;x,y.R[x;y]))
Date html generated:
2016_05_15-PM-05_43_30
Last ObjectModification:
2015_12_27-PM-00_29_54
Theory : general
Home
Index