Nuprl Lemma : lifting-1-strict

[f:Top]. (lifting-1(f) {} {})


Proof




Definitions occuring in Statement :  lifting-1: lifting-1(f) empty-bag: {} uall: [x:A]. B[x] top: Top apply: a sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T lifting-1: lifting-1(f) lifting1: lifting1(f;b) lifting-gen-rev: lifting-gen-rev(n;f;bags) lifting-gen-list-rev: lifting-gen-list-rev(n;bags) ifthenelse: if then else fi  eq_int: (i =z j) bfalse: ff bag-combine: x∈bs.f[x] bag-union: bag-union(bbs) concat: concat(ll) reduce: reduce(f;k;as) list_ind: list_ind bag-map: bag-map(f;bs) map: map(f;as) so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]) so_apply: x[s1;s2;s3;s4] so_lambda: λ2x.t[x] top: Top so_apply: x[s] uimplies: supposing a strict4: strict4(F) and: P ∧ Q all: x:A. B[x] implies:  Q has-value: (a)↓ prop: guard: {T} or: P ∨ Q squash: T empty-bag: {} nil: [] it:
Lemmas referenced :  top_wf lifting-strict-ispair is-exception_wf base_wf has-value_wf_base lifting-strict-callbyvalue
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin baseClosed isect_memberEquality voidElimination voidEquality independent_isectElimination independent_pairFormation lambdaFormation callbyvalueCallbyvalue hypothesis callbyvalueReduce baseApply closedConclusion hypothesisEquality callbyvalueExceptionCases inrFormation imageMemberEquality imageElimination exceptionSqequal inlFormation because_Cache sqequalAxiom

Latex:
\mforall{}[f:Top].  (lifting-1(f)  \{\}  \msim{}  \{\})



Date html generated: 2016_05_15-PM-03_01_31
Last ObjectModification: 2016_01_16-AM-08_36_20

Theory : bags


Home Index