Nuprl Lemma : decide2_wf
∀[T1,T2,T3,T4,T5:Type]. ∀[x:T1 + T2]. ∀[y:T3 + T4]. ∀[ll:T1 ⟶ T3 ⟶ T5]. ∀[lr:T1 ⟶ T4 ⟶ T5]. ∀[rl:T2 ⟶ T3 ⟶ T5].
∀[rr:T2 ⟶ T4 ⟶ T5].
(case x,y
of inl(a),inl(b) => ll[a;b]
| inl(a),inr(b) => lr[a;b]
| inr(a),inl(b) => rl[a;b]
| inr(a),inr(b) => rr[a;b] ∈ T5)
Proof
Definitions occuring in Statement :
decide2: decide2,
uall: ∀[x:A]. B[x],
so_apply: x[s1;s2],
member: t ∈ T,
function: x:A ⟶ B[x],
union: left + right,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
decide2: decide2,
all: ∀x:A. B[x],
implies: P ⇒ Q,
so_apply: x[s1;s2],
prop: ℙ
Lemmas referenced :
equal_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalRule,
hypothesisEquality,
equalityTransitivity,
hypothesis,
equalitySymmetry,
thin,
because_Cache,
lambdaFormation,
unionElimination,
applyEquality,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
dependent_functionElimination,
independent_functionElimination,
axiomEquality,
functionEquality,
isect_memberEquality,
unionEquality,
universeEquality
Latex:
\mforall{}[T1,T2,T3,T4,T5:Type]. \mforall{}[x:T1 + T2]. \mforall{}[y:T3 + T4]. \mforall{}[ll:T1 {}\mrightarrow{} T3 {}\mrightarrow{} T5]. \mforall{}[lr:T1 {}\mrightarrow{} T4 {}\mrightarrow{} T5].
\mforall{}[rl:T2 {}\mrightarrow{} T3 {}\mrightarrow{} T5]. \mforall{}[rr:T2 {}\mrightarrow{} T4 {}\mrightarrow{} T5].
(case x,y
of inl(a),inl(b) => ll[a;b]
| inl(a),inr(b) => lr[a;b]
| inr(a),inl(b) => rl[a;b]
| inr(a),inr(b) => rr[a;b] \mmember{} T5)
Date html generated:
2019_10_15-AM-11_14_45
Last ObjectModification:
2018_08_21-PM-01_59_31
Theory : general
Home
Index