Twelf 1.5R3, Aug 30, 2005 (%trustme)
%% OK %%
[Opening file /home/www/twelf/hcode/05363637a446d6c1015c58b9a03e5aaf]
nat : type.
z : nat.
s : nat -> nat.
0 : nat = z.
1 : nat = s z.
2 : nat = s (s z).
3 : nat = s (s (s z)).
4 : nat = s (s (s (s z))).
5 : nat = s (s (s (s (s z)))).
6 : nat = s (s (s (s (s (s z))))).
succ : nat -> nat = [n:nat] s n.
sum : nat -> nat -> nat -> type.
%mode +{N:nat} +{M:nat} -{P:nat} (sum N M P).
sum/z : {M:nat} sum z M M.
sum/s : {N':nat} {M:nat} {P:nat} sum N' M P -> sum (s N') M (s P).
%worlds () (sum _ _ _).
%total N (sum N _ _).
mult : nat -> nat -> nat -> type.
%mode +{N:nat} +{M:nat} -{P:nat} (mult N M P).
mult/z : {M:nat} mult z M z.
mult/s :
   {M:nat} {P:nat} {P':nat} {N':nat}
      sum M P P' -> mult N' M P -> mult (s N') M P'.
%worlds () (mult _ _ _).
%total N (mult N _ _).
pow : nat -> nat -> nat -> type.
%mode +{N:nat} +{M:nat} -{P:nat} (pow N M P).
pow/z : {N:nat} pow N z (s z).
pow/s :
   {N:nat} {P:nat} {P':nat} {M:nat} mult N P P' -> pow N M P -> pow N (s M) P'.
%worlds () (pow _ _ _).
%total M (pow _ M _).
rel1 : nat -> nat -> type.
%mode +{N:nat} -{M:nat} (rel1 N M).
rel1/z : rel1 z (s z).
rel1/s :
   {N':nat} {P:nat} {P':nat} mult (s N') P P' -> rel1 N' P -> rel1 (s N') P'.
%worlds () (rel1 _ _).
%total N (rel1 N _).
rel2 : nat -> nat -> nat -> type.
%mode +{N:nat} +{M:nat} -{P:nat} (rel2 N M P).
rel2/z1 : {N:nat} rel2 N z N.
rel2/z2 : {M:nat} rel2 z M M.
rel2/s : {N:nat} {M:nat} {P:nat} rel2 N M P -> rel2 (s N) (s M) (s P).
%worlds () (rel2 _ _ _).
%total [N M] (rel2 N M _).
rel3 : nat -> nat -> type.
%mode +{N:nat} -{M:nat} (rel3 N M).
rel3/z : rel3 z (s z).
rel3/1 : rel3 (s z) (s z).
rel3/s :
   {P1:nat} {P2:nat} {P:nat} {N':nat}
      sum P1 P2 P -> rel3 (s N') P2 -> rel3 N' P1 -> rel3 (s (s N')) P.
%worlds () (rel3 _ _).
%total N (rel3 N _).
list : type.
nil : list.
cons : nat -> list -> list.
tree : type.
leaf : tree.
node : nat -> tree -> tree -> tree.
mytree : tree
   = node 2 leaf
        (node 1 (node 6 (node 5 leaf leaf) (node 2 (node 3 leaf leaf) leaf))
            leaf).
append : list -> list -> list -> type.
%mode +{L1:list} +{L2:list} -{L:list} (append L1 L2 L).
%worlds () (append _ _ _).
flip : tree -> tree -> type.
%mode +{T:tree} -{T':tree} (flip T T').
%worlds () (flip _ _).
infix : tree -> list -> type.
%mode +{T:tree} -{L:list} (infix T L).
infix/z : infix leaf nil.
infix/s :
   {L1:list} {N:nat} {L2:list} {L:list} {T2:tree} {T1:tree}
      append L1 (cons N L2) L -> infix T2 L2 -> infix T1 L1
         -> infix (node N T1 T2) L.
%worlds () (infix _ _).
[Closing file /home/www/twelf/hcode/05363637a446d6c1015c58b9a03e5aaf]
%% OK %%