Nuprl Lemma : rel_exp_add-ext

[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 :  member: t ∈ T rel_exp_add complete_nat_ind_with_y complete_nat_measure_ind genrec: genrec bool_cases uall: [x:A]. B[x] so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]) so_apply: x[s1;s2;s3;s4] so_lambda: λ2x.t[x] top: Top so_apply: x[s] uimplies: supposing a strict4: strict4(F) and: P ∧ Q all: x:A. B[x] implies:  Q has-value: (a)↓ prop: guard: {T} or: P ∨ Q squash: T eq_int: (i =z j) btrue: tt bfalse: ff any: any x subtract: m
Lemmas referenced :  rel_exp_add lifting-strict-decide top_wf equal_wf has-value_wf_base base_wf is-exception_wf lifting-strict-int_eq complete_nat_ind_with_y complete_nat_measure_ind bool_cases
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut instantiate extract_by_obid hypothesis sqequalRule thin sqequalHypSubstitution isectElimination baseClosed isect_memberEquality voidElimination voidEquality independent_isectElimination independent_pairFormation lambdaFormation callbyvalueDecide hypothesisEquality equalityTransitivity equalitySymmetry unionEquality unionElimination sqleReflexivity dependent_functionElimination independent_functionElimination baseApply closedConclusion decideExceptionCases inrFormation because_Cache imageMemberEquality imageElimination exceptionSqequal inlFormation

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_19
Last ObjectModification: 2017_02_27-PM-03_10_11

Theory : relations


Home Index