Nuprl Lemma : diff_functionality_wrt_permr

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


Proof




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

Latex:
\mforall{}s:DSet.  \mforall{}as,as',bs,bs':|s|  List.
    ((as  \mequiv{}(|s|)  as')  {}\mRightarrow{}  (bs  \mequiv{}(|s|)  bs')  {}\mRightarrow{}  ((as  -  bs)  \mequiv{}(|s|)  (as'  -  bs')))



Date html generated: 2019_10_16-PM-01_04_23
Last ObjectModification: 2018_10_08-AM-11_16_18

Theory : list_2


Home Index