Nuprl Lemma : utrans_imp_sp_utrans_b

[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ((∀[x,y:T].  R[x;y] supposing R[x;y])
   UniformlyTrans(T;a,b.R[a;b])
   {∀[a,b,c:T].  (strict_part(x,y.R[x;y];a;c)) supposing (strict_part(x,y.R[x;y];a;b) and R[b;c])})


Proof




Definitions occuring in Statement :  strict_part: strict_part(x,y.R[x; y];a;b) utrans: UniformlyTrans(T;x,y.E[x; y]) uimplies: supposing a uall: [x:A]. B[x] prop: guard: {T} so_apply: x[s1;s2] implies:  Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  strict_part: strict_part(x,y.R[x; y];a;b) guard: {T} utrans: UniformlyTrans(T;x,y.E[x; y]) uall: [x:A]. B[x] implies:  Q uimplies: supposing a and: P ∧ Q not: ¬A false: False member: t ∈ T prop: so_apply: x[s1;s2] subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  not_wf uall_wf isect_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation lambdaFormation independent_pairFormation cut thin sqequalHypSubstitution productElimination applyEquality functionExtensionality hypothesisEquality cumulativity hypothesis independent_functionElimination voidElimination productEquality lambdaEquality universeEquality introduction extract_by_obid isectElimination functionEquality because_Cache independent_isectElimination

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}[x,y:T].    R[x;y]  supposing  R[x;y])
    {}\mRightarrow{}  UniformlyTrans(T;a,b.R[a;b])
    {}\mRightarrow{}  \{\mforall{}[a,b,c:T].    (strict\_part(x,y.R[x;y];a;c))  supposing  (strict\_part(x,y.R[x;y];a;b)  and  R[b;c])\}\000C)



Date html generated: 2016_10_21-AM-09_43_02
Last ObjectModification: 2016_08_01-PM-09_48_59

Theory : rel_1


Home Index