### Nuprl Lemma : l_all_reduce

`∀[T:Type]. ∀[L:T List]. ∀[P:T ⟶ 𝔹].  uiff((∀x∈L.↑P[x]);↑reduce(λx,y. (P[x] ∧b y);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-}` sq_stable: `SqStable(P)` lelt: `i ≤ j < k` squash: `↓T` guard: `{T}` false: `False` true: `True` so_apply: `x[s1;s2]` so_lambda: `λ2x y.t[x; y]` it: `⋅` nil: `[]` select: `L[n]` rev_uimplies: `rev_uimplies(P;Q)` cand: `A c∧ B` or: `P ∨ Q` band: `p ∧b q` bfalse: `ff` iff: `P `⇐⇒` Q` rev_implies: `P `` Q`
Lemmas referenced :  list_induction uall_wf bool_wf uiff_wf l_all_wf assert_wf l_member_wf reduce_wf band_wf btrue_wf list_wf reduce_nil_lemma reduce_cons_lemma assert_witness select_wf sq_stable__le int_seg_wf length_wf true_wf less_than_irreflexivity less_than_transitivity1 all_wf base_wf stuck-spread length_of_nil_lemma assert_of_band bool_cases_sqequal l_all_cons cons_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality functionEquality hypothesis applyEquality setElimination rename setEquality independent_functionElimination dependent_functionElimination isect_memberEquality voidElimination voidEquality lambdaFormation because_Cache productElimination independent_pairEquality equalityTransitivity equalitySymmetry functionExtensionality cumulativity independent_isectElimination natural_numberEquality imageMemberEquality baseClosed imageElimination universeEquality axiomEquality independent_pairFormation productEquality unionElimination addLevel

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

Date html generated: 2019_06_20-PM-00_41_28
Last ObjectModification: 2018_08_24-PM-11_01_12

Theory : list_0

Home Index