Nuprl Lemma : d-conv_wf

[r:CRng]. ∀[f,g:ℕ ⟶ |r|].  (d-conv(r;f;g) ∈ ℕ ⟶ |r|)


Proof




Definitions occuring in Statement :  d-conv: d-conv(r;f;g) nat: uall: [x:A]. B[x] member: t ∈ T function: x:A ⟶ B[x] crng: CRng rng_car: |r|
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T subtype_rel: A ⊆B uall: [x:A]. B[x] and: P ∧ Q nat: prop: uimplies: supposing a pi1: fst(t) pi2: snd(t) ge: i ≥  decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False implies:  Q not: ¬A top: Top nat_plus: + le: A ≤ B iff: ⇐⇒ Q rev_implies:  Q uiff: uiff(P;Q) less_than': less_than'(a;b) true: True d-conv: d-conv(r;f;g) crng: CRng rng: Rng so_lambda: λ2x.t[x] so_apply: x[s] cand: c∧ B
Lemmas referenced :  nat_wf two-factorizations_wf list-subtype-bag equal_wf subtype_rel_self subtype_rel_bag le_wf nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_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_formula_prop_wf mul_cancel_in_le decidable__lt false_wf not-lt-2 add_functionality_wrt_le add-commutes zero-add le-add-cancel less_than_wf itermMultiply_wf intformeq_wf int_term_value_mul_lemma int_formula_prop_eq_lemma bag-summation_wf rng_car_wf rng_plus_wf rng_zero_wf rng_times_wf rng_all_properties rng_plus_comm2 crng_wf
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation introduction extract_by_obid hypothesis applyEquality sqequalHypSubstitution sqequalRule isectElimination thin hypothesisEquality setEquality because_Cache productEquality setElimination rename independent_isectElimination intEquality natural_numberEquality productElimination multiplyEquality lambdaEquality independent_pairEquality dependent_set_memberEquality dependent_functionElimination unionElimination dependent_pairFormation int_eqEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll independent_functionElimination equalityTransitivity equalitySymmetry isect_memberFormation functionExtensionality axiomEquality functionEquality

Latex:
\mforall{}[r:CRng].  \mforall{}[f,g:\mBbbN{}  {}\mrightarrow{}  |r|].    (d-conv(r;f;g)  \mmember{}  \mBbbN{}  {}\mrightarrow{}  |r|)



Date html generated: 2018_05_21-PM-09_06_33
Last ObjectModification: 2017_07_26-PM-06_29_15

Theory : general


Home Index