Nuprl Lemma : lmax_com

s:DSet. ∀as,bs:|s| List.  (lmax(s;as;bs) ≡(|s|) lmax(s;bs;as))


Proof




Definitions occuring in Statement :  lmax: lmax(s;as;bs) permr: as ≡(T) bs list: List all: x:A. B[x] dset: DSet set_car: |p|
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  Q uall: [x:A]. B[x] dset: DSet true: True squash: T prop: subtype_rel: A ⊆B uimplies: supposing a guard: {T}
Lemmas referenced :  permr_iff_eq_counts lmax_wf set_car_wf list_wf dset_wf imax_com count_wf equal_wf squash_wf true_wf istype-universe count_lmax subtype_rel_self iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality hypothesis productElimination independent_functionElimination universeIsType isectElimination setElimination rename inhabitedIsType intEquality natural_numberEquality applyEquality lambdaEquality_alt imageElimination equalityTransitivity equalitySymmetry universeEquality sqequalRule imageMemberEquality baseClosed instantiate independent_isectElimination

Latex:
\mforall{}s:DSet.  \mforall{}as,bs:|s|  List.    (lmax(s;as;bs)  \mequiv{}(|s|)  lmax(s;bs;as))



Date html generated: 2019_10_16-PM-01_04_52
Last ObjectModification: 2018_10_08-AM-10_21_29

Theory : list_2


Home Index