### Nuprl Lemma : rel_star_order

`∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (WellFnd{i}(T;x,y.x R y) `` Order(T;x,y.x (R^*) y))`

Proof

Definitions occuring in Statement :  rel_star: `R^*` order: `Order(T;x,y.R[x; y])` wellfounded: `WellFnd{i}(A;x,y.R[x; y])` uall: `∀[x:A]. B[x]` prop: `ℙ` infix_ap: `x f y` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` order: `Order(T;x,y.R[x; y])` and: `P ∧ Q` refl: `Refl(T;x,y.E[x; y])` all: `∀x:A. B[x]` member: `t ∈ T` uimplies: `b supposing a` cand: `A c∧ B` trans: `Trans(T;x,y.E[x; y])` prop: `ℙ` infix_ap: `x f y` anti_sym: `AntiSym(T;x,y.R[x; y])` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` iff: `P `⇐⇒` Q` or: `P ∨ Q` not: `¬A` false: `False` exists: `∃x:A. B[x]`
Lemmas referenced :  rel_star_weakening rel_star_transitivity rel_star_wf wellfounded_wf rel_plus_irreflexive rel_star_iff rel-star-rel-plus2 rel-star-rel-plus3
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation independent_pairFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality because_Cache independent_isectElimination hypothesis independent_functionElimination applyEquality sqequalRule lambdaEquality functionEquality cumulativity universeEquality dependent_functionElimination productElimination unionElimination voidElimination

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    (WellFnd\{i\}(T;x,y.x  R  y)  {}\mRightarrow{}  Order(T;x,y.x  rel\_star(T;  R)  y))

Date html generated: 2016_05_14-PM-03_53_58
Last ObjectModification: 2015_12_26-PM-06_56_17

Theory : relations2

Home Index