Nuprl Lemma : add-nat-missing-prop
∀s:nat-missing-type(). ∀x,y:ℕ.
  (↑member-nat-missing(x;add-nat-missing(y;s)) 
⇐⇒ (x = y ∈ ℕ) ∨ (↑member-nat-missing(x;s)))
Proof
Definitions occuring in Statement : 
add-nat-missing: add-nat-missing(i;s)
, 
member-nat-missing: member-nat-missing(i;s)
, 
nat-missing-type: nat-missing-type()
, 
nat: ℕ
, 
assert: ↑b
, 
all: ∀x:A. B[x]
, 
iff: P 
⇐⇒ Q
, 
or: P ∨ Q
, 
equal: s = t ∈ T
Lemmas : 
lt_int_wf, 
iff_transitivity, 
assert_wf, 
le_int_wf, 
bool_wf, 
eqtt_to_assert, 
assert_of_le_int, 
bnot_wf, 
in-missing_wf, 
append_wf, 
subtype_rel_list, 
nat_wf, 
from-upto_wf, 
le_wf, 
less_than_wf, 
not_wf, 
iff_weakening_uiff, 
assert_of_band, 
assert_of_bnot, 
assert-in-missing-nat-iff, 
l_member_wf, 
subtype_rel_sets, 
decidable__le, 
false_wf, 
not-le-2, 
sq_stable__le, 
condition-implies-le, 
minus-add, 
minus-one-mul, 
add-swap, 
add-commutes, 
zero-add, 
add_functionality_wrt_le, 
add-associates, 
le-add-cancel, 
list_wf, 
l-ordered_wf, 
l_all_wf2, 
or_wf, 
equal_wf, 
eq_int_wf, 
equal-wf-base-T, 
set_subtype_base, 
int_subtype_base, 
remove-combine_wf, 
subtract_wf, 
bool_cases, 
subtype_base_sq, 
bool_subtype_base, 
assert_of_lt_int, 
eqff_to_assert, 
assert_of_eq_int, 
l-ordered-append, 
l-ordered-from-upto-lt-nat, 
from-upto-member-nat, 
l_all_iff, 
decidable__lt, 
less-iff-le, 
member_append, 
not_over_or, 
not_over_and, 
le-add-cancel2, 
decidable__equal_int, 
not-equal-2, 
l-ordered-remove-combine, 
decidable__equal_nat, 
remove-combine-implies-member2, 
equal-wf-T-base, 
less_than_transitivity1, 
le_weakening, 
less_than_transitivity2, 
le_weakening2, 
less_than_irreflexivity, 
bool_cases_sqequal, 
assert-bnot, 
neg_assert_of_eq_int, 
remove-combine-implies-member, 
remove-combine-l-ordered-implies-member, 
l_before_wf
\mforall{}s:nat-missing-type().  \mforall{}x,y:\mBbbN{}.
    (\muparrow{}member-nat-missing(x;add-nat-missing(y;s))  \mLeftarrow{}{}\mRightarrow{}  (x  =  y)  \mvee{}  (\muparrow{}member-nat-missing(x;s)))
Date html generated:
2015_07_17-AM-08_21_33
Last ObjectModification:
2015_04_02-PM-05_43_18
Home
Index