### Nuprl Lemma : same-final-iterate-one-one

`∀[A:Type]`
`  ∀f:A ⟶ (A + Top)`
`    (SWellFounded(p-graph(A;f) y x)`
`    `` ∀x,y:A.`
`         ∃n:ℕ. ((p-graph(A;f^n) x y) ∨ (p-graph(A;f^n) y x)) supposing final-iterate(f;x) = final-iterate(f;y) ∈ A `
`       supposing p-inject(A;A;f))`

Proof

Definitions occuring in Statement :  final-iterate: `final-iterate(f;x)` p-graph: `p-graph(A;f)` p-inject: `p-inject(A;B;f)` p-fun-exp: `f^n` strongwellfounded: `SWellFounded(R[x; y])` nat: `ℕ` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` top: `Top` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` or: `P ∨ Q` apply: `f a` function: `x:A ⟶ B[x]` union: `left + right` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` uimplies: `b supposing a` p-graph: `p-graph(A;f)` member: `t ∈ T` exists: `∃x:A. B[x]` cand: `A c∧ B` and: `P ∧ Q` nat: `ℕ` decidable: `Dec(P)` or: `P ∨ Q` prop: `ℙ` so_lambda: `λ2x y.t[x; y]` subtype_rel: `A ⊆r B` so_apply: `x[s1;s2]` ge: `i ≥ j ` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` so_lambda: `λ2x.t[x]` so_apply: `x[s]` guard: `{T}` le: `A ≤ B` subtract: `n - m` sq_type: `SQType(T)` p-inject: `p-inject(A;B;f)`
Lemmas referenced :  final-iterate-property decidable__le final-iterate_wf p-inject_wf strongwellfounded_wf p-graph_wf2 subtype_rel_self istype-top istype-universe subtract_wf nat_properties full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermSubtract_wf itermVar_wf istype-int 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_wf istype-le istype-assert can-apply_wf p-fun-exp_wf subtype_rel_dep_function top_wf subtype_rel_union do-apply_wf can-apply-fun-exp trivial-int-eq1 can-apply-fun-exp-add p-fun-exp-injection minus-one-mul add-commutes add-associates add-mul-special zero-mul zero-add subtype_base_sq int_subtype_base equal_wf assert_wf add-swap add-zero
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaFormation_alt sqequalRule cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality dependent_functionElimination independent_functionElimination hypothesis because_Cache productElimination setElimination rename unionElimination equalityIstype independent_isectElimination universeIsType lambdaEquality_alt applyEquality instantiate inhabitedIsType functionIsType unionIsType universeEquality dependent_pairFormation_alt dependent_set_memberEquality_alt natural_numberEquality approximateComputation int_eqEquality Error :memTop,  independent_pairFormation voidElimination inlFormation_alt productIsType unionEquality equalityTransitivity equalitySymmetry cumulativity intEquality applyLambdaEquality promote_hyp hyp_replacement functionEquality inrFormation_alt

Latex:
\mforall{}[A:Type]
\mforall{}f:A  {}\mrightarrow{}  (A  +  Top)
(SWellFounded(p-graph(A;f)  y  x)
{}\mRightarrow{}  \mforall{}x,y:A.
\mexists{}n:\mBbbN{}.  ((p-graph(A;f\^{}n)  x  y)  \mvee{}  (p-graph(A;f\^{}n)  y  x))
supposing  final-iterate(f;x)  =  final-iterate(f;y)
supposing  p-inject(A;A;f))

Date html generated: 2020_05_20-AM-08_09_14
Last ObjectModification: 2020_01_28-PM-04_51_04

Theory : general

Home Index