Nuprl Lemma : rel-comp-star

[T:Type]. ∀[R,S:T ⟶ T ⟶ ℙ].  (R S)^* ⇐⇒ (R ((S R)^* S)) ∨ x,y. (x y ∈ T))


Proof




Definitions occuring in Statement :  rel-comp: (R1 R2) rel_equivalent: R1 ⇐⇒ R2 rel_or: R1 ∨ R2 rel_star: R^* uall: [x:A]. B[x] prop: lambda: λx.A[x] function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T rel_equivalent: R1 ⇐⇒ R2 all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q subtype_rel: A ⊆B prop: rev_implies:  Q rel_or: R1 ∨ R2 infix_ap: y rel_star: R^* exists: x:A. B[x] nat: guard: {T} or: P ∨ Q so_lambda: λ2x.t[x] so_apply: x[s] uimplies: supposing a not: ¬A false: False sq_type: SQType(T) uiff: uiff(P;Q) ifthenelse: if then else fi  btrue: tt bfalse: ff rel-comp: (R1 R2) decidable: Dec(P) sq_stable: SqStable(P) squash: T top: Top le: A ≤ B less_than': less_than'(a;b) true: True subtract: m cand: c∧ B bool: 𝔹 unit: Unit it: bnot: ¬bb assert: b ge: i ≥  int_upper: {i...}
Lemmas referenced :  rel-comp-exp rel_star_wf rel-comp_wf subtype_rel_self rel_or_wf equal_wf istype-universe eq_int_wf assert_wf bnot_wf not_wf equal-wf-base set_subtype_base le_wf istype-int int_subtype_base istype-assert istype-void 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 rel_exp_wf subtract_wf decidable__le istype-false not-le-2 not-equal-2 sq_stable__le add_functionality_wrt_le add-associates add-zero zero-add le-add-cancel condition-implies-le add-commutes minus-add minus-zero minus-one-mul minus-one-mul-top minus-minus add-swap istype-le le_antisymmetry_iff bool_cases_sqequal assert-bnot neg_assert_of_eq_int infix_ap_wf upper_subtype_nat nat_properties nequal-le-implies add-subtract-cancel iff_weakening_equal rel_star_weakening
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality Error :lambdaFormation_alt,  independent_pairFormation Error :universeIsType,  applyEquality sqequalRule instantiate universeEquality Error :lambdaEquality_alt,  Error :inhabitedIsType,  because_Cache Error :functionIsType,  productElimination dependent_functionElimination independent_functionElimination setElimination rename natural_numberEquality equalityTransitivity equalitySymmetry Error :inrFormation_alt,  intEquality independent_isectElimination baseClosed Error :equalityIstype,  sqequalBase unionElimination cumulativity Error :inlFormation_alt,  Error :productIsType,  Error :dependent_set_memberEquality_alt,  voidElimination imageMemberEquality imageElimination addEquality Error :isect_memberEquality_alt,  minusEquality Error :dependent_pairFormation_alt,  promote_hyp equalityElimination closedConclusion hypothesis_subsumption

Latex:
\mforall{}[T:Type].  \mforall{}[R,S:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (R  o  S)\^{}*  \mLeftarrow{}{}\mRightarrow{}  (R  o  ((S  o  R)\^{}*  o  S))  \mvee{}  (\mlambda{}x,y.  (x  =  y))



Date html generated: 2019_06_20-PM-00_31_28
Last ObjectModification: 2019_03_28-PM-03_48_44

Theory : relations


Home Index