Nuprl Lemma : imax-imax-list-left
[L:
List
]. [x:]. (imax(imax-list(L);x) = imax-list(L @ [x]))
Proof not projected
Definitions occuring in Statement :
append: as @ bs,
imax: imax(a;b),
uall: [x:A]. B[x],
cons: [car / cdr],
nil: [],
int: ,
equal: s = t,
listp: A List,
imax-list: imax-list(L)
Lemmas :
select_wf,
decidable__equal_int,
int_subtype_base,
subtype_base_sq,
listp_wf,
listp_properties,
iff_wf,
rev_implies_wf,
imax-list-append2,
imax_wf,
imax-list_wf,
length_nil,
length_cons,
non_neg_length,
length_wf,
member_wf,
top_wf,
imax-list-unique,
nat_wf,
cons_member,
l_all_wf,
l_member_wf,
not_wf,
false_wf,
length_wf_nat,
le_wf,
true_wf,
squash_wf
\mforall{}[L:\mBbbZ{} List\msupplus{}]. \mforall{}[x:\mBbbZ{}]. (imax(imax-list(L);x) = imax-list(L @ [x]))
Date html generated:
2012_02_20-PM-05_58_55
Last ObjectModification:
2012_02_02-PM-02_30_31
Home
Index