Nuprl Lemma : dma-neg-dM_opp

[I:fset(ℕ)]. ∀[x:names(I)].  (<1-x>= <x> ∈ Point(dM(I)))


Proof




Definitions occuring in Statement :  dM_opp: <1-x> dM_inc: <x> dM: dM(I) names: names(I) dma-neg: ¬(x) lattice-point: Point(l) fset: fset(T) nat: uall: [x:A]. B[x] equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T prop: squash: T subtype_rel: A ⊆B DeMorgan-algebra: DeMorganAlgebra so_lambda: λ2x.t[x] and: P ∧ Q guard: {T} uimplies: supposing a so_apply: x[s] dma-neg: ¬(x) record-select: r.x dM: dM(I) free-DeMorgan-algebra: free-DeMorgan-algebra(T;eq) mk-DeMorgan-algebra: mk-DeMorgan-algebra(L;n) record-update: r[x := v] ifthenelse: if then else fi  eq_atom: =a y btrue: tt dm-neg: ¬(x) lattice-extend: lattice-extend(L;eq;eqL;f;ac) lattice-fset-join: \/(s) reduce: reduce(f;k;as) list_ind: list_ind fset-image: f"(s) f-union: f-union(domeq;rngeq;s;x.g[x]) list_accum: list_accum dM_opp: <1-x> dmopp: <1-i> free-dl-inc: free-dl-inc(x) fset-singleton: {x} cons: [a b] nil: [] it: fset-union: x ⋃ y l-union: as ⋃ bs insert: insert(a;L) eval_list: eval_list(t) deq-member: x ∈b L bfalse: ff lattice-join: a ∨ b opposite-lattice: opposite-lattice(L) mk-bounded-distributive-lattice: mk-bounded-distributive-lattice mk-bounded-lattice: mk-bounded-lattice(T;m;j;z;o) so_lambda: λ2y.t[x; y] lattice-meet: a ∧ b free-DeMorgan-lattice: free-DeMorgan-lattice(T;eq) free-dist-lattice: free-dist-lattice(T; eq) fset-ac-glb: fset-ac-glb(eq;ac1;ac2) fset-minimals: fset-minimals(x,y.less[x; y]; s) fset-filter: {x ∈ P[x]} filter: filter(P;l) lattice-fset-meet: /\(s) fset-ac-lub: fset-ac-lub(eq;ac1;ac2) lattice-1: 1 lattice-0: 0 empty-fset: {} fset-minimal: fset-minimal(x,y.less[x; y];s;a) fset-null: fset-null(s) null: null(as) f-proper-subset-dec: f-proper-subset-dec(eq;xs;ys) band: p ∧b q deq-f-subset: deq-f-subset(eq) isl: isl(x) decidable__f-subset decidable__all_fset decidable_functionality iff_preserves_decidability iff_weakening_uiff fset-all-iff decidable__assert bnot: ¬bb decidable__fset-member assert-deq-fset-member deq-fset-member: a ∈b s bor: p ∨bq union-deq: union-deq(A;B;a;b) sumdeq: sumdeq(a;b) names-deq: NamesDeq int-deq: IntDeq eq_int: (i =z j) lattice-point: Point(l) bdd-distributive-lattice: BoundedDistributiveLattice true: True
Lemmas referenced :  neg-dM_opp equal_wf squash_wf true_wf istype-universe lattice-point_wf dM_wf subtype_rel_set DeMorgan-algebra-structure_wf lattice-structure_wf lattice-axioms_wf bounded-lattice-structure-subtype DeMorgan-algebra-structure-subtype subtype_rel_transitivity bounded-lattice-structure_wf bounded-lattice-axioms_wf uall_wf lattice-meet_wf lattice-join_wf DeMorgan-algebra-axioms_wf dm-neg_wf names_wf names-deq_wf dM_opp_wf subtype_rel-equal free-DeMorgan-lattice_wf fset_wf nat_wf decidable__f-subset decidable__all_fset decidable_functionality iff_preserves_decidability iff_weakening_uiff fset-all-iff decidable__assert decidable__fset-member assert-deq-fset-member
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality hyp_replacement equalitySymmetry sqequalRule applyEquality lambdaEquality_alt imageElimination equalityTransitivity universeIsType inhabitedIsType instantiate universeEquality productEquality independent_isectElimination cumulativity because_Cache natural_numberEquality imageMemberEquality baseClosed

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[x:names(I)].    (\mneg{}(ə-x>)  =  <x>)



Date html generated: 2019_11_04-PM-05_30_33
Last ObjectModification: 2018_11_08-AM-10_18_17

Theory : cubical!type!theory


Home Index