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