Nuprl Lemma : omralist_cases

g:OCMon. ∀r:CDRng. ∀Q:|omral(g;r)| ⟶ ℙ.
  (Q[[]]
   (∀ws:|omral(g;r)|. ∀x:|g|. ∀y:|r|.  ((↑before(x;map(λx.(fst(x));ws)))  (y 0 ∈ |r|))  Q[[<x, y> ws]]))
   {∀ws:|omral(g;r)|. Q[ws]})


Proof




Definitions occuring in Statement :  omralist: omral(g;r) before: before(u;ps) map: map(f;as) cons: [a b] nil: [] assert: b prop: guard: {T} so_apply: x[s] pi1: fst(t) all: x:A. B[x] not: ¬A implies:  Q lambda: λx.A[x] function: x:A ⟶ B[x] pair: <a, b> equal: t ∈ T cdrng: CDRng rng_zero: 0 rng_car: |r| oset_of_ocmon: g↓oset ocmon: OCMon grp_car: |g| set_car: |p|
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T uall: [x:A]. B[x] subtype_rel: A ⊆B ocmon: OCMon omon: OMon so_lambda: λ2x.t[x] prop: and: P ∧ Q abmonoid: AbMon mon: Mon so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt band: p ∧b q ifthenelse: if then else fi  uiff: uiff(P;Q) uimplies: supposing a bfalse: ff infix_ap: y so_apply: x[s] cand: c∧ B oset_of_ocmon: g↓oset dset_of_mon: g↓set set_car: |p| pi1: fst(t) add_grp_of_rng: r↓+gp grp_car: |g| grp_id: e pi2: snd(t) omralist: omral(g;r)
Lemmas referenced :  oalist_cases_a oset_of_ocmon_wf subtype_rel_sets abmonoid_wf ulinorder_wf grp_car_wf assert_wf infix_ap_wf bool_wf grp_le_wf equal_wf grp_eq_wf eqtt_to_assert cancel_wf grp_op_wf uall_wf monot_wf cdrng_wf ocmon_wf cdrng_is_abdmonoid
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin isectElimination hypothesisEquality applyEquality sqequalRule instantiate hypothesis because_Cache lambdaEquality productEquality setElimination rename cumulativity universeEquality functionEquality unionElimination equalityElimination productElimination independent_isectElimination equalityTransitivity equalitySymmetry independent_functionElimination setEquality independent_pairFormation

Latex:
\mforall{}g:OCMon.  \mforall{}r:CDRng.  \mforall{}Q:|omral(g;r)|  {}\mrightarrow{}  \mBbbP{}.
    (Q[[]]
    {}\mRightarrow{}  (\mforall{}ws:|omral(g;r)|.  \mforall{}x:|g|.  \mforall{}y:|r|.
                ((\muparrow{}before(x;map(\mlambda{}x.(fst(x));ws)))  {}\mRightarrow{}  (\mneg{}(y  =  0))  {}\mRightarrow{}  Q[[<x,  y>  /  ws]]))
    {}\mRightarrow{}  \{\mforall{}ws:|omral(g;r)|.  Q[ws]\})



Date html generated: 2017_10_01-AM-10_05_01
Last ObjectModification: 2017_03_03-PM-01_10_14

Theory : polynom_3


Home Index