Nuprl Lemma : un-half-squash-test
∀[P,Q,R:ℙ]. (((P ∧ R) ⇒ Q) ⇒ ⇃(R) ⇒ half-squash-stable(Q) ⇒ ⇃(P) ⇒ True ⇒ {Q ∧ ⇃(P) ∧ (∀n:ℕ. Q)})
Proof
Definitions occuring in Statement :
half-squash-stable: half-squash-stable(P),
quotient: x,y:A//B[x; y],
nat: ℕ,
uall: ∀[x:A]. B[x],
prop: ℙ,
guard: {T},
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
true: True
Definitions unfolded in proof :
cand: A c∧ B,
half-squash-stable: half-squash-stable(P),
all: ∀x:A. B[x],
so_apply: x[s],
so_lambda: λ2x.t[x],
uimplies: b supposing a,
so_apply: x[s1;s2],
so_lambda: λ2x y.t[x; y],
and: P ∧ Q,
prop: ℙ,
member: t ∈ T,
guard: {T},
implies: P ⇒ Q,
uall: ∀[x:A]. B[x]
Lemmas referenced :
trivial-quotient-true,
half-squash-stable_wf,
implies-quotient-true,
half-squash-stable__all,
half-squash-stable__half-squash,
nat_wf,
all_wf,
equiv_rel_true,
true_wf,
quotient_wf,
half-squash-stable__and
Rules used in proof :
independent_pairFormation,
universeEquality,
functionEquality,
promote_hyp,
cumulativity,
independent_functionElimination,
independent_isectElimination,
hypothesis,
lambdaEquality,
because_Cache,
productEquality,
hypothesisEquality,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
sqequalRule,
cut,
lambdaFormation,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[P,Q,R:\mBbbP{}].
(((P \mwedge{} R) {}\mRightarrow{} Q) {}\mRightarrow{} \00D9(R) {}\mRightarrow{} half-squash-stable(Q) {}\mRightarrow{} \00D9(P) {}\mRightarrow{} True {}\mRightarrow{} \{Q \mwedge{} \00D9(P) \mwedge{} (\mforall{}n:\mBbbN{}. Q)\})
Date html generated:
2017_09_29-PM-05_48_13
Last ObjectModification:
2017_08_30-AM-11_48_12
Theory : quot_1
Home
Index