### 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