### Nuprl Lemma : find_wf

`∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[as:T List]. ∀[d:T].  ((first a ∈ as s.t. P[a] else d) ∈ T)`

Proof

Definitions occuring in Statement :  find: `(first x ∈ as s.t. P[x] else d)` list: `T List` bool: `𝔹` uall: `∀[x:A]. B[x]` so_apply: `x[s]` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` find: `(first x ∈ as s.t. P[x] else d)` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s1;s2;s3]` so_apply: `x[s]` prop: `ℙ`
Lemmas referenced :  list_ind_wf list_wf filter_wf5 l_member_wf bool_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaEquality hypothesis applyEquality setElimination rename setEquality axiomEquality equalityTransitivity equalitySymmetry universeIsType isect_memberEquality because_Cache functionIsType functionEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[as:T  List].  \mforall{}[d:T].    ((first  a  \mmember{}  as  s.t.  P[a]  else  d)  \mmember{}  T)

Date html generated: 2019_10_15-AM-10_53_55
Last ObjectModification: 2018_09_27-AM-09_38_59

Theory : list!

Home Index