### Nuprl Lemma : decidable__rel_exp_finite

`∀[T:Type]`
`  ((∀x,y:T.  Dec(x = y ∈ T))`
`  `` (∀[R:T ⟶ T ⟶ ℙ]. (rel_finite(T;R) `` (∀x,y:T.  Dec(x R y)) `` (∀k:ℕ. ∀x,y:T.  Dec(x R^k y)))))`

Proof

Definitions occuring in Statement :  rel_finite: `rel_finite(T;R)` rel_exp: `R^n` nat: `ℕ` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` prop: `ℙ` infix_ap: `x f y` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` all: `∀x:A. B[x]` rel_exp: `R^n` eq_int: `(i =z j)` subtract: `n - m` ifthenelse: `if b then t else f fi ` btrue: `tt` infix_ap: `x f y` member: `t ∈ T` prop: `ℙ` so_lambda: `λ2x.t[x]` nat: `ℕ` decidable: `Dec(P)` or: `P ∨ Q` uimplies: `b supposing a` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` not: `¬A` top: `Top` and: `P ∧ Q` so_apply: `x[s]` iff: `P `⇐⇒` Q` cand: `A c∧ B` subtype_rel: `A ⊆r B` rev_implies: `P `` Q` rel_finite: `rel_finite(T;R)` l_exists: `(∃x∈L. P[x])` int_seg: `{i..j-}` guard: `{T}` lelt: `i ≤ j < k` less_than: `a < b` squash: `↓T`
Lemmas referenced :  all_wf decidable_wf infix_ap_wf rel_exp_wf decidable__le subtract_wf satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermSubtract_wf itermVar_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_subtract_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf le_wf set_wf less_than_wf primrec-wf2 nat_wf rel_finite_wf equal_wf intformeq_wf int_formula_prop_eq_lemma or_wf exists_wf equal-wf-base int_subtype_base rel_exp_iff iff_wf decidable_functionality decidable__l_exists decidable__and2 select_wf int_seg_properties length_wf decidable__lt not_wf l_exists_iff l_member_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut thin sqequalRule hypothesis rename setElimination hypothesisEquality introduction extract_by_obid sqequalHypSubstitution isectElimination cumulativity lambdaEquality because_Cache instantiate universeEquality dependent_set_memberEquality dependent_functionElimination natural_numberEquality unionElimination independent_isectElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll functionExtensionality applyEquality functionEquality productElimination productEquality baseClosed inlFormation addLevel impliesFunctionality independent_functionElimination imageElimination inrFormation setEquality

Latex:
\mforall{}[T:Type]
((\mforall{}x,y:T.    Dec(x  =  y))
{}\mRightarrow{}  (\mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}]
(rel\_finite(T;R)  {}\mRightarrow{}  (\mforall{}x,y:T.    Dec(x  R  y))  {}\mRightarrow{}  (\mforall{}k:\mBbbN{}.  \mforall{}x,y:T.    Dec(x  rel\_exp(T;  R;  k)  y)))))

Date html generated: 2017_04_17-AM-09_26_33
Last ObjectModification: 2017_02_27-PM-05_28_04

Theory : relations2

Home Index