Nuprl Lemma : rel_exp_add

[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀m,n:ℕ.  ∀[x,y,z:T].  ((x R^m y)  (y R^n z)  (x R^m z))


Proof




Definitions occuring in Statement :  rel_exp: R^n nat: uall: [x:A]. B[x] prop: infix_ap: y all: x:A. B[x] implies:  Q function: x:A ⟶ B[x] add: m universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] so_lambda: λ2x.t[x] member: t ∈ T implies:  Q prop: nat: all: x:A. B[x] guard: {T} sq_stable: SqStable(P) squash: T so_apply: x[s] infix_ap: y subtype_rel: A ⊆B uimplies: supposing a le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) false: False not: ¬A int_seg: {i..j-} lelt: i ≤ j < k rel_exp: R^n or: P ∨ Q sq_type: SQType(T) uiff: uiff(P;Q) ifthenelse: if then else fi  btrue: tt iff: ⇐⇒ Q rev_implies:  Q bfalse: ff subtract: m ge: i ≥  top: Top nat_plus: + less_than: a < b true: True exists: x:A. B[x] cand: c∧ B bool: 𝔹 unit: Unit it: decidable: Dec(P)
Lemmas referenced :  complete_nat_ind_with_y all_wf nat_wf uall_wf infix_ap_wf rel_exp_wf add_nat_wf sq_stable__le equal_wf le_wf int_seg_wf int_seg_subtype_nat false_wf eq_int_wf assert_wf bnot_wf not_wf equal-wf-T-base bool_cases subtype_base_sq bool_wf bool_subtype_base eqtt_to_assert assert_of_eq_int eqff_to_assert iff_transitivity iff_weakening_uiff assert_of_bnot int_subtype_base and_wf subtract_wf minus-zero zero-add add-zero nat_properties add-associates add-mul-special zero-mul not-equal-implies-less subtype_rel_self less-iff-le add_functionality_wrt_le le_reflexive minus-one-mul-top one-mul add-commutes minus-one-mul mul-associates omega-shadow less_than_wf two-mul mul-distributes-right add-swap mul-distributes minus-add mul-commutes mul-swap not-le-2 le-add-cancel uiff_transitivity decidable__le general_arith_equation1 not-equal-2 condition-implies-le minus-minus decidable__lt not-lt-2 le-add-cancel-alt lelt_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut thin instantiate introduction extract_by_obid sqequalHypSubstitution isectElimination sqequalRule lambdaEquality hypothesis cumulativity hypothesisEquality because_Cache functionEquality universeEquality functionExtensionality applyEquality dependent_set_memberEquality addEquality setElimination rename lambdaFormation natural_numberEquality independent_functionElimination imageMemberEquality baseClosed imageElimination equalityTransitivity equalitySymmetry dependent_functionElimination independent_isectElimination independent_pairFormation productElimination intEquality unionElimination impliesFunctionality addLevel hyp_replacement applyLambdaEquality levelHypothesis multiplyEquality minusEquality isect_memberEquality voidElimination voidEquality promote_hyp dependent_pairFormation productEquality equalityElimination

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}m,n:\mBbbN{}.    \mforall{}[x,y,z:T].    ((x  R\^{}m  y)  {}\mRightarrow{}  (y  R\^{}n  z)  {}\mRightarrow{}  (x  rel\_exp(T;  R;  m  +  n)  z))



Date html generated: 2017_04_14-AM-07_38_14
Last ObjectModification: 2017_02_27-PM-03_10_26

Theory : relations


Home Index