### Nuprl Lemma : hdf-sqequal1

`∀[F:Top]. (hdf-base(m.F[m]) ~ fix((λmk-hdf.(inl (λm.<mk-hdf, F[m]>)))))`

Proof

Definitions occuring in Statement :  hdf-base: `hdf-base(m.F[m])` uall: `∀[x:A]. B[x]` top: `Top` so_apply: `x[s]` fix: `fix(F)` lambda: `λx.A[x]` pair: `<a, b>` inl: `inl x` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` hdf-base: `hdf-base(m.F[m])` mk-hdf: `mk-hdf(s,m.G[s; m];st.H[st];s0)` ifthenelse: `if b then t else f fi ` bfalse: `ff` hdf-run: `hdf-run(P)` so_apply: `x[s]` it: `⋅` all: `∀x:A. B[x]` guard: `{T}` int_seg: `{i..j-}` lelt: `i ≤ j < k` and: `P ∧ Q` uimplies: `b supposing a` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` implies: `P `` Q` not: `¬A` top: `Top` prop: `ℙ` decidable: `Dec(P)` or: `P ∨ Q` subtype_rel: `A ⊆r B` le: `A ≤ B` less_than': `less_than'(a;b)` nat: `ℕ` ge: `i ≥ j ` sq_type: `SQType(T)` so_lambda: `λ2x.t[x]`

Latex:
\mforall{}[F:Top].  (hdf-base(m.F[m])  \msim{}  fix((\mlambda{}mk-hdf.(inl  (\mlambda{}m.<mk-hdf,  F[m]>)))))

Date html generated: 2016_05_16-AM-10_44_55
Last ObjectModification: 2016_01_17-AM-11_12_23

Theory : halting!dataflow

Home Index