Nuprl Lemma : fseg-test
∀T:Type. ∀as,bs,cs:T List.
((fseg(T;as;as) ∧ (fseg(T;as;bs) ⇒ fseg(T;bs;cs) ⇒ fseg(T;as;cs))) ∧ as ≤ as ∧ (as ≤ bs ⇒ bs ≤ cs ⇒ as ≤ cs))
Proof
Definitions occuring in Statement :
fseg: fseg(T;L1;L2),
iseg: l1 ≤ l2,
list: T List,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
universe: Type
Definitions unfolded in proof :
all: ∀x:A. B[x],
and: P ∧ Q,
cand: A c∧ B,
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
implies: P ⇒ Q,
guard: {T},
prop: ℙ,
label: ...$L... t,
iseg: l1 ≤ l2,
exists: ∃x:A. B[x]
Lemmas referenced :
fseg_weakening,
fseg_transitivity,
fseg_wf,
iseg_weakening,
iseg_transitivity2,
iseg_wf,
list_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
dependent_functionElimination,
because_Cache,
independent_isectElimination,
hypothesis,
independent_pairFormation,
independent_functionElimination,
productElimination,
universeEquality
Latex:
\mforall{}T:Type. \mforall{}as,bs,cs:T List.
((fseg(T;as;as) \mwedge{} (fseg(T;as;bs) {}\mRightarrow{} fseg(T;bs;cs) {}\mRightarrow{} fseg(T;as;cs)))
\mwedge{} as \mleq{} as
\mwedge{} (as \mleq{} bs {}\mRightarrow{} bs \mleq{} cs {}\mRightarrow{} as \mleq{} cs))
Date html generated:
2016_05_15-PM-03_35_30
Last ObjectModification:
2015_12_27-PM-01_13_56
Theory : general
Home
Index