### 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