Nuprl Lemma : ite_rw_test
∀[n:ℕ]. ∀[i:ℕ+n]. False supposing (¬(0 = 0 ∈ ℤ)) ∧ (¬(n = 0 ∈ ℤ))
Proof
Definitions occuring in Statement :
int_seg: {i..j-},
nat: ℕ,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
not: ¬A,
and: P ∧ Q,
false: False,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
false: False,
and: P ∧ Q,
not: ¬A,
implies: P ⇒ Q,
prop: ℙ,
nat: ℕ
Lemmas referenced :
not_wf,
equal-wf-base,
equal-wf-T-base,
int_seg_wf,
nat_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalHypSubstitution,
productElimination,
thin,
hypothesis,
independent_functionElimination,
natural_numberEquality,
voidElimination,
sqequalRule,
because_Cache,
productEquality,
extract_by_obid,
isectElimination,
intEquality,
baseClosed,
setElimination,
rename,
hypothesisEquality,
isect_memberEquality,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}[n:\mBbbN{}]. \mforall{}[i:\mBbbN{}\msupplus{}n]. False supposing (\mneg{}(0 = 0)) \mwedge{} (\mneg{}(n = 0))
Date html generated:
2018_05_21-PM-00_04_05
Last ObjectModification:
2018_05_19-AM-07_10_44
Theory : int_1
Home
Index