Twelf 1.5R3, Aug 30, 2005 (%trustme)
%% OK %%
[Opening file /home/www/twelf/hcode/76f09faf5ece1b77c14e13b83b23acfd]
tp : type.
pos : (tp -> tp) -> type.
neg : (tp -> tp) -> type.
un : tp.
* : tp -> tp -> tp.
%infix right 11 *.
=> : tp -> tp -> tp.
%infix right 10 =>.
mu : {F:tp -> tp} pos ([x:tp] F x) -> tp.
pos_id : pos ([a:tp] a).
pos_un : pos ([a:tp] un).
pos_* :
   {F1:tp -> tp} {F2:tp -> tp}
      pos ([a:tp] F1 a) -> pos ([a:tp] F2 a) -> pos ([a:tp] F1 a * F2 a).
pos_=> :
   {F1:tp -> tp} {F2:tp -> tp}
      neg ([a:tp] F1 a) -> pos ([a:tp] F2 a) -> pos ([a:tp] F1 a => F2 a).
pos_mu :
   {F:tp -> tp -> tp} {X1:{a:tp} pos ([x:tp] F a x)}
      ({b:tp} pos ([a:tp] b) -> pos ([a:tp] F a b))
         -> pos ([a:tp] mu ([b:tp] F a b) (X1 a)).
neg_un : neg ([a:tp] un).
neg_* :
   {F1:tp -> tp} {F2:tp -> tp}
      neg ([a:tp] F1 a) -> neg ([a:tp] F2 a) -> neg ([a:tp] F1 a * F2 a).
neg_=> :
   {F1:tp -> tp} {F2:tp -> tp}
      pos ([a:tp] F1 a) -> neg ([a:tp] F2 a) -> neg ([a:tp] F1 a => F2 a).
neg_mu :
   {F:tp -> tp -> tp} {X1:{a:tp} pos ([x:tp] F a x)}
      ({b:tp} neg ([a:tp] b) -> neg ([a:tp] F a b))
         -> neg ([a:tp] mu ([b:tp] F a b) (X1 a)).
pos_vac : {F:tp} pos ([a:tp] F).
neg_vac : {F:tp} neg ([a:tp] F).
streams : tp
   = mu ([x:tp] mu ([y:tp] x * y) (pos_* pos_vac pos_id))
        (pos_mu ([y:tp] [py:pos ([a:tp] y)] pos_* pos_id py)).
proof1 : pos ([a:tp] un * un) = pos_* pos_un pos_un.
proof2 : pos ([a:tp] un * un) = pos_* pos_vac pos_un.
proof3 : pos ([a:tp] un * un) = pos_* pos_un pos_vac.
proof4 : pos ([a:tp] un * un) = pos_* pos_vac pos_vac.
proof5 : pos ([a:tp] un * un) = pos_vac.
[Closing file /home/www/twelf/hcode/76f09faf5ece1b77c14e13b83b23acfd]
%% OK %%