Nuprl Lemma : pw-evenodd_wf
pw-evenodd() ∈ 𝔹 ⟶ Type
Proof
Definitions occuring in Statement :
pw-evenodd: pw-evenodd(),
bool: 𝔹,
member: t ∈ T,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
pw-evenodd: pw-evenodd(),
member: t ∈ T,
uall: ∀[x:A]. B[x],
so_lambda: λ2x.t[x],
prop: ℙ,
so_apply: x[s],
so_lambda: λ2x y.t[x; y],
all: ∀x:A. B[x],
implies: P ⇒ Q,
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_wf,
bool_wf,
equal-wf-T-base,
unit_wf2,
equal_wf,
bnot_wf
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesis,
lambdaEquality,
unionEquality,
hypothesisEquality,
baseClosed,
equalityTransitivity,
equalitySymmetry,
because_Cache,
lambdaFormation,
unionElimination,
voidEquality,
dependent_functionElimination,
independent_functionElimination
Latex:
pw-evenodd() \mmember{} \mBbbB{} {}\mrightarrow{} Type
Date html generated:
2019_06_20-PM-00_36_18
Last ObjectModification:
2018_08_21-PM-01_53_35
Theory : co-recursion
Home
Index