Nuprl Lemma : bigrel-induction-monotone

[T:Type]
  ∀P:(T ⟶ T ⟶ ℙ) ⟶ ℙ. ∀F:(T ⟶ T ⟶ ℙ) ⟶ T ⟶ T ⟶ ℙ.
    (rel-monotone{i:l}(T;R.F[R])
     (∀Rs:ℕ ⟶ T ⟶ T ⟶ ℙ((∀n:ℕRs[n 1] => Rs[n])  (∀n:ℕP[Rs[n]])  P[isect-rel(ℕ;n.Rs[n])]))
     (∀R:T ⟶ T ⟶ ℙ(P[R]  P[F[R]]))
     P[λx,y. True]
     P[∨R.F[R]])


Proof




Definitions occuring in Statement :  bigrel: R.F[R] rel-monotone: rel-monotone{i:l}(T;R.F[R]) isect-rel: isect-rel(T;i.R[i]) rel_implies: R1 => R2 nat: uall: [x:A]. B[x] prop: so_apply: x[s] all: x:A. B[x] implies:  Q true: True lambda: λx.A[x] function: x:A ⟶ B[x] add: m natural_number: $n universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] implies:  Q bigrel: R.F[R] so_lambda: λ2x.t[x] member: t ∈ T prop: so_apply: x[s] nat: decidable: Dec(P) or: P ∨ Q iff: ⇐⇒ Q and: P ∧ Q not: ¬A rev_implies:  Q false: False uiff: uiff(P;Q) uimplies: supposing a subtract: m subtype_rel: A ⊆B top: Top le: A ≤ B less_than': less_than'(a;b) true: True sq_stable: SqStable(P) squash: T eq_int: (i =z j) bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  bfalse: ff exists: x:A. B[x] sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b nequal: a ≠ b ∈  rel-monotone: rel-monotone{i:l}(T;R.F[R]) rel_implies: R1 => R2 infix_ap: y
Lemmas referenced :  primrec_wf true_wf int_seg_wf nat_wf rel_implies_wf subtract_wf decidable__le false_wf not-le-2 less-iff-le condition-implies-le minus-add minus-one-mul zero-add minus-one-mul-top minus-minus add-associates add-swap add-commutes add_functionality_wrt_le add-zero le-add-cancel le_wf set_wf less_than_wf primrec-wf2 sq_stable__le primrec-unroll btrue_wf eqtt_to_assert assert_of_eq_int eqff_to_assert eq_int_wf equal_wf bool_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int all_wf isect-rel_wf rel-monotone_wf bfalse_wf int_subtype_base primrec0_lemma le_antisymmetry_iff less_than_transitivity1 le_weakening less_than_irreflexivity not-equal-2 general_arith_equation1
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut hypothesis sqequalHypSubstitution dependent_functionElimination thin sqequalRule lambdaEquality instantiate introduction extract_by_obid isectElimination functionEquality cumulativity hypothesisEquality universeEquality applyEquality functionExtensionality natural_numberEquality setElimination rename independent_functionElimination because_Cache dependent_set_memberEquality addEquality unionElimination independent_pairFormation voidElimination productElimination independent_isectElimination minusEquality isect_memberEquality voidEquality intEquality imageMemberEquality baseClosed imageElimination equalityElimination equalityTransitivity equalitySymmetry dependent_pairFormation promote_hyp

Latex:
\mforall{}[T:Type]
    \mforall{}P:(T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{})  {}\mrightarrow{}  \mBbbP{}.  \mforall{}F:(T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{})  {}\mrightarrow{}  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.
        (rel-monotone\{i:l\}(T;R.F[R])
        {}\mRightarrow{}  (\mforall{}Rs:\mBbbN{}  {}\mrightarrow{}  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
                    ((\mforall{}n:\mBbbN{}.  Rs[n  +  1]  =>  Rs[n])  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  P[Rs[n]])  {}\mRightarrow{}  P[isect-rel(\mBbbN{};n.Rs[n])]))
        {}\mRightarrow{}  (\mforall{}R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.  (P[R]  {}\mRightarrow{}  P[F[R]]))
        {}\mRightarrow{}  P[\mlambda{}x,y.  True]
        {}\mRightarrow{}  P[\mvee{}R.F[R]])



Date html generated: 2017_04_14-AM-07_38_56
Last ObjectModification: 2017_02_27-PM-03_10_50

Theory : relations


Home Index