Nuprl Lemma : rel-is-immediate

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

Proof

Definitions occuring in Statement :  rel-immediate: `R!` rel_plus: `R+` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` prop: `ℙ` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` not: `¬A` implies: `P `` Q` and: `P ∧ Q` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` uimplies: `b supposing a` member: `t ∈ T` all: `∀x:A. B[x]` implies: `P `` Q` not: `¬A` false: `False` subtype_rel: `A ⊆r B` prop: `ℙ` and: `P ∧ Q` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` so_lambda: `λ2x.t[x]` so_apply: `x[s]` rel-immediate: `R!` cand: `A c∧ B` infix_ap: `x f 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: `n - m` ifthenelse: `if b then t else f 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