%------------------------------------------------------------------------------
% File     : DAT001_1 : TPTP v10.0.0. Released v10.0.0.
% Domain   : Data Structures
% Problem  :
% Version  : Especial.
% English  :

% Refs     :
% Source   : [TPTP]
% Names    :

% Status   : Theorem
% Rating   : ? v10.0.0
% Syntax   : Number of formulae    :   40 (  20 unt;  18 typ;   0 def)
%            Number of atoms       :   26 (  21 equ)
%            Maximal formula atoms :    4 (   1 avg)
%            Number of connectives :    5 (   1   ~;   0   |;   2   &)
%                                         (   2 <=>;   0  =>;   0  <=;   0 <~>)
%            Maximal formula depth :   10 (   3 avg)
%            Maximal term depth    :    4 (   2 avg)
%            Number of types       :    4 (   3 usr;   0 ari;   3 dat;   0 cdt)
%            Number of type conns  :   19 (  12   >;   7   *;   0   +;   0  <<)
%            Number of predicates  :    2 (   1 usr;   0 prp; 2-2 aty)
%            Number of functors    :   14 (  14 usr;   3 con; 0-3 aty)
%            Number of variables   :   45 (  45   !;   0   ?;  45   :)
% SPC      : TF0_THM_EQU_NAR_DAT

% Comments :
%------------------------------------------------------------------------------
tff(nat_type,type-datatype,
    nat: $tType ).

tff(list_type,type-datatype,
    list: $tType ).

tff(tree_type,type-datatype,
    tree: $tType ).

tff(zero_type,type-datatype_constructor,
    zero: nat ).

tff(s_type,type-datatype_constructor,
    s: nat > nat ).

tff(nil_type,type-datatype_constructor,
    nil: list ).

tff(cons_type,type-datatype_constructor,
    cons: ( nat * list ) > list ).

tff(leaf_type,type-datatype_constructor,
    leaf: tree ).

tff(node_type,type-datatype_constructor,
    node: ( tree * nat * tree ) > tree ).

tff(add_type,type,
    add: ( nat * nat ) > nat ).

tff(1,axiom,
    ! [Y: nat] : ( add(zero,Y) = Y ) ).

tff(2,axiom,
    ! [X: nat,Y: nat] : ( add(s(X),Y) = s(add(X,Y)) ) ).

tff(app_type,type,
    app: ( list * list ) > list ).

tff(3,axiom,
    ! [R: list] : ( app(nil,R) = R ) ).

tff(4,axiom,
    ! [A: nat,L: list,R: list] : ( app(cons(A,L),R) = cons(A,app(L,R)) ) ).

tff(rev_type,type,
    rev: list > list ).

tff(5,axiom,
    rev(nil) = nil ).

tff(6,axiom,
    ! [X: nat,Xs: list] : ( rev(cons(X,Xs)) = app(rev(Xs),cons(X,nil)) ) ).

tff(flatten0_type,type,
    flatten0: tree > list ).

tff(7,axiom,
    flatten0(leaf) = nil ).

tff(8,axiom,
    ! [P: tree,X: nat,Q: tree] : ( flatten0(node(P,X,Q)) = app(flatten0(P),cons(X,flatten0(Q))) ) ).

tff(size_type,type,
    size: tree > nat ).

tff(9,axiom,
    size(leaf) = zero ).

tff(10,axiom,
    ! [P: tree,X: nat,Q: tree] : ( size(node(P,X,Q)) = s(add(size(P),size(Q))) ) ).

tff(flatten2_type,type,
    flatten2: ( tree * list ) > list ).

tff(11,axiom,
    ! [R: list] : ( flatten2(leaf,R) = R ) ).

tff(12,axiom,
    ! [P: tree,X: nat,Q: tree,R: list] : ( flatten2(node(P,X,Q),R) = flatten2(P,cons(X,flatten2(Q,R))) ) ).

tff(rotateLeft_type,type,
    rotateLeft: tree > tree ).

tff(13,axiom,
    rotateLeft(leaf) = leaf ).

tff(14,axiom,
    ! [P: tree,X: nat] : ( rotateLeft(node(P,X,leaf)) = node(P,X,leaf) ) ).

tff(15,axiom,
    ! [P: tree,X: nat,Q: tree,Y: nat,R: tree] : ( rotateLeft(node(P,X,node(Q,Y,R))) = rotateLeft(node(node(P,X,Q),Y,R)) ) ).

tff(rotateRight_type,type,
    rotateRight: tree > tree ).

tff(16,axiom,
    rotateRight(leaf) = leaf ).

tff(17,axiom,
    ! [P: tree,X: nat] : ( rotateRight(node(leaf,X,P)) = node(leaf,X,P) ) ).

tff(18,axiom,
    ! [P: tree,X: nat,Q: tree,Y: nat,R: tree] : ( rotateRight(node(node(P,X,Q),Y,R)) = rotateRight(node(P,X,node(Q,Y,R))) ) ).

tff(mirror_type,type,
    mirror: ( tree * tree ) > $o ).

tff(19,axiom,
    ! [T: tree] :
      ( mirror(leaf,T)
    <=> ( T = leaf ) ) ).

tff(20,axiom,
    ! [P: tree,X: nat,Q: tree] : ~ mirror(node(P,X,Q),leaf) ).

tff(21,axiom,
    ! [P1: tree,X1: nat,Q1: tree,P2: tree,X2: nat,Q2: tree] :
      ( mirror(node(P1,X1,Q1),node(P2,X2,Q2))
    <=> ( ( X1 = X2 )
        & mirror(P1,Q2)
        & mirror(Q1,P2) ) ) ).

tff(goal,conjecture,
    ! [X: tree] : ( flatten2(rotateRight(X),nil) = flatten2(X,nil) ) ).

%------------------------------------------------------------------------------