### Nuprl Lemma : diamond-implies-TC-confluent

`∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].`
`  (rel-diamond-property(T;x,y.R[x;y])`
`  `` (∃m:T ⟶ ℕ. ∀x,y:T.  (R[x;y] `` m y < m x))`
`  `` rel-confluent(T;x,y.λx,y. R[x;y]^* x y))`

Proof

Definitions occuring in Statement :  rel-confluent: `rel-confluent(T;x,y.R[x; y])` rel-diamond-property: `rel-diamond-property(T;x,y.R[x; y])` transitive-reflexive-closure: `R^*` nat: `ℕ` less_than: `a < b` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` apply: `f a` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` rel-confluent: `rel-confluent(T;x,y.R[x; y])` exists: `∃x:A. B[x]` all: `∀x:A. B[x]` member: `t ∈ T` so_apply: `x[s1;s2]` subtype_rel: `A ⊆r B` prop: `ℙ` nat: `ℕ` so_lambda: `λ2x y.t[x; y]` and: `P ∧ Q` so_lambda: `λ2x.t[x]` so_apply: `x[s]` le: `A ≤ B` less_than': `less_than'(a;b)` not: `¬A` false: `False` guard: `{T}` ge: `i ≥ j ` decidable: `Dec(P)` or: `P ∨ Q` uimplies: `b supposing a` uiff: `uiff(P;Q)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top` infix_ap: `x f y` cand: `A c∧ B` transitive-reflexive-closure: `R^*` rel-diamond-property: `rel-diamond-property(T;x,y.R[x; y])` less_than: `a < b` squash: `↓T`
Lemmas referenced :  istype-nat subtype_rel_self istype-less_than rel-diamond-property_wf istype-universe transitive-reflexive-closure_wf subtract_wf istype-int primrec-wf2 less_than_wf add_nat_wf istype-void istype-le nat_properties decidable__le add-is-int-iff set_subtype_base le_wf int_subtype_base full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf itermAdd_wf intformeq_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_term_value_add_lemma int_formula_prop_eq_lemma int_formula_prop_wf false_wf decidable__lt intformless_wf int_formula_prop_less_lemma transitive-reflexive-closure-cases transitive-closure_wf itermSubtract_wf int_term_value_subtract_lemma transitive-reflexive-closure-base-case transitive-reflexive-closure_transitivity
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaFormation_alt sqequalRule productIsType functionIsType universeIsType hypothesisEquality cut introduction extract_by_obid hypothesis because_Cache applyEquality thin instantiate sqequalHypSubstitution isectElimination universeEquality lambdaEquality_alt setElimination rename inhabitedIsType productElimination natural_numberEquality setIsType functionEquality productEquality dependent_functionElimination dependent_set_memberEquality_alt addEquality independent_pairFormation voidElimination equalityTransitivity equalitySymmetry applyLambdaEquality unionElimination pointwiseFunctionality promote_hyp intEquality independent_isectElimination baseClosed approximateComputation independent_functionElimination dependent_pairFormation_alt int_eqEquality isect_memberEquality_alt equalityIstype hyp_replacement inlFormation_alt imageElimination

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
(rel-diamond-property(T;x,y.R[x;y])
{}\mRightarrow{}  (\mexists{}m:T  {}\mrightarrow{}  \mBbbN{}.  \mforall{}x,y:T.    (R[x;y]  {}\mRightarrow{}  m  y  <  m  x))
{}\mRightarrow{}  rel-confluent(T;x,y.\mlambda{}x,y.  R[x;y]\^{}*  x  y))

Date html generated: 2019_10_15-AM-10_24_43
Last ObjectModification: 2019_08_16-PM-03_15_24

Theory : relations2

Home Index