Nuprl Lemma : hdf-union-halt
hdf-halt() + hdf-halt() ~ hdf-halt()
Proof
Definitions occuring in Statement : 
hdf-union: X + Y
, 
hdf-halt: hdf-halt()
, 
sqequal: s ~ t
Definitions unfolded in proof : 
hdf-union: X + Y
, 
mk-hdf: mk-hdf(s,m.G[s; m];st.H[st];s0)
, 
hdf-ap: X(a)
, 
hdf-halt: hdf-halt()
, 
callbyvalueall: callbyvalueall, 
evalall: evalall(t)
, 
bag-append: as + bs
, 
append: as @ bs
, 
list_ind: list_ind, 
bag-map: bag-map(f;bs)
, 
map: map(f;as)
, 
empty-bag: {}
, 
nil: []
, 
it: ⋅
, 
btrue: tt
, 
band: p ∧b q
, 
ifthenelse: if b then t else f fi 
Latex:
hdf-halt()  +  hdf-halt()  \msim{}  hdf-halt()
Date html generated:
2016_05_16-AM-10_42_10
Last ObjectModification:
2015_12_28-PM-07_42_49
Theory : halting!dataflow
Home
Index