Termination w.r.t. Q of the given QTRS could be proven:

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

flatten(nil) → nil
flatten(unit(x)) → flatten(x)
flatten(++(x, y)) → ++(flatten(x), flatten(y))
flatten(++(unit(x), y)) → ++(flatten(x), flatten(y))
flatten(flatten(x)) → flatten(x)
rev(nil) → nil
rev(unit(x)) → unit(x)
rev(++(x, y)) → ++(rev(y), rev(x))
rev(rev(x)) → x
++(x, nil) → x
++(nil, y) → y
++(++(x, y), z) → ++(x, ++(y, z))

Q is empty.

(1) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(++(x₁, x₂)) = x₁ + x₂   
POL(flatten(x₁)) = x₁   
POL(nil) = 0   
POL(rev(x₁)) = x₁   
POL(unit(x₁)) = 1 + x₁   

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

flatten(unit(x)) → flatten(x)
flatten(++(unit(x), y)) → ++(flatten(x), flatten(y))

(2) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

flatten(nil) → nil
flatten(++(x, y)) → ++(flatten(x), flatten(y))
flatten(flatten(x)) → flatten(x)
rev(nil) → nil
rev(unit(x)) → unit(x)
rev(++(x, y)) → ++(rev(y), rev(x))
rev(rev(x)) → x
++(x, nil) → x
++(nil, y) → y
++(++(x, y), z) → ++(x, ++(y, z))

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(++(x₁, x₂)) = x₁ + x₂   
POL(flatten(x₁)) = x₁   
POL(nil) = 1   
POL(rev(x₁)) = x₁   
POL(unit(x₁)) = x₁   

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

++(x, nil) → x
++(nil, y) → y

(4) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

flatten(nil) → nil
flatten(++(x, y)) → ++(flatten(x), flatten(y))
flatten(flatten(x)) → flatten(x)
rev(nil) → nil
rev(unit(x)) → unit(x)
rev(++(x, y)) → ++(rev(y), rev(x))
rev(rev(x)) → x
++(++(x, y), z) → ++(x, ++(y, z))

Q is empty.

(5) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(++(x₁, x₂)) = x₁ + x₂   
POL(flatten(x₁)) = 2·x₁   
POL(nil) = 2   
POL(rev(x₁)) = x₁   
POL(unit(x₁)) = 2·x₁   

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

flatten(nil) → nil

(6) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

flatten(++(x, y)) → ++(flatten(x), flatten(y))
flatten(flatten(x)) → flatten(x)
rev(nil) → nil
rev(unit(x)) → unit(x)
rev(++(x, y)) → ++(rev(y), rev(x))
rev(rev(x)) → x
++(++(x, y), z) → ++(x, ++(y, z))

Q is empty.

(7) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(++(x₁, x₂)) = 1 + x₁ + x₂   
POL(flatten(x₁)) = 2·x₁   
POL(nil) = 0   
POL(rev(x₁)) = x₁   
POL(unit(x₁)) = 2·x₁   

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

flatten(++(x, y)) → ++(flatten(x), flatten(y))

(8) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

flatten(flatten(x)) → flatten(x)
rev(nil) → nil
rev(unit(x)) → unit(x)
rev(++(x, y)) → ++(rev(y), rev(x))
rev(rev(x)) → x
++(++(x, y), z) → ++(x, ++(y, z))

Q is empty.

(9) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(++(x₁, x₂)) = x₁ + x₂   
POL(flatten(x₁)) = 1 + x₁   
POL(nil) = 0   
POL(rev(x₁)) = x₁   
POL(unit(x₁)) = x₁   

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

flatten(flatten(x)) → flatten(x)

(10) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

rev(nil) → nil
rev(unit(x)) → unit(x)
rev(++(x, y)) → ++(rev(y), rev(x))
rev(rev(x)) → x
++(++(x, y), z) → ++(x, ++(y, z))

Q is empty.

(11) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(++(x₁, x₂)) = x₁ + x₂   
POL(nil) = 2   
POL(rev(x₁)) = 2·x₁   
POL(unit(x₁)) = 2·x₁   

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

rev(nil) → nil

(12) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

rev(unit(x)) → unit(x)
rev(++(x, y)) → ++(rev(y), rev(x))
rev(rev(x)) → x
++(++(x, y), z) → ++(x, ++(y, z))

Q is empty.

(13) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(++(x₁, x₂)) = 2 + x₁ + x₂   
POL(rev(x₁)) = 2 + 2·x₁   
POL(unit(x₁)) = 2·x₁   

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

rev(unit(x)) → unit(x)
rev(rev(x)) → x

(14) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

rev(++(x, y)) → ++(rev(y), rev(x))
++(++(x, y), z) → ++(x, ++(y, z))

Q is empty.

(15) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(++(x₁, x₂)) = 1 + x₁ + x₂   
POL(rev(x₁)) = 2·x₁   

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

rev(++(x, y)) → ++(rev(y), rev(x))

(16) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

++(++(x, y), z) → ++(x, ++(y, z))

Q is empty.

(17) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(++(x₁, x₂)) = 2 + 2·x₁ + x₂   

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

++(++(x, y), z) → ++(x, ++(y, z))

(18) Obligation:

Q restricted rewrite system:
R is empty.
Q is empty.

(19) RisEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.

(20) TRUE

(21) RisEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.

(22) TRUE