Nuprl Lemma : rel_star_iff

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


Proof




Definitions occuring in Statement :  rel_star: R^* uall: [x:A]. B[x] prop: infix_ap: y all: x:A. B[x] exists: x:A. B[x] iff: ⇐⇒ Q or: P ∨ Q and: P ∧ Q function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  rel_star: R^* infix_ap: y uall: [x:A]. B[x] all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q exists: x:A. B[x] member: t ∈ T prop: so_lambda: λ2x.t[x] so_apply: x[s] rev_implies:  Q or: P ∨ Q cand: c∧ B nat: ge: i ≥  decidable: Dec(P) uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) false: False not: ¬A top: Top guard: {T} le: A ≤ B less_than': less_than'(a;b) rel_exp: R^n ifthenelse: if then else fi  eq_int: (i =z j) btrue: tt
Lemmas referenced :  false_wf infix_ap_wf less_than_wf add-subtract-cancel decidable__lt int_term_value_add_lemma itermAdd_wf le_wf int_formula_prop_wf int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_subtract_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma intformless_wf itermVar_wf itermSubtract_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__le nat_properties subtract_wf rel_exp_iff equal_wf and_wf or_wf rel_exp_wf nat_wf exists_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation lambdaFormation independent_pairFormation sqequalHypSubstitution productElimination thin cut lemma_by_obid isectElimination hypothesis lambdaEquality applyEquality hypothesisEquality unionElimination functionEquality cumulativity universeEquality dependent_functionElimination independent_functionElimination inlFormation dependent_pairFormation dependent_set_memberEquality setElimination rename natural_numberEquality independent_isectElimination int_eqEquality intEquality isect_memberEquality voidElimination voidEquality computeAll inrFormation addEquality because_Cache productEquality instantiate

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



Date html generated: 2016_05_14-PM-03_52_39
Last ObjectModification: 2016_01_14-PM-11_11_01

Theory : relations2


Home Index