Nuprl Lemma : before_trans
∀a:LOSet. ∀u,v:|a|. ∀ws:|a| List. ((v <a u) ⇒ (↑before(v;ws)) ⇒ (↑before(u;ws)))
Proof
Definitions occuring in Statement :
before: before(u;ps),
list: T List,
assert: ↑b,
all: ∀x:A. B[x],
implies: P ⇒ Q,
loset: LOSet,
set_lt: a <p b,
set_car: |p|
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
uall: ∀[x:A]. B[x],
loset: LOSet,
poset: POSet{i},
qoset: QOSet,
dset: DSet,
or: P ∨ Q,
top: Top,
assert: ↑b,
ifthenelse: if b then t else f fi ,
btrue: tt,
implies: P ⇒ Q,
true: True,
prop: ℙ,
cons: [a / b],
uiff: uiff(P;Q),
and: P ∧ Q,
uimplies: b supposing a
Lemmas referenced :
set_car_wf,
list-cases,
before_nil_lemma,
true_wf,
set_lt_wf,
product_subtype_list,
before_cons_lemma,
assert_of_set_lt,
assert_wf,
set_blt_wf,
list_wf,
loset_wf,
qoset_lt_trans
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
setElimination,
rename,
hypothesisEquality,
hypothesis,
dependent_functionElimination,
unionElimination,
sqequalRule,
isect_memberEquality,
voidElimination,
voidEquality,
natural_numberEquality,
promote_hyp,
hypothesis_subsumption,
productElimination,
because_Cache,
addLevel,
impliesFunctionality,
independent_isectElimination,
functionEquality
Latex:
\mforall{}a:LOSet. \mforall{}u,v:|a|. \mforall{}ws:|a| List. ((v <a u) {}\mRightarrow{} (\muparrow{}before(v;ws)) {}\mRightarrow{} (\muparrow{}before(u;ws)))
Date html generated:
2016_05_16-AM-08_14_59
Last ObjectModification:
2015_12_28-PM-06_28_53
Theory : polynom_2
Home
Index