Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)
%% OK %%
%% OK %%
%% OK %%
[Opening file /home/www/twelfwiki/code/d6a3b283a95da8644d75feaedf3d9d39]
color : type.
color/red : color.
color/blue : color.
color/white : color.
colortree : type.
colortree/node : colortree -> colortree -> colortree.
colortree/leaf : color -> colortree.
recolor1 : color -> color -> type.
recolor1/rb : recolor1 color/red color/blue.
recolor1/bw : recolor1 color/blue color/white.
recolor1/wr : recolor1 color/white color/red.
recolor2 : color -> color -> type.
recolor2/rr : recolor2 color/red color/red.
recolor2/br : recolor2 color/blue color/red.
recolor2/wb : recolor2 color/white color/blue.
recolortree1 : colortree -> colortree -> type.
recolortree2 : colortree -> colortree -> type.
recolortree1/node :
   {TA:colortree} {TA':colortree} {TA'':colortree} {TB:colortree}
      recolortree2 TA TA' -> recolortree1 TA' TA''
         -> recolortree1 (colortree/node TA TB) (colortree/node TA'' TB).
recolortree1/leaf :
   {C1:color} {C2:color}
      recolor1 C1 C2 -> recolortree1 (colortree/leaf C1) (colortree/leaf C2).
recolortree2/node :
   {TB:colortree} {TB':colortree} {TB'':colortree} {TA:colortree}
      recolortree1 TB TB' -> recolortree2 TB' TB''
         -> recolortree2 (colortree/node TA TB) (colortree/node TA TB'').
recolortree2/leaf :
   {C1:color} {C2:color}
      recolor2 C1 C2 -> recolortree2 (colortree/leaf C1) (colortree/leaf C2).
can-recolor1 : {C':color} {C:color} recolor1 C C' -> type.
%mode -{C':color} +{D:color} -{D1:recolor1 D C'} (can-recolor1 D D1).
- : can-recolor1 color/red recolor1/rb.
- : can-recolor1 color/blue recolor1/bw.
- : can-recolor1 color/white recolor1/wr.
%worlds () (can-recolor1 _ _).
%total {} (can-recolor1 _ _).
can-recolor2 : {C':color} {C:color} recolor2 C C' -> type.
%mode -{C':color} +{D:color} -{D1:recolor2 D C'} (can-recolor2 D D1).
- : can-recolor2 color/red recolor2/rr.
- : can-recolor2 color/blue recolor2/br.
- : can-recolor2 color/white recolor2/wb.
%worlds () (can-recolor2 _ _).
%total {} (can-recolor2 _ _).
can-recolortree1 : {T:colortree} {T':colortree} recolortree1 T T' -> type.
%mode +{T:colortree} -{T':colortree} -{D1:recolortree1 T T'}
   (can-recolortree1 T T' D1).
can-recolortree2 : {T:colortree} {T':colortree} recolortree2 T T' -> type.
%mode +{T:colortree} -{T':colortree} -{D1:recolortree2 T T'}
   (can-recolortree2 T T' D1).
- :
   {T1':colortree} {T1'':colortree} {D2:recolortree1 T1' T1''} {T1:colortree}
      {D1:recolortree2 T1 T1'} {T2:colortree}
      can-recolortree1 T1' T1'' D2 -> can-recolortree2 T1 T1' D1
         -> can-recolortree1 (colortree/node T1 T2) (colortree/node T1'' T2)
               (recolortree1/node D1 D2).
%worlds () (can-recolortree1 _ _ _) (can-recolortree2 _ _ _).
tree : type.
tree/node : tree -> tree -> tree.
tree/leaf : tree.
colortree-shape : colortree -> tree -> type.
colortree-shape/node :
   {T1:colortree} {T1':tree} {T2:colortree} {T2':tree}
      colortree-shape T1 T1' -> colortree-shape T2 T2'
         -> colortree-shape (colortree/node T1 T2) (tree/node T1' T2').
colortree-shape/leaf : {X1:color} colortree-shape (colortree/leaf X1) tree/leaf.
can-colortree-shape : {C:colortree} {T:tree} colortree-shape C T -> type.
%mode +{C:colortree} -{T:tree} -{D1:colortree-shape C T} (can-colortree-shape C T D1).
- :
   {C2:colortree} {T2:tree} {D2:colortree-shape C2 T2} {C1:colortree} {T1:tree}
      {D1:colortree-shape C1 T1}
      can-colortree-shape C2 T2 D2 -> can-colortree-shape C1 T1 D1
         -> can-colortree-shape (colortree/node C1 C2) (tree/node T1 T2)
               (colortree-shape/node D1 D2).
- :
   {X1:color}
      can-colortree-shape (colortree/leaf X1) tree/leaf colortree-shape/leaf.
%worlds () (can-colortree-shape _ _ _).
%total C (can-colortree-shape C _ _).
can-recolortree1* :
   {CT:colortree} {CT':colortree} {T:tree}
      colortree-shape CT T -> colortree-shape CT' T -> recolortree1 CT CT'
         -> type.
%mode +{CT:colortree} -{CT':colortree} +{T:tree} +{D1:colortree-shape CT T}
   -{D2:colortree-shape CT' T} -{D3:recolortree1 CT CT'}
   (can-recolortree1* T D1 D2 D3).
can-recolortree2* :
   {CT:colortree} {CT':colortree} {T:tree}
      colortree-shape CT T -> colortree-shape CT' T -> recolortree2 CT CT'
         -> type.
%mode +{CT:colortree} -{CT':colortree} +{T:tree} +{D1:colortree-shape CT T}
   -{D2:colortree-shape CT' T} -{D3:recolortree2 CT CT'}
   (can-recolortree2* T D1 D2 D3).
- :
   {X1:colortree} {X2:colortree} {T1:tree} {DCS1':colortree-shape X1 T1}
      {DCS1'':colortree-shape X2 T1} {DR2:recolortree1 X1 X2} {X3:colortree}
      {DCS1:colortree-shape X3 T1} {DR1:recolortree2 X3 X1} {X4:colortree}
      {T2:tree} {DCS2:colortree-shape X4 T2}
      can-recolortree1* T1 DCS1' DCS1'' DR2
         -> can-recolortree2* T1 DCS1 DCS1' DR1
         -> can-recolortree1* (tree/node T1 T2) (colortree-shape/node DCS1 DCS2)
               (colortree-shape/node DCS1'' DCS2) (recolortree1/node DR1 DR2).
- :
   {X1:color} {X2:color} {DR:recolor1 X2 X1}
      can-recolor1 X2 DR
         -> can-recolortree1* tree/leaf colortree-shape/leaf
               colortree-shape/leaf (recolortree1/leaf DR).
- :
   {X1:colortree} {X2:colortree} {T2:tree} {DCS2':colortree-shape X1 T2}
      {DCS2'':colortree-shape X2 T2} {DR2:recolortree2 X1 X2} {X3:colortree}
      {DCS2:colortree-shape X3 T2} {DR1:recolortree1 X3 X1} {X4:colortree}
      {T1:tree} {DCS1:colortree-shape X4 T1}
      can-recolortree2* T2 DCS2' DCS2'' DR2
         -> can-recolortree1* T2 DCS2 DCS2' DR1
         -> can-recolortree2* (tree/node T1 T2) (colortree-shape/node DCS1 DCS2)
               (colortree-shape/node DCS1 DCS2'') (recolortree2/node DR1 DR2).
- :
   {X1:color} {X2:color} {DR:recolor2 X2 X1}
      can-recolor2 X2 DR
         -> can-recolortree2* tree/leaf colortree-shape/leaf
               colortree-shape/leaf (recolortree2/leaf DR).
%worlds () (can-recolortree1* _ _ _ _) (can-recolortree2* _ _ _ _).
%total (T1 T2) (can-recolortree1* T1 _ _ _) (can-recolortree2* T2 _ _ _).
can-recolortree1 : {T:colortree} {T':colortree} recolortree1 T T' -> type.
%mode +{T:colortree} -{T':colortree} -{D1:recolortree1 T T'}
   (can-recolortree1 T T' D1).
- :
   {CT:colortree} {X1:colortree} {T:tree} {DCS:colortree-shape CT T}
      {X2:colortree-shape X1 T} {DR:recolortree1 CT X1}
      can-recolortree1* T DCS X2 DR -> can-colortree-shape CT T DCS
         -> can-recolortree1 CT X1 DR.
%worlds () (can-recolortree1 _ _ _).
%total {} (can-recolortree1 _ _ _).
can-recolortree2 : {T:colortree} {T':colortree} recolortree2 T T' -> type.
%mode +{T:colortree} -{T':colortree} -{D1:recolortree2 T T'}
   (can-recolortree2 T T' D1).
- :
   {CT:colortree} {X1:colortree} {T:tree} {DCS:colortree-shape CT T}
      {X2:colortree-shape X1 T} {DR:recolortree2 CT X1}
      can-recolortree2* T DCS X2 DR -> can-colortree-shape CT T DCS
         -> can-recolortree2 CT X1 DR.
%worlds () (can-recolortree2 _ _ _).
%total {} (can-recolortree2 _ _ _).
[Closing file /home/www/twelfwiki/code/d6a3b283a95da8644d75feaedf3d9d39]
%% OK %%