Nuprl Lemma : hdf-buffer-transformation2
∀[init,L,G:Top]. ∀[m:ℕ].
  (hdf-buffer(fix((λmk-hdf.(inl (λa.cbva_seq(L[a]; λg.<mk-hdf, G[g]> m)))));init) 
  ~ fix((λmk-hdf,s. (inl (λa.cbva_seq(λn.if (n =z m) then mk_lambdas_fun(λg.∪f∈G[g].∪b∈s.f b;m) else L[a] n fi
                                      λg.<mk-hdf if bag-null(select_fun_last(g;m)) then s else select_fun_last(g;m) fi 
                                         , select_fun_last(g;m)
                                         > m + 1))))) 
    init)
Proof
Definitions occuring in Statement : 
hdf-buffer: hdf-buffer(X;bs)
, 
nat: ℕ
, 
ifthenelse: if b then t else f fi 
, 
eq_int: (i =z j)
, 
uall: ∀[x:A]. B[x]
, 
top: Top
, 
so_apply: x[s]
, 
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-combine: ∪x∈bs.f[x]
, 
bag-null: bag-null(bs)
, 
select_fun_last: select_fun_last(g;m)
, 
mk_lambdas_fun: mk_lambdas_fun(F;m)
, 
cbva_seq: cbva_seq(L; F; m)
Lemmas : 
lifting-strict-spread, 
has-value_wf_base, 
base_wf, 
is-exception_wf, 
lifting-strict-int_eq, 
top_wf, 
lifting-strict-decide, 
strict4-spread, 
lifting-strict-callbyvalueall, 
nat_properties, 
less_than_transitivity1, 
less_than_irreflexivity, 
ge_wf, 
less_than_wf, 
strictness-apply, 
lifting-strict-less, 
lifting-strict-ispair, 
lifting-strict-isaxiom, 
strictness-decide, 
bottom-sqle, 
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, 
le_weakening2, 
le_wf, 
eq_int_wf, 
bool_wf, 
eqtt_to_assert, 
assert_of_eq_int, 
le_weakening, 
eqff_to_assert, 
equal_wf, 
bool_cases_sqequal, 
subtype_base_sq, 
bool_subtype_base, 
assert-bnot, 
neg_assert_of_eq_int, 
nat_wf, 
cbva_seq-spread, 
cbva_seq_extend, 
set_subtype_base, 
int_subtype_base
\mforall{}[init,L,G:Top].  \mforall{}[m:\mBbbN{}].
    (hdf-buffer(fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.cbva\_seq(L[a];  \mlambda{}g.<mk-hdf,  G[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.\mcup{}f\mmember{}G[g].\mcup{}b\mmember{}s.f  b;m)
                                                                                  else  L[a]  n
                                                                                  fi  ;  \mlambda{}g.<mk-hdf 
                                                                                                    if  bag-null(select\_fun\_last(g;m))
                                                                                                    then  s
                                                                                                    else  select\_fun\_last(g;m)
                                                                                                    fi 
                                                                                                  ,  select\_fun\_last(g;m)
                                                                                                  >  m  +  1))))) 
        init)
Date html generated:
2015_07_17-AM-08_08_48
Last ObjectModification:
2015_06_19-PM-01_00_23
Home
Index