Nuprl Lemma : hdf-compose1-transformation3
∀[f,L,S,G,init:Top]. ∀[m:ℕ].
  (f o (fix((λmk-hdf,s. (inl (λa.cbva_seq(L[s;a]; λg.<mk-hdf S[s;a;g], G[s;a;g]> m))))) init) 
  ~ fix((λmk-hdf,s. (inl (λa.cbva_seq(λn.if (n =z m) then mk_lambdas_fun(λg.bag-map(f;G[s;a;g]);m) else L[s;a] n fi
                                      λg.<mk-hdf S[s;a;partial_ap(g;m + 1;m)], select_fun_ap(g;m + 1;m)> m + 1))))) 
    init)
Proof
Definitions occuring in Statement : 
hdf-compose1: f o X
, 
nat: ℕ
, 
ifthenelse: if b then t else f fi 
, 
eq_int: (i =z j)
, 
uall: ∀[x:A]. B[x]
, 
top: Top
, 
so_apply: x[s1;s2;s3]
, 
so_apply: x[s1;s2]
, 
apply: f a
, 
fix: fix(F)
, 
lambda: λx.A[x]
, 
pair: <a, b>
, 
inl: inl x
, 
add: n + m
, 
natural_number: $n
, 
sqequal: s ~ t
, 
bag-map: bag-map(f;bs)
, 
select_fun_ap: select_fun_ap(g;n;m)
, 
partial_ap: partial_ap(g;n;m)
, 
mk_lambdas_fun: mk_lambdas_fun(F;m)
, 
cbva_seq: cbva_seq(L; F; m)
Lemmas : 
lifting-strict-decide, 
has-value_wf_base, 
base_wf, 
lifting-strict-int_eq, 
top_wf, 
lifting-strict-spread, 
strict4-spread, 
lifting-strict-callbyvalueall, 
nat_properties, 
less_than_transitivity1, 
less_than_irreflexivity, 
ge_wf, 
less_than_wf, 
nat_wf, 
fun_exp0_lemma, 
strictness-apply, 
bottom_diverge, 
decidable__le, 
subtract_wf, 
false_wf, 
not-ge-2, 
less-iff-le, 
condition-implies-le, 
minus-one-mul, 
zero-add, 
minus-add, 
minus-minus, 
add-associates, 
add-swap, 
add-commutes, 
add_functionality_wrt_le, 
add-zero, 
le-add-cancel, 
fun_exp_unroll_1, 
cbva_seq-spread, 
cbva_seq_extend, 
set_subtype_base, 
le_wf, 
int_subtype_base
\mforall{}[f,L,S,G,init:Top].  \mforall{}[m:\mBbbN{}].
    (f  o  (fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(L[s;a];  \mlambda{}g.<mk-hdf  S[s;a;g],  G[s;a;g]>  m)))))  init) 
    \msim{}  fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(\mlambda{}n.if  (n  =\msubz{}  m)
                                                                                  then  mk\_lambdas\_fun(\mlambda{}g.bag-map(f;G[s;a;g]);m)
                                                                                  else  L[s;a]  n
                                                                                  fi  ;  \mlambda{}g.<mk-hdf  S[s;a;partial\_ap(g;m  +  1;m)]
                                                                                                  ,  select\_fun\_ap(g;m  +  1;m)
                                                                                                  >  m  +  1))))) 
        init)
Date html generated:
2015_07_17-AM-08_08_41
Last ObjectModification:
2015_01_27-PM-00_08_00
Home
Index