Nuprl Lemma : Wleq-Wmul

[A:Type]. ∀[B:A ⟶ Type].
  ∀zero,succ:A ⟶ 𝔹.
    ((∀a:A. ((↑(succ a))  (Unit ⊆B[a])))
     (∀a:A. (¬↑(zero a) ⇐⇒ B[a]))
     (∀w3,w2,w1:W(A;a.B[a]).  ((w1 ≤  w2)  ((w1 w3) ≤  (w2 w3)))))


Proof




Definitions occuring in Statement :  Wmul: (w1 w2) Wcmp: Wcmp(A;a.B[a];leq) W: W(A;a.B[a]) assert: b btrue: tt bool: 𝔹 subtype_rel: A ⊆B uall: [x:A]. B[x] infix_ap: y so_apply: x[s] all: x:A. B[x] iff: ⇐⇒ Q not: ¬A implies:  Q unit: Unit apply: a function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] implies:  Q member: t ∈ T so_lambda: λ2x.t[x] so_apply: x[s] prop: subtype_rel: A ⊆B uimplies: supposing a Wmul: (w1 w2) Wsup: Wsup(a;b) bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q ifthenelse: if then else fi  bfalse: ff exists: x:A. B[x] or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b false: False Wcmp: Wcmp(A;a.B[a];leq) infix_ap: y
Lemmas referenced :  W-induction all_wf W_wf infix_ap_wf Wcmp_wf btrue_wf Wmul_wf bool_wf eqtt_to_assert eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot iff_wf not_wf assert_wf subtype_rel_wf unit_wf2 Wcmp_transitivity Wadd_wf it_wf Wleq-Wadd Wleq-Wadd2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule lambdaEquality applyEquality functionExtensionality cumulativity because_Cache hypothesis functionEquality instantiate universeEquality independent_isectElimination independent_functionElimination unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination dependent_pairFormation promote_hyp dependent_functionElimination voidElimination

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].
    \mforall{}zero,succ:A  {}\mrightarrow{}  \mBbbB{}.
        ((\mforall{}a:A.  ((\muparrow{}(succ  a))  {}\mRightarrow{}  (Unit  \msubseteq{}r  B[a])))
        {}\mRightarrow{}  (\mforall{}a:A.  (\mneg{}\muparrow{}(zero  a)  \mLeftarrow{}{}\mRightarrow{}  B[a]))
        {}\mRightarrow{}  (\mforall{}w3,w2,w1:W(A;a.B[a]).    ((w1  \mleq{}    w2)  {}\mRightarrow{}  ((w1  *  w3)  \mleq{}    (w2  *  w3)))))



Date html generated: 2017_04_14-AM-07_45_05
Last ObjectModification: 2017_02_27-PM-03_16_20

Theory : co-recursion


Home Index