### Nuprl Lemma : l_all_exists_max

`∀[A:Type]. ∀[R:A ⟶ ℤ ⟶ ℙ].`
`  ((∀x:A. ∀n,m:ℤ.  (R[x;n] `` R[x;m] supposing n ≤ m)) `` (∀L:A List. ((∀x∈L.∃n:ℤ. R[x;n]) `` (∃n:ℤ. (∀x∈L.R[x;n])))))`

Proof

Definitions occuring in Statement :  l_all: `(∀x∈L.P[x])` list: `T List` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` le: `A ≤ B` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` int: `ℤ` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` all: `∀x:A. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` prop: `ℙ` so_apply: `x[s1;s2]` so_apply: `x[s]` uimplies: `b supposing a` exists: `∃x:A. B[x]` top: `Top` subtype_rel: `A ⊆r B` and: `P ∧ Q` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` cand: `A c∧ B` or: `P ∨ Q` decidable: `Dec(P)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` not: `¬A` l_all: `(∀x∈L.P[x])` int_seg: `{i..j-}` guard: `{T}` lelt: `i ≤ j < k` less_than: `a < b` squash: `↓T`
Lemmas referenced :  int_seg_wf int_formula_prop_less_lemma intformless_wf decidable__lt int_term_value_constant_lemma int_formula_prop_and_lemma itermConstant_wf intformand_wf length_wf int_seg_properties select_wf int_formula_prop_wf int_term_value_var_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma itermVar_wf intformle_wf intformnot_wf satisfiable-full-omega-tt decidable__le imax_ub imax_wf cons_wf l_all_cons and_wf l_all_wf_nil l_all_nil le_wf isect_wf all_wf list_wf l_member_wf exists_wf l_all_wf list_induction
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut thin lemma_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality functionEquality intEquality applyEquality setElimination rename hypothesis setEquality independent_functionElimination because_Cache dependent_functionElimination cumulativity universeEquality dependent_pairFormation natural_numberEquality isect_memberEquality voidElimination voidEquality productElimination addLevel impliesFunctionality existsFunctionality productEquality independent_pairFormation independent_isectElimination inlFormation unionElimination int_eqEquality computeAll imageElimination inrFormation

Latex:
\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  \mBbbZ{}  {}\mrightarrow{}  \mBbbP{}].
((\mforall{}x:A.  \mforall{}n,m:\mBbbZ{}.    (R[x;n]  {}\mRightarrow{}  R[x;m]  supposing  n  \mleq{}  m))
{}\mRightarrow{}  (\mforall{}L:A  List.  ((\mforall{}x\mmember{}L.\mexists{}n:\mBbbZ{}.  R[x;n])  {}\mRightarrow{}  (\mexists{}n:\mBbbZ{}.  (\mforall{}x\mmember{}L.R[x;n])))))

Date html generated: 2016_05_14-PM-02_45_46
Last ObjectModification: 2016_01_15-AM-07_35_48

Theory : list_1

Home Index