Nuprl Lemma : evodd-zero_wf
evodd-zero() ∈ pw-evenodd() tt
Proof
Definitions occuring in Statement :
evodd-zero: evodd-zero(),
pw-evenodd: pw-evenodd(),
btrue: tt,
member: t ∈ T,
apply: f a
Definitions unfolded in proof :
pw-evenodd: pw-evenodd(),
evodd-zero: evodd-zero(),
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],
so_apply: x[s1;s2],
so_lambda: so_lambda(x,y,z.t[x; y; z]),
so_apply: x[s1;s2;s3],
subtype_rel: A ⊆r B,
bnot: ¬bb,
ifthenelse: if b then t else f fi ,
btrue: tt
Lemmas referenced :
btrue_wf,
bnot_wf,
unit_wf2,
equal-wf-T-base,
bool_wf,
pW-sup_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
sqequalRule,
cut,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesis,
lambdaEquality,
unionEquality,
hypothesisEquality,
baseClosed,
because_Cache,
unionElimination,
voidEquality,
inlEquality,
axiomEquality,
applyEquality,
voidElimination
Latex:
evodd-zero() \mmember{} pw-evenodd() tt
Date html generated:
2016_05_14-AM-06_14_39
Last ObjectModification:
2016_01_14-PM-08_03_45
Theory : co-recursion
Home
Index