Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)
%% OK %%
%% OK %%
%% OK %%
[Opening file /home/www/twelfwiki/code/1574d8dc13fa5ad3c5c94b99b966ed1f]
t : type.
pol : type = t -> t -> t.
opp : (t -> t -> t) -> t -> t -> t = [p:t -> t -> t] [pos:t] [neg:t] p neg pos.
tp : (t -> t -> t) -> type.
un : {P:t -> t -> t} tp ([x:t] [x1:t] P x x1).
* :
   {P:t -> t -> t}
      tp ([x:t] [x1:t] P x x1) -> tp ([x:t] [x1:t] P x x1)
         -> tp ([x:t] [x1:t] P x x1).
%infix right 11 *.
=> :
   {P:t -> t -> t}
      tp ([x:t] [x1:t] P x1 x) -> tp ([x:t] [x1:t] P x x1)
         -> tp ([x:t] [x1:t] P x x1).
%infix right 10 =>.
mu :
   {P:t -> t -> t}
      (tp ([x:t] [x1:t] P x x1) -> tp ([x:t] [x1:t] P x x1))
         -> tp ([x:t] [x1:t] P x x1).
pos_ind : type = {P:t -> t -> t} tp ([x:t] [x1:t] P x x1).
streams : {P:t -> t -> t} tp ([x:t] [x1:t] P x x1)
   = [P:t -> t -> t]
        mu
           ([x:tp ([x:t] [x1:t] P x x1)]
               mu ([y:tp ([x1:t] [x2:t] P x1 x2)] x * y)).
ones : {P:t -> t -> t} tp ([x:t] [x1:t] P x x1)
   = [P:t -> t -> t] mu ([x:tp ([x:t] [x1:t] P x x1)] un * un).
ex1 : {P:t -> t -> t} tp ([x:t] [x1:t] P x x1)
   = [P:t -> t -> t] mu ([x:tp ([x:t] [x1:t] P x x1)] un => x).
ex2 : {P:t -> t -> t} tp ([x:t] [x1:t] P x x1)
   = [P:t -> t -> t] mu ([x:tp ([x:t] [x1:t] P x x1)] (x => un) => x).
ex3 : {P:t -> t -> t} tp ([x:t] [x1:t] P x x1)
   = [P:t -> t -> t] mu ([x:tp ([x:t] [x1:t] P x x1)] (x * x => un) => x * x).
ex4 : {P:t -> t -> t} tp ([x:t] [x1:t] P x x1)
   = [P:t -> t -> t]
        mu
           ([x:tp ([x:t] [x1:t] P x x1)]
               mu ([y:tp ([x1:t] [x2:t] P x2 x1)] x => y) => x).
[Closing file /home/www/twelfwiki/code/1574d8dc13fa5ad3c5c94b99b966ed1f]
%% OK %%