Nuprl Lemma : fixpoint-induction-bottom-bar
∀[E,S:Type]. (∀[G:S ⟶ bar(E)]. ∀[g:S ⟶ S]. (G[fix(g)] ∈ bar(E))) supposing ((⊥ ∈ S) and mono(E) and value-type(E))
Proof
Definitions occuring in Statement :
bar: bar(T),
mono: mono(T),
bottom: ⊥,
value-type: value-type(T),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
so_apply: x[s],
member: t ∈ T,
fix: fix(F),
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
bar: bar(T),
so_apply: x[s],
member: t ∈ T,
uall: ∀[x:A]. B[x],
uimplies: b supposing a
Lemmas referenced :
fixpoint-induction-bottom
Rules used in proof :
cut,
lemma_by_obid,
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
sqequalHypSubstitution,
hypothesis
Latex:
\mforall{}[E,S:Type].
(\mforall{}[G:S {}\mrightarrow{} bar(E)]. \mforall{}[g:S {}\mrightarrow{} S]. (G[fix(g)] \mmember{} bar(E))) supposing
((\mbot{} \mmember{} S) and
mono(E) and
value-type(E))
Date html generated:
2016_05_15-PM-10_04_45
Last ObjectModification:
2016_01_05-PM-06_48_38
Theory : bar!type
Home
Index