Nuprl Lemma : rel-is-immediate

[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  (∀x,y:T.  (R ⇐⇒ R+y)) supposing 
     ((∀a,b,c:T.  (((R b) ∧ (R c))  (b c ∈ T))) and 
     (∀x,y:T.  ((R+ y)  (R+ x)))))


Proof




Definitions occuring in Statement :  rel-immediate: R! rel_plus: R+ uimplies: supposing a uall: [x:A]. B[x] prop: all: x:A. B[x] iff: ⇐⇒ Q not: ¬A implies:  Q and: P ∧ Q apply: a function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a member: t ∈ T all: x:A. B[x] implies:  Q not: ¬A false: False subtype_rel: A ⊆B prop: and: P ∧ Q iff: ⇐⇒ Q rev_implies:  Q so_lambda: λ2x.t[x] so_apply: x[s] rel-immediate: R! cand: c∧ B infix_ap: y exists: x:A. B[x] or: P ∨ Q rel_plus: R+ nat_plus: + decidable: Dec(P) sq_type: SQType(T) guard: {T} rel_exp: R^n eq_int: (i =z j) subtract: m ifthenelse: if then else fi  bfalse: ff btrue: tt satisfiable_int_formula: satisfiable_int_formula(fmla) top: Top uiff: uiff(P;Q) less_than: a < b squash: T less_than': less_than'(a;b) true: True le: A ≤ B
Lemmas referenced :  rel_plus_wf rel-immediate_wf all_wf equal_wf not_wf rel-rel-plus rel_plus_iff2 rel_star_wf rel-star-iff-rel-plus-or nat_plus_properties decidable__equal_int subtype_base_sq int_subtype_base eq_int_wf satisfiable-full-omega-tt intformand_wf intformeq_wf itermVar_wf itermConstant_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_less_lemma int_formula_prop_wf assert_wf bnot_wf equal-wf-base bool_cases bool_wf bool_subtype_base eqtt_to_assert assert_of_eq_int eqff_to_assert iff_transitivity iff_weakening_uiff assert_of_bnot less_than_wf rel_exp_one rel_exp_wf nat_plus_subtype_nat subtract_wf decidable__lt false_wf not-lt-2 not-equal-2 less-iff-le add_functionality_wrt_le add-associates add-zero add-commutes zero-add le-add-cancel condition-implies-le minus-add add-swap minus-zero le-add-cancel2 minus-minus minus-one-mul minus-one-mul-top
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut introduction sqequalRule sqequalHypSubstitution lambdaEquality dependent_functionElimination thin hypothesisEquality voidElimination applyEquality extract_by_obid isectElimination cumulativity functionExtensionality hypothesis functionEquality universeEquality rename axiomEquality productEquality because_Cache lambdaFormation independent_pairFormation independent_functionElimination productElimination equalitySymmetry hyp_replacement Error :applyLambdaEquality,  unionElimination setElimination natural_numberEquality instantiate intEquality independent_isectElimination equalityTransitivity dependent_pairFormation int_eqEquality isect_memberEquality voidEquality computeAll baseClosed impliesFunctionality dependent_set_memberEquality imageMemberEquality addEquality minusEquality

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (\mforall{}x,y:T.    (R  x  y  \mLeftarrow{}{}\mRightarrow{}  R\msupplus{}!  x  y))  supposing 
          ((\mforall{}a,b,c:T.    (((R  a  b)  \mwedge{}  (R  a  c))  {}\mRightarrow{}  (b  =  c)))  and 
          (\mforall{}x,y:T.    ((R\msupplus{}  x  y)  {}\mRightarrow{}  (\mneg{}(R\msupplus{}  y  x)))))



Date html generated: 2016_10_25-AM-11_01_19
Last ObjectModification: 2016_07_12-AM-07_08_22

Theory : general


Home Index