Nuprl Lemma : bar-converges-not-diverges
∀[T:Type]. ∀[x:bar-base(T)]. ∀[a:T]. (x↓a ⇒ (¬x↑))
Proof
Definitions occuring in Statement :
bar-diverges: x↑,
bar-converges: x↓a,
bar-base: bar-base(T),
uall: ∀[x:A]. B[x],
not: ¬A,
implies: P ⇒ Q,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
implies: P ⇒ Q,
not: ¬A,
false: False,
bar-converges: x↓a,
exists: ∃x:A. B[x],
bar-diverges: x↑,
all: ∀x:A. B[x],
assert: ↑b,
ifthenelse: if b then t else f fi ,
isl: isl(x),
btrue: tt,
true: True,
prop: ℙ
Lemmas referenced :
assert_wf,
isl_wf,
unit_wf2,
bar-diverges_wf,
bar-converges_wf,
bar-base_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
lambdaFormation,
thin,
sqequalHypSubstitution,
productElimination,
dependent_functionElimination,
hypothesisEquality,
independent_functionElimination,
hypothesis,
natural_numberEquality,
hyp_replacement,
equalitySymmetry,
Error :applyLambdaEquality,
extract_by_obid,
isectElimination,
cumulativity,
sqequalRule,
voidElimination,
lambdaEquality,
because_Cache,
isect_memberEquality,
universeEquality
Latex:
\mforall{}[T:Type]. \mforall{}[x:bar-base(T)]. \mforall{}[a:T]. (x\mdownarrow{}a {}\mRightarrow{} (\mneg{}x\muparrow{}))
Date html generated:
2016_10_21-AM-09_47_26
Last ObjectModification:
2016_07_12-AM-05_07_32
Theory : co-recursion
Home
Index