Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)
%% OK %%
%% OK %%
%% OK %%
[Opening file /home/www/twelfwiki/code/7b09cc13a2f0aeb4a4249561319dc6ad]
tree : type.
leaf : tree.
node : tree -> tree -> tree.
id-tree : tree -> tree -> type.
id-tree/refl : {T:tree} id-tree T T.
id-tree-sym : {T1:tree} {T2:tree} id-tree T1 T2 -> id-tree T2 T1 -> type.
%mode +{T1:tree} +{T2:tree} +{X1:id-tree T1 T2} -{X2:id-tree T2 T1}
   (id-tree-sym X1 X2).
- : {X1:tree} id-tree-sym id-tree/refl id-tree/refl.
%worlds () (id-tree-sym _ _).
%total {} (id-tree-sym _ _).
id-tree-trans :
   {T1:tree} {T2:tree} {T3:tree}
      id-tree T1 T2 -> id-tree T2 T3 -> id-tree T1 T3 -> type.
%mode +{T1:tree} +{T2:tree} +{T3:tree} +{X1:id-tree T1 T2} +{X2:id-tree T2 T3}
   -{X3:id-tree T1 T3} (id-tree-trans X1 X2 X3).
- : {X1:tree} id-tree-trans id-tree/refl id-tree/refl id-tree/refl.
%worlds () (id-tree-trans _ _ _).
%total {} (id-tree-trans _ _ _).
id-tree-node-cong :
   {T1:tree} {T1':tree} {T2:tree} {T2':tree}
      id-tree T1 T1' -> id-tree T2 T2' -> id-tree (node T1 T2) (node T1' T2')
         -> type.
%mode +{T1:tree} +{T1':tree} +{T2:tree} +{T2':tree} +{X1:id-tree T1 T1'}
   +{X2:id-tree T2 T2'} -{X3:id-tree (node T1 T2) (node T1' T2')}
   (id-tree-node-cong X1 X2 X3).
- :
   {X1:tree} {X2:tree} id-tree-node-cong id-tree/refl id-tree/refl id-tree/refl.
%worlds () (id-tree-node-cong _ _ _).
%total {} (id-tree-node-cong _ _ _).
id-tree-node-inv :
   {T1:tree} {T2:tree} {T1':tree} {T2':tree}
      id-tree (node T1 T2) (node T1' T2') -> id-tree T1 T1' -> id-tree T2 T2'
         -> type.
%mode +{T1:tree} +{T2:tree} +{T1':tree} +{T2':tree}
   +{X1:id-tree (node T1 T2) (node T1' T2')} -{X2:id-tree T1 T1'}
   -{X3:id-tree T2 T2'} (id-tree-node-inv X1 X2 X3).
- : {X1:tree} {X2:tree} id-tree-node-inv id-tree/refl id-tree/refl id-tree/refl.
%worlds () (id-tree-node-inv _ _ _).
%total {} (id-tree-node-inv _ _ _).
nat : type.
height : tree -> nat -> type.
height-respects-id :
   {T:tree} {N:nat} {T':tree} {N':nat}
      height T N -> id-tree T T' -> height T N' -> type.
%mode +{T:tree} +{N:nat} +{T':tree} -{N':nat} +{X1:height T N} +{X2:id-tree T T'}
   -{X3:height T N'} (height-respects-id X1 X2 X3).
%worlds () (height-respects-id _ _ _).
eq-tree : tree -> tree -> type.
eq-leaf : eq-tree leaf leaf.
eq-node :
   {T2:tree} {T2':tree} {T1:tree} {T1':tree}
      eq-tree T2 T2' -> eq-tree T1 T1' -> eq-tree (node T1 T2) (node T1' T2').
eq-refl : {T:tree} eq-tree T T.
eq-sym : {T2:tree} {T1:tree} eq-tree T2 T1 -> eq-tree T1 T2.
eq-trans :
   {T2:tree} {T3:tree} {T1:tree} eq-tree T2 T3 -> eq-tree T1 T2 -> eq-tree T1 T3.
eq-node-inv-1 :
   {T1:tree} {T2:tree} {T1':tree} {T2':tree}
      eq-tree (node T1 T2) (node T1' T2') -> eq-tree T1 T1'.
eq-node-inv-2 :
   {T1:tree} {T2:tree} {T1':tree} {T2':tree}
      eq-tree (node T1 T2) (node T1' T2') -> eq-tree T2 T2'.
nat : type.
z : nat.
s : nat -> nat.
tree : type.
leaf : tree.
node : tree -> nat -> tree -> tree.
id-tree : tree -> tree -> type.
id-tree/refl : {T:tree} id-tree T T.
id-nat : nat -> nat -> type.
id-nat/refl : {T:nat} id-nat T T.
id-tree-node-cong :
   {T1:tree} {T1':tree} {T2:tree} {T2':tree} {N:nat} {N':nat}
      id-tree T1 T1' -> id-tree T2 T2' -> id-nat N N'
         -> id-tree (node T1 N T2) (node T1' N' T2') -> type.
%mode +{T1:tree} +{T1':tree} +{T2:tree} +{T2':tree} +{N:nat} +{N':nat}
   +{X1:id-tree T1 T1'} +{X2:id-tree T2 T2'} +{X3:id-nat N N'}
   -{X4:id-tree (node T1 N T2) (node T1' N' T2')}
   (id-tree-node-cong X1 X2 X3 X4).
- :
   {X1:tree} {X2:tree} {X3:nat} {X4:id-tree X1 X1} {X5:id-tree X2 X2}
      {X6:id-nat X3 X3} id-tree-node-cong X4 X5 X6 id-tree/refl.
%worlds () (id-tree-node-cong _ _ _ _).
%total {} (id-tree-node-cong _ _ _ _).
[Closing file /home/www/twelfwiki/code/7b09cc13a2f0aeb4a4249561319dc6ad]
%% OK %%