Nuprl Lemma : ocmon_properties

g:OCMon
  (UniformLinorder(|g|;x,y.↑(x ≤b y))
  ∧ Cancel(|g|;|g|;*)
  ∧ (∀[z:|g|]. monot(|g|;x,y.↑(x ≤b y);λw.(z w)))
  ∧ IsEqFun(|g|;=b))


Proof




Definitions occuring in Statement :  ocmon: OCMon grp_op: * grp_le: b grp_eq: =b grp_car: |g| monot: monot(T;x,y.R[x; y];f) cancel: Cancel(T;S;op) ulinorder: UniformLinorder(T;x,y.R[x; y]) eqfun_p: IsEqFun(T;eq) assert: b uall: [x:A]. B[x] infix_ap: y all: x:A. B[x] and: P ∧ Q lambda: λx.A[x]
Definitions unfolded in proof :  all: x:A. B[x] ocmon: OCMon uall: [x:A]. B[x] member: t ∈ T and: P ∧ Q prop: abmonoid: AbMon mon: Mon so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] infix_ap: y so_lambda: λ2x.t[x] so_apply: x[s] implies:  Q sq_stable: SqStable(P) monot: monot(T;x,y.R[x; y];f) cancel: Cancel(T;S;op) uimplies: supposing a squash: T cand: c∧ B omon: OMon bool: 𝔹 unit: Unit it: btrue: tt band: p ∧b q ifthenelse: if then else fi  uiff: uiff(P;Q) bfalse: ff ulinorder: UniformLinorder(T;x,y.R[x; y]) uorder: UniformOrder(T;x,y.R[x; y]) utrans: UniformlyTrans(T;x,y.E[x; y]) uanti_sym: UniformlyAntiSym(T;x,y.R[x; y])
Lemmas referenced :  sq_stable__and ulinorder_wf grp_car_wf assert_wf infix_ap_wf bool_wf grp_le_wf equal_wf cancel_wf grp_op_wf uall_wf monot_wf sq_stable__equal grp_eq_wf squash_wf sq_stable__cancel sq_stable__uall sq_stable__monot sq_stable_from_decidable decidable__assert assert_witness omon_properties eqtt_to_assert ocmon_wf urefl_wf utrans_wf uanti_sym_wf connex_wf isect_wf sq_stable__urefl sq_stable__utrans sq_stable__uanti_sym sq_stable__connex
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution setElimination thin rename cut introduction extract_by_obid isectElimination productElimination productEquality because_Cache hypothesis sqequalRule lambdaEquality hypothesisEquality functionEquality functionExtensionality applyEquality equalityTransitivity equalitySymmetry isect_memberEquality independent_functionElimination dependent_functionElimination axiomEquality isect_memberFormation independent_pairEquality imageMemberEquality baseClosed imageElimination independent_pairFormation dependent_set_memberEquality unionElimination equalityElimination independent_isectElimination

Latex:
\mforall{}g:OCMon
    (UniformLinorder(|g|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
    \mwedge{}  Cancel(|g|;|g|;*)
    \mwedge{}  (\mforall{}[z:|g|].  monot(|g|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y);\mlambda{}w.(z  *  w)))
    \mwedge{}  IsEqFun(|g|;=\msubb{}))



Date html generated: 2017_10_01-AM-08_14_32
Last ObjectModification: 2017_02_28-PM-01_59_39

Theory : groups_1


Home Index