Nuprl Lemma : oob-left-or-right
∀[B,A:Type]. ∀x:one_or_both(A;B). ((↑oob-hasleft(x)) ∨ (↑oob-hasright(x)))
Proof
Definitions occuring in Statement :
oob-hasright: oob-hasright(x),
oob-hasleft: oob-hasleft(x),
one_or_both: one_or_both(A;B),
assert: ↑b,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
or: P ∨ Q,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
member: t ∈ T,
so_lambda: λ2x.t[x],
oob-hasright: oob-hasright(x),
oob-hasleft: oob-hasleft(x),
so_apply: x[s],
implies: P ⇒ Q,
oobleft?: oobleft?(x),
oobboth?: oobboth?(x),
oobright?: oobright?(x),
top: Top,
bor: p ∨bq,
ifthenelse: if b then t else f fi ,
bfalse: ff,
assert: ↑b,
btrue: tt,
or: P ∨ Q,
true: True,
prop: ℙ,
guard: {T}
Lemmas referenced :
one_or_both-induction,
or_wf,
assert_wf,
bor_wf,
oobleft?_wf,
oobboth?_wf,
oobright?_wf,
one_or_both_wf,
one_or_both_ind_oobboth_lemma,
true_wf,
one_or_both_oobleft_lemma,
false_wf,
one_or_both_ind_oobright_lemma
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
lambdaFormation,
cut,
thin,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
hypothesisEquality,
sqequalRule,
lambdaEquality,
hypothesis,
independent_functionElimination,
dependent_functionElimination,
isect_memberEquality,
voidElimination,
voidEquality,
inlFormation,
natural_numberEquality,
productEquality,
because_Cache,
inrFormation,
universeEquality
Latex:
\mforall{}[B,A:Type]. \mforall{}x:one\_or\_both(A;B). ((\muparrow{}oob-hasleft(x)) \mvee{} (\muparrow{}oob-hasright(x)))
Date html generated:
2016_05_15-PM-05_36_51
Last ObjectModification:
2015_12_27-PM-02_06_54
Theory : general
Home
Index