Nuprl Lemma : strong-continuity-test-bound-unroll
∀[T:Type]. ∀[M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ?)]. ∀[n:ℕ]. ∀[f,b:Top].
(strong-continuity-test-bound(M;n;f;b) ~ if (n =z 0) then inr Ax
if n - 1 <z b then inr Ax
if (n - 1 =z b) then inl b
if isl(M (n - 1) f) then inr Ax
else strong-continuity-test-bound(M;n - 1;f;b)
fi )
Proof
Definitions occuring in Statement :
strong-continuity-test-bound: strong-continuity-test-bound(M;n;f;b),
int_seg: {i..j-},
nat: ℕ,
ifthenelse: if b then t else f fi ,
isl: isl(x),
lt_int: i <z j,
eq_int: (i =z j),
uall: ∀[x:A]. B[x],
top: Top,
unit: Unit,
apply: f a,
function: x:A ⟶ B[x],
inr: inr x ,
inl: inl x,
union: left + right,
subtract: n - m,
natural_number: $n,
universe: Type,
sqequal: s ~ t,
axiom: Ax
Definitions unfolded in proof :
member: t ∈ T,
uall: ∀[x:A]. B[x],
nat: ℕ,
strong-continuity-test-bound: strong-continuity-test-bound(M;n;f;b),
top: Top
Lemmas referenced :
primrec-unroll,
unit_wf2,
int_seg_wf,
nat_wf,
top_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
lemma_by_obid,
hypothesis,
because_Cache,
functionEquality,
sqequalHypSubstitution,
isectElimination,
thin,
natural_numberEquality,
setElimination,
rename,
hypothesisEquality,
cumulativity,
unionEquality,
universeEquality,
isect_memberFormation,
introduction,
sqequalAxiom,
sqequalRule,
isect_memberEquality,
voidElimination,
voidEquality
Latex:
\mforall{}[T:Type]. \mforall{}[M:n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} T) {}\mrightarrow{} (\mBbbN{}?)]. \mforall{}[n:\mBbbN{}]. \mforall{}[f,b:Top].
(strong-continuity-test-bound(M;n;f;b) \msim{} if (n =\msubz{} 0) then inr Ax
if n - 1 <z b then inr Ax
if (n - 1 =\msubz{} b) then inl b
if isl(M (n - 1) f) then inr Ax
else strong-continuity-test-bound(M;n - 1;f;b)
fi )
Date html generated:
2016_05_19-AM-11_59_37
Last ObjectModification:
2016_05_17-AM-08_56_39
Theory : continuity
Home
Index