Nuprl Lemma : increasing-zero-seq

increasing-sequence(0s)


Proof




Definitions occuring in Statement :  increasing-sequence: increasing-sequence(a) zero-seq: 0s
Definitions unfolded in proof :  top: Top exists: x:A. B[x] satisfiable_int_formula: satisfiable_int_formula(fmla) uimplies: supposing a decidable: Dec(P) prop: implies:  Q not: ¬A false: False less_than': less_than'(a;b) and: P ∧ Q le: A ≤ B ge: i ≥  nat: member: t ∈ T uall: [x:A]. B[x] or: P ∨ Q all: x:A. B[x] increasing-sequence: increasing-sequence(a) zero-seq: 0s
Lemmas referenced :  nat_wf equal-wf-base int_formula_prop_wf decidable__equal_int int_term_value_constant_lemma int_formula_prop_eq_lemma int_formula_prop_not_lemma itermConstant_wf intformeq_wf intformnot_wf satisfiable-full-omega-tt le_wf false_wf decidable__equal_nat nat_properties
Rules used in proof :  baseClosed equalitySymmetry equalityTransitivity computeAll independent_functionElimination voidEquality voidElimination isect_memberEquality intEquality lambdaEquality dependent_pairFormation independent_isectElimination unionElimination because_Cache independent_pairFormation natural_numberEquality dependent_set_memberEquality dependent_functionElimination rename setElimination hypothesis hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid introduction cut inlFormation lambdaFormation sqequalRule sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
increasing-sequence(0s)



Date html generated: 2017_04_21-AM-11_23_11
Last ObjectModification: 2017_04_20-PM-04_50_05

Theory : continuity


Home Index