Nuprl Lemma : test2
∀p:ℕ + (ℕ ⟶ ℕ). ∀bs:ℕ List. (case p of inl(x) => x + 1 | inr(y) => y 3 ∈ ℤ)
Proof
Definitions occuring in Statement :
list: T List,
nat: ℕ,
all: ∀x:A. B[x],
member: t ∈ T,
apply: f a,
function: x:A ⟶ B[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
union: left + right,
add: n + m,
natural_number: $n,
int: ℤ
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
nat: ℕ,
le: A ≤ B,
and: P ∧ Q,
less_than': less_than'(a;b),
false: False,
not: ¬A,
implies: P ⇒ Q,
prop: ℙ,
uall: ∀[x:A]. B[x],
subtype_rel: A ⊆r B
Lemmas referenced :
false_wf,
le_wf,
list_wf,
nat_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
unionElimination,
thin,
sqequalRule,
addEquality,
sqequalHypSubstitution,
setElimination,
rename,
hypothesisEquality,
hypothesis,
natural_numberEquality,
applyEquality,
dependent_set_memberEquality,
independent_pairFormation,
lemma_by_obid,
isectElimination,
because_Cache,
unionEquality,
functionEquality
Latex:
\mforall{}p:\mBbbN{} + (\mBbbN{} {}\mrightarrow{} \mBbbN{}). \mforall{}bs:\mBbbN{} List. (case p of inl(x) => x + 1 | inr(y) => y 3 \mmember{} \mBbbZ{})
Date html generated:
2016_05_15-PM-07_46_18
Last ObjectModification:
2015_12_27-AM-11_09_53
Theory : general
Home
Index