Nuprl Lemma : lattice-fset-join_wf

[l:BoundedLattice]. ((∀x,y:Point(l).  Dec(x y ∈ Point(l)))  (∀[s:fset(Point(l))]. (\/(s) ∈ Point(l))))


Proof




Definitions occuring in Statement :  lattice-fset-join: \/(s) bdd-lattice: BoundedLattice lattice-point: Point(l) fset: fset(T) decidable: Dec(P) uall: [x:A]. B[x] all: x:A. B[x] implies:  Q member: t ∈ T equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T implies:  Q subtype_rel: A ⊆B bdd-lattice: BoundedLattice so_lambda: λ2x.t[x] prop: and: P ∧ Q so_apply: x[s] uimplies: supposing a all: x:A. B[x] iff: ⇐⇒ Q rev_implies:  Q fset: fset(T) quotient: x,y:A//B[x; y] nat: false: False ge: i ≥  not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] le: A ≤ B less_than': less_than'(a;b) guard: {T} decidable: Dec(P) or: P ∨ Q uiff: uiff(P;Q) cons: [a b] assert: b ifthenelse: if then else fi  btrue: tt lattice-fset-join: \/(s) bfalse: ff deq: EqDecider(T) squash: T true: True colength: colength(L) nil: [] it: sq_type: SQType(T) less_than: a < b so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] bool: 𝔹 unit: Unit eqof: eqof(d) bnot: ¬bb lattice: Lattice l_member: (x ∈ l) select: L[n] cand: c∧ B nat_plus: +
Lemmas referenced :  fset_wf lattice-point_wf subtype_rel_set bounded-lattice-structure_wf lattice-structure_wf lattice-axioms_wf bounded-lattice-structure-subtype bounded-lattice-axioms_wf decidable_wf equal_wf bdd-lattice_wf deq-exists nat_properties full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf istype-int int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf ge_wf istype-less_than non_neg_length set-equal_wf length_wf list_wf subtract-1-ge-0 istype-nat add_nat_wf length_wf_nat istype-void istype-le decidable__le add-is-int-iff intformnot_wf itermAdd_wf intformeq_wf int_formula_prop_not_lemma int_term_value_add_lemma int_formula_prop_eq_lemma false_wf decidable__lt list-cases product_subtype_list set-equal-nil null_nil_lemma length_of_nil_lemma reduce_nil_lemma lattice-0_wf null_cons_lemma set-equal-cons2 filter_wf5 bnot_wf l_member_wf less_than_wf squash_wf true_wf length-filter-bnot subtract_wf subtype_rel_self iff_weakening_equal length_of_cons_lemma itermSubtract_wf int_term_value_subtract_lemma btrue_wf member-implies-null-eq-bfalse nil_wf btrue_neq_bfalse colength-cons-not-zero colength_wf_list subtype_base_sq set_subtype_base int_subtype_base spread_cons_lemma decidable__equal_int le_wf reduce_cons_lemma filter_cons_lemma cons_wf filter_nil_lemma lattice-join_wf eqtt_to_assert safe-assert-deq eqff_to_assert bool_cases_sqequal bool_subtype_base assert-bnot iff_weakening_uiff assert_wf reduce_wf istype-universe lattice_wf lattice-join-idempotent lattice_properties cons_member bool_wf add_nat_plus nat_plus_properties select_wf member_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut lambdaFormation_alt sqequalHypSubstitution hypothesis sqequalRule axiomEquality equalityTransitivity equalitySymmetry universeIsType extract_by_obid isectElimination thin hypothesisEquality applyEquality instantiate lambdaEquality_alt productEquality cumulativity independent_isectElimination functionIsType because_Cache dependent_functionElimination isect_memberEquality_alt isectIsTypeImplies inhabitedIsType functionIsTypeImplies productElimination independent_functionElimination rename promote_hyp pointwiseFunctionalityForEquality pertypeElimination setElimination intWeakElimination natural_numberEquality approximateComputation dependent_pairFormation_alt int_eqEquality Error :memTop,  independent_pairFormation voidElimination dependent_set_memberEquality_alt addEquality applyLambdaEquality unionElimination pointwiseFunctionality baseApply closedConclusion baseClosed equalityIstype productIsType sqequalBase hypothesis_subsumption setIsType imageElimination imageMemberEquality universeEquality intEquality equalityElimination hyp_replacement

Latex:
\mforall{}[l:BoundedLattice].  ((\mforall{}x,y:Point(l).    Dec(x  =  y))  {}\mRightarrow{}  (\mforall{}[s:fset(Point(l))].  (\mbackslash{}/(s)  \mmember{}  Point(l))))



Date html generated: 2020_05_20-AM-08_43_40
Last ObjectModification: 2020_01_06-PM-00_12_04

Theory : lattices


Home Index