Nuprl Lemma : dep-all_wf

[n:ℕ]. ∀[P:nat-prop{i:l}(n)].  (dep-all(n;i.P[i]) ∈ ℙ)


Proof




Definitions occuring in Statement :  dep-all: dep-all(n;i.P[i]) nat-prop: nat-prop{i:l}(n) nat: uall: [x:A]. B[x] prop: so_apply: x[s] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T and: P ∧ Q all: x:A. B[x] nat: int_seg: {i..j-} lelt: i ≤ j < k decidable: Dec(P) or: P ∨ Q uimplies: supposing a not: ¬A implies:  Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False prop:
Lemmas referenced :  nat-prop-dep-all-wf decidable__lt full-omega-unsat intformnot_wf intformless_wf itermVar_wf itermAdd_wf itermConstant_wf istype-int int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_add_lemma int_term_value_constant_lemma int_formula_prop_wf istype-le istype-less_than istype-nat
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality productElimination dependent_functionElimination setElimination rename dependent_set_memberEquality_alt independent_pairFormation addEquality natural_numberEquality unionElimination independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation_alt lambdaEquality_alt int_eqEquality Error :memTop,  sqequalRule universeIsType voidElimination productIsType because_Cache axiomEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[P:nat-prop\{i:l\}(n)].    (dep-all(n;i.P[i])  \mmember{}  \mBbbP{})



Date html generated: 2020_05_19-PM-09_39_53
Last ObjectModification: 2020_03_04-PM-03_46_58

Theory : co-recursion-2


Home Index