Nuprl Lemma : subterm-cases
∀[opr:Type]. ∀s,t:term(opr). (s << t ⇐⇒ s < t ∨ (∃r:term(opr). (s < r ∧ r << t)))
Proof
Definitions occuring in Statement :
subterm: s << t,
immediate-subterm: s < t,
term: term(opr),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
iff: P ⇐⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
subterm-rel: subterm-rel(opr),
subterm: s << t,
infix_ap: x f y,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
implies: P ⇒ Q,
prop: ℙ,
rev_implies: P ⇐ Q,
or: P ∨ Q,
exists: ∃x:A. B[x],
guard: {T}
Lemmas referenced :
transitive-closure-cases,
term_wf,
immediate-subterm_wf,
subterm_wf,
istype-universe,
immediate-is-subterm,
subterm_transitivity
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
lambdaEquality_alt,
inhabitedIsType,
universeIsType,
sqequalRule,
lambdaFormation_alt,
independent_pairFormation,
unionIsType,
productIsType,
because_Cache,
instantiate,
universeEquality,
dependent_functionElimination,
independent_functionElimination,
unionElimination,
productElimination
Latex:
\mforall{}[opr:Type]. \mforall{}s,t:term(opr). (s << t \mLeftarrow{}{}\mRightarrow{} s < t \mvee{} (\mexists{}r:term(opr). (s < r \mwedge{} r << t)))
Date html generated:
2020_05_19-PM-09_54_13
Last ObjectModification:
2020_03_10-PM-01_55_21
Theory : terms
Home
Index