### Nuprl Lemma : l_all_assert_iff_reduce

`∀[A:Type]. ∀[P:A ⟶ 𝔹]. ∀[L:A List].  uiff((∀x∈L.↑P[x]);↑reduce(λx,b. (P[x] ∧b b);tt;L))`

Proof

Definitions occuring in Statement :  l_all: `(∀x∈L.P[x])` reduce: `reduce(f;k;as)` list: `T List` band: `p ∧b q` assert: `↑b` btrue: `tt` bool: `𝔹` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` so_apply: `x[s]` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` so_apply: `x[s]` prop: `ℙ` implies: `P `` Q` all: `∀x:A. B[x]` top: `Top` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` l_all: `(∀x∈L.P[x])` int_seg: `{i..j-}` guard: `{T}` lelt: `i ≤ j < k` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` not: `¬A` less_than: `a < b` squash: `↓T` true: `True` subtype_rel: `A ⊆r B` iff: `P `⇐⇒` Q` rev_implies: `P `` Q`
Lemmas referenced :  assert_of_band iff_weakening_uiff false_wf int_term_value_add_lemma itermAdd_wf add-is-int-iff length_of_cons_lemma cons_wf l_all_cons and_wf true_wf length_of_nil_lemma nil_wf l_all_nil l_all_wf_nil int_seg_wf int_formula_prop_less_lemma intformless_wf decidable__lt int_formula_prop_wf int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermVar_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__le length_wf int_seg_properties select_wf assert_witness reduce_cons_lemma reduce_nil_lemma list_wf btrue_wf band_wf bool_wf reduce_wf l_member_wf assert_wf l_all_wf uiff_wf list_induction
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin lemma_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality applyEquality setElimination rename hypothesis setEquality independent_functionElimination dependent_functionElimination isect_memberEquality voidElimination voidEquality lambdaFormation because_Cache productElimination independent_pairEquality equalityTransitivity equalitySymmetry functionEquality cumulativity independent_isectElimination natural_numberEquality unionElimination dependent_pairFormation int_eqEquality intEquality independent_pairFormation computeAll imageElimination universeEquality axiomEquality addLevel addEquality pointwiseFunctionality promote_hyp baseApply closedConclusion baseClosed

Latex:
\mforall{}[A:Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:A  List].    uiff((\mforall{}x\mmember{}L.\muparrow{}P[x]);\muparrow{}reduce(\mlambda{}x,b.  (P[x]  \mwedge{}\msubb{}  b);tt;L))

Date html generated: 2016_05_14-PM-02_45_25
Last ObjectModification: 2016_01_15-AM-07_36_50

Theory : list_1

Home Index