Nuprl Lemma : evodd-induction
∀[Q:b:𝔹 ⟶ (pw-evenodd() b) ⟶ ℙ]
((∀b:𝔹. ∀a:b = tt?. ∀f:case a of inl(x) => Void | inr(x) => Unit ⟶ (pw-evenodd() (¬bb)).
((∀x:case a of inl(x) => Void | inr(x) => Unit. Q[¬bb;f x]) ⇒ Q[b;pW-sup(a;f)]))
⇒ (∀b:𝔹. ∀n:pw-evenodd() b. Q[b;n]))
Proof
Definitions occuring in Statement :
pw-evenodd: pw-evenodd(),
pW-sup: pW-sup(a;f),
bnot: ¬bb,
btrue: tt,
bool: 𝔹,
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s1;s2],
all: ∀x:A. B[x],
implies: P ⇒ Q,
unit: Unit,
apply: f a,
function: x:A ⟶ B[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
union: left + right,
void: Void,
equal: s = t ∈ T
Definitions unfolded in proof :
pw-evenodd: pw-evenodd(),
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
member: t ∈ T,
so_lambda: λ2x.t[x],
prop: ℙ,
so_apply: x[s],
so_lambda: λ2x y.t[x; y],
all: ∀x:A. B[x],
so_apply: x[s1;s2],
so_lambda: so_lambda(x,y,z.t[x; y; z]),
so_apply: x[s1;s2;s3]
Lemmas referenced :
param-W-induction,
bool_wf,
equal-wf-T-base,
unit_wf2,
equal_wf,
bnot_wf,
all_wf,
param-W_wf,
pW-sup_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
lambdaFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesis,
sqequalRule,
lambdaEquality,
unionEquality,
hypothesisEquality,
baseClosed,
equalityTransitivity,
equalitySymmetry,
because_Cache,
unionElimination,
voidEquality,
dependent_functionElimination,
independent_functionElimination,
functionEquality,
applyEquality,
cumulativity,
universeEquality
Latex:
\mforall{}[Q:b:\mBbbB{} {}\mrightarrow{} (pw-evenodd() b) {}\mrightarrow{} \mBbbP{}]
((\mforall{}b:\mBbbB{}. \mforall{}a:b = tt?. \mforall{}f:case a of inl(x) => Void | inr(x) => Unit {}\mrightarrow{} (pw-evenodd() (\mneg{}\msubb{}b)).
((\mforall{}x:case a of inl(x) => Void | inr(x) => Unit. Q[\mneg{}\msubb{}b;f x]) {}\mRightarrow{} Q[b;pW-sup(a;f)]))
{}\mRightarrow{} (\mforall{}b:\mBbbB{}. \mforall{}n:pw-evenodd() b. Q[b;n]))
Date html generated:
2019_06_20-PM-00_36_20
Last ObjectModification:
2018_08_21-PM-01_53_41
Theory : co-recursion
Home
Index