Nuprl Lemma : hdf-once-transformation3

[L,G:Top]. ∀[m:ℕ].
  (hdf-once(fix((λmk-hdf.(inl a.cbva_seq(L[a]; λg.<mk-hdf, G[a;g]>m)))))) 
  fix((λmk-hdf.(inl a.cbva_seq(L[a]; λg.<case null(G[a;g]) of inl() => mk-hdf inr() => inr Ax G[a;g]>m))))))


Definitions occuring in Statement :  hdf-once: hdf-once(X) null: null(as) nat: uall: [x:A]. B[x] top: Top so_apply: x[s1;s2] so_apply: x[s] fix: fix(F) lambda: λx.A[x] pair: <a, b> decide: case of inl(x) => s[x] inr(y) => t[y] inr: inr  inl: inl x sqequal: t axiom: Ax cbva_seq: cbva_seq(L; F; m)
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T hdf-once: hdf-once(X) hdf-halted: hdf-halted(P) hdf-halt: hdf-halt() bag-null: bag-null(bs) ifthenelse: if then else fi  hdf-ap: X(a) mk-hdf: mk-hdf(s,m.G[s; m];st.H[st];s0) it: hdf-run: hdf-run(P) isr: isr(x) btrue: tt bfalse: ff so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]) so_apply: x[s1;s2;s3;s4] so_lambda: λ2x.t[x] top: Top so_apply: x[s] uimplies: supposing a strict4: strict4(F) and: P ∧ Q all: x:A. B[x] implies:  Q has-value: (a)↓ prop: guard: {T} or: P ∨ Q squash: T so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] nat: false: False ge: i ≥  satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] not: ¬A fun_exp: f^n primrec: primrec(n;b;c) null: null(as) cbva_seq: cbva_seq(L; F; m) callbyvalueall_seq: callbyvalueall_seq(L;G;F;n;m) le_int: i ≤j bnot: ¬bb lt_int: i <j decidable: Dec(P) nat_plus: + subtype_rel: A ⊆B

\mforall{}[L,G:Top].  \mforall{}[m:\mBbbN{}].
    (hdf-once(fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.cbva\_seq(L[a];  \mlambda{}g.<mk-hdf,  G[a;g]>  m)))))) 
    \msim{}  fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.cbva\_seq(L[a];  \mlambda{}g.<case  null(G[a;g])  of  inl()  =>  mk-hdf  |  inr()  =>  inr  Ax 
                                                                                        ,  G[a;g]
                                                                                        >  m))))))

Date html generated: 2016_05_16-AM-10_48_14
Last ObjectModification: 2016_01_17-AM-11_08_12

Theory : halting!dataflow

Home Index