Nuprl Lemma : fixpoint-upper-bound

j:ℕ. ∀F:Top.  (F^j ⊥ ≤ fix(F))


Proof




Definitions occuring in Statement :  fun_exp: f^n nat: bottom: top: Top all: x:A. B[x] apply: a fix: fix(F) sqle: s ≤ t
Definitions unfolded in proof :  all: x:A. B[x] uall: [x:A]. B[x] member: t ∈ T nat: implies:  Q false: False ge: i ≥  guard: {T} uimplies: supposing a prop: top: Top decidable: Dec(P) or: P ∨ Q iff: ⇐⇒ Q and: P ∧ Q not: ¬A rev_implies:  Q uiff: uiff(P;Q) subtract: m subtype_rel: A ⊆B le: A ≤ B less_than': less_than'(a;b) true: True nat_plus: +
Lemmas referenced :  nat_properties less_than_transitivity1 less_than_irreflexivity ge_wf less_than_wf top_wf fun_exp0_lemma bottom-sqle decidable__le subtract_wf false_wf not-ge-2 less-iff-le condition-implies-le minus-one-mul zero-add minus-one-mul-top minus-add minus-minus add-associates add-swap add-commutes add_functionality_wrt_le add-zero le-add-cancel fun_exp_unroll_1 nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename introduction intWeakElimination natural_numberEquality independent_isectElimination independent_functionElimination voidElimination sqequalRule lambdaEquality dependent_functionElimination axiomSqleEquality isect_memberEquality voidEquality unionElimination independent_pairFormation productElimination addEquality applyEquality intEquality minusEquality because_Cache dependent_set_memberEquality sqleRule sqleReflexivity

Latex:
\mforall{}j:\mBbbN{}.  \mforall{}F:Top.    (F\^{}j  \mbot{}  \mleq{}  fix(F))



Date html generated: 2016_05_13-PM-04_07_22
Last ObjectModification: 2015_12_26-AM-11_03_59

Theory : fun_1


Home Index