Nuprl Lemma : nat-to-incomparable-property

`∀[n,m:ℕ].  ¬nat-to-incomparable(n) ≤ nat-to-incomparable(m) supposing ¬(n = m ∈ ℤ)`

Proof

Definitions occuring in Statement :  nat-to-incomparable: `nat-to-incomparable(n)` iseg: `l1 ≤ l2` nat: `ℕ` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` not: `¬A` int: `ℤ` atom: `Atom` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` not: `¬A` implies: `P `` Q` false: `False` nat-to-incomparable: `nat-to-incomparable(n)` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` or: `P ∨ Q` prop: `ℙ` subtype_rel: `A ⊆r B` name: `Name` nat: `ℕ` rev_implies: `P `` Q` guard: `{T}` assert: `↑b` ifthenelse: `if b then t else f fi ` deq-member: `x ∈b L` reduce: `reduce(f;k;as)` list_ind: list_ind cons: `[a / b]` bor: `p ∨bq` atom-deq: `AtomDeq` eq_atom: `x =a y` bfalse: `ff` nil: `[]` it: `⋅` exists: `∃x:A. B[x]` less_than: `a < b` squash: `↓T` less_than': `less_than'(a;b)` top: `Top` sq_type: `SQType(T)` btrue: `tt` true: `True`
Lemmas referenced :  list_wf true_wf squash_wf str-to-nat_wf int_subtype_base str-to-nat-to-str append-cancellation-right length_wf null_cons_lemma null_nil_lemma iseg_nil atom_subtype_base subtype_base_sq cons_iseg length_of_cons_lemma product_subtype_list length_of_nil_lemma list-cases atom-deq_wf assert-deq-member member-nat-to-str iseg_member l_member_wf cons_member member_append nat_wf equal_wf not_wf name_wf nat-to-incomparable_wf iseg_wf nil_wf cons_wf nat-to-str_wf append_wf iseg_append_iff
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation thin sqequalHypSubstitution lemma_by_obid isectElimination atomEquality dependent_functionElimination hypothesisEquality hypothesis tokenEquality productElimination independent_functionElimination unionElimination because_Cache voidElimination applyEquality lambdaEquality sqequalRule intEquality setElimination rename isect_memberEquality equalityTransitivity equalitySymmetry inrFormation inlFormation imageElimination promote_hyp hypothesis_subsumption voidEquality instantiate cumulativity independent_isectElimination natural_numberEquality imageMemberEquality baseClosed

Latex:
\mforall{}[n,m:\mBbbN{}].    \mneg{}nat-to-incomparable(n)  \mleq{}  nat-to-incomparable(m)  supposing  \mneg{}(n  =  m)

Date html generated: 2016_05_14-PM-03_36_17
Last ObjectModification: 2016_01_14-PM-11_19_20

Theory : decidable!equality

Home Index