Problem:
if(true(),x,y) -> x
if(false(),x,y) -> y
if(x,y,y) -> y
if(if(x,y,z),u(),v()) -> if(x,if(y,u(),v()),if(z,u(),v()))
Proof:
Bounds Processor:
bound: 0
enrichment: match
automaton:
final states: {13,12,11,10,5}
transitions:
if0(3,4,2) -> 5*
if0(13,2,11) -> 5*
if0(4,10,3) -> 5*
if0(13,4,11) -> 5*
if0(3,2,11) -> 5*
if0(4,12,3) -> 5*
if0(12,10,13) -> 5*
if0(13,10,2) -> 5*
if0(3,4,11) -> 5*
if0(10,10,1) -> 5*
if0(4,10,12) -> 5*
if0(11,1,4) -> 5*
if0(12,12,13) -> 5*
if0(2,10,13) -> 5*
if0(12,2,10) -> 5*
if0(13,12,2) -> 5*
if0(3,10,2) -> 5*
if0(10,12,1) -> 5*
if0(4,12,12) -> 5*
if0(11,3,4) -> 5*
if0(1,1,4) -> 5*
if0(2,12,13) -> 5*
if0(2,2,10) -> 5*
if0(12,4,10) -> 5*
if0(3,12,2) -> 5*
if0(13,10,11) -> 5*
if0(1,3,4) -> 5*
if0(2,4,10) -> 5*
if0(13,12,11) -> 5*
if0(3,10,11) -> 5*
if0(10,1,3) -> 5*
if0(3,12,11) -> 5*
if0(10,3,3) -> 5*
if0(12,10,10) -> 5*
if0(13,1,13) -> 5*
if0(10,1,12) -> 5*
if0(11,11,4) -> 5*
if0(11,1,1) -> 5*
if0(12,12,10) -> 5*
if0(2,10,10) -> 5*
if0(3,1,13) -> 5*
if0(13,3,13) -> 5*
if0(4,1,2) -> 5*
if0(10,3,12) -> 5*
if0(11,13,4) -> 5*
if0(1,11,4) -> 5*
if0(11,3,1) -> 5*
if0(1,1,1) -> 5*
if0(2,12,10) -> 5*
if0(3,3,13) -> 5*
if0(4,3,2) -> 5*
if0(1,13,4) -> 5*
if0(1,3,1) -> 5*
if0(10,11,3) -> 5*
if0(4,1,11) -> 5*
if0(10,13,3) -> 5*
if0(4,3,11) -> 5*
if0(13,11,13) -> 5*
if0(13,1,10) -> 5*
if0(10,11,12) -> 5*
if0(11,11,1) -> 5*
if0(12,2,4) -> 5*
if0(13,13,13) -> 5*
if0(3,11,13) -> 5*
if0(3,1,10) -> 5*
if0(13,3,10) -> 5*
if0(4,11,2) -> 5*
if0(10,13,12) -> 5*
if0(11,13,1) -> 5*
if0(1,11,1) -> 5*
if0(12,4,4) -> 5*
if0(2,2,4) -> 5*
if0(3,13,13) -> 5*
if0(3,3,10) -> 5*
if0(4,13,2) -> 5*
if0(1,13,1) -> 5*
if0(2,4,4) -> 5*
if0(4,11,11) -> 5*
if0(11,2,3) -> 5*
if0(4,13,11) -> 5*
if0(11,4,3) -> 5*
if0(1,2,3) -> 5*
if0(12,10,4) -> 5*
if0(13,11,10) -> 5*
if0(1,4,3) -> 5*
if0(11,2,12) -> 5*
if0(12,12,4) -> 5*
if0(2,10,4) -> 5*
if0(12,2,1) -> 5*
if0(13,13,10) -> 5*
if0(3,11,10) -> 5*
if0(10,2,2) -> 5*
if0(4,2,13) -> 5*
if0(1,2,12) -> 5*
if0(11,4,12) -> 5*
if0(2,12,4) -> 5*
if0(12,4,1) -> 5*
if0(2,2,1) -> 5*
if0(3,13,10) -> 5*
if0(10,4,2) -> 5*
if0(4,4,13) -> 5*
if0(11,10,3) -> 5*
if0(1,4,12) -> 5*
if0(2,4,1) -> 5*
if0(10,2,11) -> 5*
if0(11,12,3) -> 5*
if0(1,10,3) -> 5*
if0(10,4,11) -> 5*
if0(1,12,3) -> 5*
if0(11,10,12) -> 5*
if0(12,10,1) -> 5*
if0(10,10,2) -> 5*
if0(13,1,4) -> 5*
if0(4,10,13) -> 5*
if0(11,12,12) -> 5*
if0(1,10,12) -> 5*
if0(12,12,1) -> 5*
if0(2,10,1) -> 5*
if0(10,12,2) -> 5*
if0(13,3,4) -> 5*
if0(3,1,4) -> 5*
if0(4,12,13) -> 5*
if0(4,2,10) -> 5*
if0(1,12,12) -> 5*
if0(2,12,1) -> 5*
if0(3,3,4) -> 5*
if0(10,10,11) -> 5*
if0(4,4,10) -> 5*
if0(12,1,3) -> 5*
if0(10,12,11) -> 5*
if0(12,3,3) -> 5*
if0(2,1,3) -> 5*
if0(2,3,3) -> 5*
if0(12,1,12) -> 5*
if0(10,1,13) -> 5*
if0(13,11,4) -> 5*
if0(13,1,1) -> 5*
if0(4,10,10) -> 5*
if0(11,1,2) -> 5*
if0(2,1,12) -> 5*
if0(12,3,12) -> 5*
if0(10,3,13) -> 5*
if0(13,13,4) -> 5*
if0(3,11,4) -> 5*
if0(13,3,1) -> 5*
if0(3,1,1) -> 5*
if0(4,12,10) -> 5*
if0(11,3,2) -> 5*
if0(1,1,2) -> 5*
if0(2,3,12) -> 5*
if0(3,13,4) -> 5*
if0(3,3,1) -> 5*
if0(1,3,2) -> 5*
if0(11,1,11) -> 5*
if0(12,11,3) -> 5*
if0(1,1,11) -> 5*
if0(11,3,11) -> 5*
if0(12,13,3) -> 5*
if0(2,11,3) -> 5*
if0(1,3,11) -> 5*
if0(2,13,3) -> 5*
if0(12,11,12) -> 5*
if0(10,11,13) -> 5*
if0(10,1,10) -> 5*
if0(13,11,1) -> 5*
if0(11,11,2) -> 5*
if0(12,13,12) -> 5*
if0(2,11,12) -> 5*
if0(10,13,13) -> 5*
if0(10,3,10) -> 5*
if0(13,13,1) -> 5*
if0(3,11,1) -> 5*
if0(11,13,2) -> 5*
if0(1,11,2) -> 5*
if0(4,2,4) -> 5*
if0(2,13,12) -> 5*
if0(3,13,1) -> 5*
if0(1,13,2) -> 5*
if0(4,4,4) -> 5*
if0(11,11,11) -> 5*
if0(13,2,3) -> 5*
if0(11,13,11) -> 5*
if0(1,11,11) -> 5*
if0(13,4,3) -> 5*
if0(3,2,3) -> 5*
if0(1,13,11) -> 5*
if0(3,4,3) -> 5*
if0(10,11,10) -> 5*
if0(13,2,12) -> 5*
if0(11,2,13) -> 5*
if0(4,10,4) -> 5*
if0(12,2,2) -> 5*
if0(10,13,10) -> 5*
if0(3,2,12) -> 5*
if0(13,4,12) -> 5*
if0(11,4,13) -> 5*
if0(1,2,13) -> 5*
if0(4,12,4) -> 5*
if0(4,2,1) -> 5*
if0(12,4,2) -> 5*
if0(2,2,2) -> 5*
if0(13,10,3) -> 5*
if0(3,4,12) -> 5*
if0(1,4,13) -> 5*
if0(4,4,1) -> 5*
if0(2,4,2) -> 5*
if0(12,2,11) -> 5*
if0(13,12,3) -> 5*
if0(3,10,3) -> 5*
if0(12,4,11) -> 5*
if0(2,2,11) -> 5*
if0(3,12,3) -> 5*
if0(13,10,12) -> 5*
if0(11,10,13) -> 5*
if0(12,10,2) -> 5*
if0(2,4,11) -> 5*
if0(10,1,4) -> 5*
if0(13,12,12) -> 5*
if0(3,10,12) -> 5*
if0(1,10,13) -> 5*
if0(11,12,13) -> 5*
if0(11,2,10) -> 5*
if0(4,10,1) -> 5*
if0(12,12,2) -> 5*
if0(2,10,2) -> 5*
if0(10,3,4) -> 5*
if0(3,12,12) -> 5*
if0(1,12,13) -> 5*
if0(11,4,10) -> 5*
if0(1,2,10) -> 5*
if0(4,12,1) -> 5*
if0(2,12,2) -> 5*
if0(12,10,11) -> 5*
if0(1,4,10) -> 5*
if0(12,12,11) -> 5*
if0(2,10,11) -> 5*
if0(4,1,3) -> 5*
if0(2,12,11) -> 5*
if0(4,3,3) -> 5*
if0(11,10,10) -> 5*
if0(12,1,13) -> 5*
if0(13,1,2) -> 5*
if0(10,11,4) -> 5*
if0(10,1,1) -> 5*
if0(1,10,10) -> 5*
if0(11,12,10) -> 5*
if0(4,1,12) -> 5*
if0(12,3,13) -> 5*
if0(2,1,13) -> 5*
if0(13,3,2) -> 5*
if0(3,1,2) -> 5*
if0(10,13,4) -> 5*
if0(10,3,1) -> 5*
if0(1,12,10) -> 5*
if0(4,3,12) -> 5*
if0(2,3,13) -> 5*
if0(3,3,2) -> 5*
if0(13,1,11) -> 5*
if0(13,3,11) -> 5*
if0(3,1,11) -> 5*
if0(4,11,3) -> 5*
if0(3,3,11) -> 5*
if0(4,13,3) -> 5*
if0(12,11,13) -> 5*
if0(12,1,10) -> 5*
if0(13,11,2) -> 5*
if0(10,11,1) -> 5*
if0(11,2,4) -> 5*
if0(4,11,12) -> 5*
if0(2,11,13) -> 5*
if0(12,13,13) -> 5*
if0(12,3,10) -> 5*
if0(2,1,10) -> 5*
if0(13,13,2) -> 5*
if0(3,11,2) -> 5*
if0(10,13,1) -> 5*
if0(11,4,4) -> 5*
if0(4,13,12) -> 5*
if0(1,2,4) -> 5*
if0(2,13,13) -> 5*
if0(2,3,10) -> 5*
if0(3,13,2) -> 5*
if0(13,11,11) -> 5*
if0(1,4,4) -> 5*
if0(10,2,3) -> 5*
if0(13,13,11) -> 5*
if0(3,11,11) -> 5*
if0(3,13,11) -> 5*
if0(10,4,3) -> 5*
if0(11,10,4) -> 5*
if0(12,11,10) -> 5*
if0(13,2,13) -> 5*
if0(10,2,12) -> 5*
if0(1,10,4) -> 5*
if0(11,12,4) -> 5*
if0(11,2,1) -> 5*
if0(2,11,10) -> 5*
if0(12,13,10) -> 5*
if0(13,4,13) -> 5*
if0(3,2,13) -> 5*
if0(4,2,2) -> 5*
if0(10,4,12) -> 5*
if0(1,12,4) -> 5*
if0(11,4,1) -> 5*
if0(1,2,1) -> 5*
if0(2,13,10) -> 5*
if0(3,4,13) -> 5*
if0(10,10,3) -> 5*
if0(4,4,2) -> 5*
if0(1,4,1) -> 5*
if0(10,12,3) -> 5*
if0(4,2,11) -> 5*
if0(13,10,13) -> 5*
if0(10,10,12) -> 5*
if0(4,4,11) -> 5*
if0(11,10,1) -> 5*
if0(12,1,4) -> 5*
if0(3,10,13) -> 5*
if0(13,12,13) -> 5*
if0(13,2,10) -> 5*
if0(4,10,2) -> 5*
if0(10,12,12) -> 5*
if0(1,10,1) -> 5*
if0(11,12,1) -> 5*
if0(12,3,4) -> 5*
if0(2,1,4) -> 5*
if0(3,12,13) -> 5*
if0(13,4,10) -> 5*
if0(3,2,10) -> 5*
if0(4,12,2) -> 5*
if0(1,12,1) -> 5*
if0(2,3,4) -> 5*
if0(3,4,10) -> 5*
if0(4,10,11) -> 5*
if0(11,1,3) -> 5*
if0(4,12,11) -> 5*
if0(11,3,3) -> 5*
if0(1,1,3) -> 5*
if0(13,10,10) -> 5*
if0(1,3,3) -> 5*
if0(11,1,12) -> 5*
if0(12,11,4) -> 5*
if0(12,1,1) -> 5*
if0(3,10,10) -> 5*
if0(10,1,2) -> 5*
if0(13,12,10) -> 5*
if0(4,1,13) -> 5*
if0(11,3,12) -> 5*
if0(1,1,12) -> 5*
if0(2,11,4) -> 5*
if0(12,13,4) -> 5*
if0(12,3,1) -> 5*
if0(2,1,1) -> 5*
if0(3,12,10) -> 5*
if0(10,3,2) -> 5*
if0(4,3,13) -> 5*
if0(1,3,12) -> 5*
if0(2,13,4) -> 5*
if0(2,3,1) -> 5*
if0(10,1,11) -> 5*
if0(11,11,3) -> 5*
if0(10,3,11) -> 5*
if0(1,11,3) -> 5*
if0(11,13,3) -> 5*
if0(1,13,3) -> 5*
if0(11,11,12) -> 5*
if0(12,11,1) -> 5*
if0(10,11,2) -> 5*
if0(13,2,4) -> 5*
if0(4,11,13) -> 5*
if0(4,1,10) -> 5*
if0(1,11,12) -> 5*
if0(11,13,12) -> 5*
if0(2,11,1) -> 5*
if0(12,13,1) -> 5*
if0(10,13,2) -> 5*
if0(13,4,4) -> 5*
if0(3,2,4) -> 5*
if0(4,13,13) -> 5*
if0(4,3,10) -> 5*
if0(1,13,12) -> 5*
if0(2,13,1) -> 5*
if0(3,4,4) -> 5*
if0(10,11,11) -> 5*
if0(12,2,3) -> 5*
if0(10,13,11) -> 5*
if0(12,4,3) -> 5*
if0(2,2,3) -> 5*
if0(13,10,4) -> 5*
if0(2,4,3) -> 5*
if0(12,2,12) -> 5*
if0(3,10,4) -> 5*
if0(10,2,13) -> 5*
if0(13,12,4) -> 5*
if0(13,2,1) -> 5*
if0(4,11,10) -> 5*
if0(11,2,2) -> 5*
if0(12,4,12) -> 5*
if0(2,2,12) -> 5*
if0(3,12,4) -> 5*
if0(10,4,13) -> 5*
if0(13,4,1) -> 5*
if0(3,2,1) -> 5*
if0(4,13,10) -> 5*
if0(11,4,2) -> 5*
if0(1,2,2) -> 5*
if0(12,10,3) -> 5*
if0(2,4,12) -> 5*
if0(3,4,1) -> 5*
if0(1,4,2) -> 5*
if0(11,2,11) -> 5*
if0(2,10,3) -> 5*
if0(12,12,3) -> 5*
if0(11,4,11) -> 5*
if0(1,2,11) -> 5*
if0(2,12,3) -> 5*
if0(12,10,12) -> 5*
if0(10,10,13) -> 5*
if0(13,10,1) -> 5*
if0(11,10,2) -> 5*
if0(1,4,11) -> 5*
if0(2,10,12) -> 5*
if0(12,12,12) -> 5*
if0(10,12,13) -> 5*
if0(3,10,1) -> 5*
if0(10,2,10) -> 5*
if0(13,12,1) -> 5*
if0(1,10,2) -> 5*
if0(11,12,2) -> 5*
if0(4,1,4) -> 5*
if0(2,12,12) -> 5*
if0(3,12,1) -> 5*
if0(10,4,10) -> 5*
if0(1,12,2) -> 5*
if0(4,3,4) -> 5*
if0(11,10,11) -> 5*
if0(13,1,3) -> 5*
if0(1,10,11) -> 5*
if0(11,12,11) -> 5*
if0(13,3,3) -> 5*
if0(3,1,3) -> 5*
if0(1,12,11) -> 5*
if0(3,3,3) -> 5*
if0(10,10,10) -> 5*
if0(13,1,12) -> 5*
if0(11,1,13) -> 5*
if0(12,1,2) -> 5*
if0(10,12,10) -> 5*
if0(13,3,12) -> 5*
if0(3,1,12) -> 5*
if0(1,1,13) -> 5*
if0(4,11,4) -> 5*
if0(11,3,13) -> 5*
if0(4,1,1) -> 5*
if0(12,3,2) -> 5*
if0(2,1,2) -> 5*
if0(3,3,12) -> 5*
if0(1,3,13) -> 5*
if0(4,13,4) -> 5*
if0(4,3,1) -> 5*
if0(2,3,2) -> 5*
if0(12,1,11) -> 5*
if0(13,11,3) -> 5*
if0(12,3,11) -> 5*
if0(2,1,11) -> 5*
if0(3,11,3) -> 5*
if0(13,13,3) -> 5*
if0(2,3,11) -> 5*
if0(3,13,3) -> 5*
if0(13,11,12) -> 5*
if0(11,11,13) -> 5*
if0(11,1,10) -> 5*
if0(12,11,2) -> 5*
if0(3,11,12) -> 5*
if0(10,2,4) -> 5*
if0(13,13,12) -> 5*
if0(11,13,13) -> 5*
if0(1,11,13) -> 5*
if0(1,1,10) -> 5*
if0(4,11,1) -> 5*
if0(11,3,10) -> 5*
if0(12,13,2) -> 5*
if0(2,11,2) -> 5*
if0(3,13,12) -> 5*
if0(10,4,4) -> 5*
if0(1,13,13) -> 5*
if0(1,3,10) -> 5*
if0(4,13,1) -> 5*
if0(2,13,2) -> 5*
if0(12,11,11) -> 5*
if0(12,13,11) -> 5*
if0(2,11,11) -> 5*
if0(4,2,3) -> 5*
if0(2,13,11) -> 5*
if0(10,10,4) -> 5*
if0(4,4,3) -> 5*
if0(11,11,10) -> 5*
if0(12,2,13) -> 5*
if0(13,2,2) -> 5*
if0(10,12,4) -> 5*
if0(10,2,1) -> 5*
if0(11,13,10) -> 5*
if0(1,11,10) -> 5*
if0(4,2,12) -> 5*
if0(2,2,13) -> 5*
if0(12,4,13) -> 5*
if0(13,4,2) -> 5*
if0(3,2,2) -> 5*
if0(10,4,1) -> 5*
if0(1,13,10) -> 5*
if0(4,4,12) -> 5*
if0(2,4,13) -> 5*
true0() -> 10*,5,1
false0() -> 11*,5,2
u0() -> 12*,5,3
v0() -> 13*,5,4
1 -> 5*
2 -> 5*
3 -> 5*
4 -> 5*
10 -> 5*
11 -> 5*
12 -> 5*
13 -> 5*
problem:
Qed