Inferring Expected Runtimes Using Sizes

KoAT2 Proof WORST_CASE( ?, 9/2 {O(1)})

Initial Complexity Problem (after preprocessing)

Start:f
Program_Vars:Arg_0, Arg_1, Arg_2
Temp_Vars:
Locations:ab, ab_end, abc, abc_end, ac_end, bc, bc_end, f
Transitions:
ab(Arg_0,Arg_1,Arg_2) -> 1/3:ab(0,Arg_1,Arg_2) :+: 1/3:ab(0,Arg_1,Arg_2) :+: 1/3:ab(1,Arg_1,Arg_2) :|: 0<Arg_0 && Arg_2<=0 && Arg_2<=Arg_1 && Arg_1+Arg_2<=0 && Arg_2<=Arg_0 && Arg_0+Arg_2<=1 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && Arg_1<=Arg_2 && 0<=Arg_0+Arg_2 && Arg_0<=1+Arg_2 && Arg_1<=0 && Arg_1<=Arg_0 && Arg_0+Arg_1<=1 && 0<=Arg_1 && 0<=Arg_0+Arg_1 && Arg_0<=1+Arg_1 && Arg_0<=1 && 0<=Arg_0 && Arg_2<=0 && Arg_2<=Arg_1 && Arg_1+Arg_2<=0 && Arg_2<=Arg_0 && Arg_0+Arg_2<=1 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && Arg_1<=Arg_2 && 0<=Arg_0+Arg_2 && Arg_0<=1+Arg_2 && Arg_1<=0 && Arg_1<=Arg_0 && Arg_0+Arg_1<=1 && 0<=Arg_1 && 0<=Arg_0+Arg_1 && Arg_0<=1+Arg_1 && Arg_0<=1 && 0<=Arg_0
ab(Arg_0,Arg_1,Arg_2) -{0}> ab_end(Arg_0,Arg_1,Arg_2) :|: Arg_0<1 && Arg_2<=0 && Arg_2<=Arg_1 && Arg_1+Arg_2<=0 && Arg_2<=Arg_0 && Arg_0+Arg_2<=1 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && Arg_1<=Arg_2 && 0<=Arg_0+Arg_2 && Arg_0<=1+Arg_2 && Arg_1<=0 && Arg_1<=Arg_0 && Arg_0+Arg_1<=1 && 0<=Arg_1 && 0<=Arg_0+Arg_1 && Arg_0<=1+Arg_1 && Arg_0<=1 && 0<=Arg_0 && Arg_2<=0 && Arg_2<=Arg_1 && Arg_1+Arg_2<=0 && Arg_2<=Arg_0 && Arg_0+Arg_2<=1 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && Arg_1<=Arg_2 && 0<=Arg_0+Arg_2 && Arg_0<=1+Arg_2 && Arg_1<=0 && Arg_1<=Arg_0 && Arg_0+Arg_1<=1 && 0<=Arg_1 && 0<=Arg_0+Arg_1 && Arg_0<=1+Arg_1 && Arg_0<=1 && 0<=Arg_0
bc(Arg_0,Arg_1,Arg_2) -> 1/2:bc(Arg_0,Arg_1,0) :+: 1/2:bc(Arg_0,Arg_1,0) :|: 0<Arg_2 && Arg_2<=1 && Arg_2<=1+Arg_1 && Arg_1+Arg_2<=1 && Arg_2<=1+Arg_0 && Arg_0+Arg_2<=1 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && Arg_1<=Arg_2 && 0<=Arg_0+Arg_2 && Arg_0<=Arg_2 && Arg_1<=0 && Arg_1<=Arg_0 && Arg_0+Arg_1<=0 && 0<=Arg_1 && 0<=Arg_0+Arg_1 && Arg_0<=Arg_1 && Arg_0<=0 && 0<=Arg_0 && Arg_2<=1 && Arg_2<=1+Arg_1 && Arg_1+Arg_2<=1 && Arg_2<=1+Arg_0 && Arg_0+Arg_2<=1 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && Arg_1<=Arg_2 && 0<=Arg_0+Arg_2 && Arg_0<=Arg_2 && Arg_1<=0 && Arg_1<=Arg_0 && Arg_0+Arg_1<=0 && 0<=Arg_1 && 0<=Arg_0+Arg_1 && Arg_0<=Arg_1 && Arg_0<=0 && 0<=Arg_0
bc(Arg_0,Arg_1,Arg_2) -{0}> bc_end(Arg_0,Arg_1,Arg_2) :|: Arg_2<1 && Arg_2<=1 && Arg_2<=1+Arg_1 && Arg_1+Arg_2<=1 && Arg_2<=1+Arg_0 && Arg_0+Arg_2<=1 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && Arg_1<=Arg_2 && 0<=Arg_0+Arg_2 && Arg_0<=Arg_2 && Arg_1<=0 && Arg_1<=Arg_0 && Arg_0+Arg_1<=0 && 0<=Arg_1 && 0<=Arg_0+Arg_1 && Arg_0<=Arg_1 && Arg_0<=0 && 0<=Arg_0 && Arg_2<=1 && Arg_2<=1+Arg_1 && Arg_1+Arg_2<=1 && Arg_2<=1+Arg_0 && Arg_0+Arg_2<=1 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && Arg_1<=Arg_2 && 0<=Arg_0+Arg_2 && Arg_0<=Arg_2 && Arg_1<=0 && Arg_1<=Arg_0 && Arg_0+Arg_1<=0 && 0<=Arg_1 && 0<=Arg_0+Arg_1 && Arg_0<=Arg_1 && Arg_0<=0 && 0<=Arg_0
f(Arg_0,Arg_1,Arg_2) -{0}> abc(1,1,1)
abc_end(Arg_0,Arg_1,Arg_2) -{0}> ab(Arg_0,Arg_1,Arg_2) :|: Arg_0<=1 && 1<=Arg_0 && Arg_2<=1 && Arg_2<=1+Arg_1 && Arg_1+Arg_2<=1 && Arg_2<=1+Arg_0 && Arg_0+Arg_2<=1 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && Arg_1<=Arg_2 && 0<=Arg_0+Arg_2 && Arg_0<=1+Arg_2 && Arg_1<=0 && Arg_1<=Arg_0 && Arg_0+Arg_1<=1 && 0<=Arg_1 && 0<=Arg_0+Arg_1 && Arg_0<=1+Arg_1 && Arg_0<=1 && 0<=Arg_0 && Arg_2<=1 && Arg_2<=1+Arg_1 && Arg_1+Arg_2<=1 && Arg_2<=1+Arg_0 && Arg_0+Arg_2<=1 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && Arg_1<=Arg_2 && 0<=Arg_0+Arg_2 && Arg_0<=1+Arg_2 && Arg_1<=0 && Arg_1<=Arg_0 && Arg_0+Arg_1<=1 && 0<=Arg_1 && 0<=Arg_0+Arg_1 && Arg_0<=1+Arg_1 && Arg_0<=1 && 0<=Arg_0
abc_end(Arg_0,Arg_1,Arg_2) -{0}> ab_end(Arg_0,Arg_1,Arg_2) :|: Arg_0<=0 && 0<=Arg_0 && Arg_2<=1 && Arg_2<=1+Arg_1 && Arg_1+Arg_2<=1 && Arg_2<=1+Arg_0 && Arg_0+Arg_2<=1 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && Arg_1<=Arg_2 && 0<=Arg_0+Arg_2 && Arg_0<=1+Arg_2 && Arg_1<=0 && Arg_1<=Arg_0 && Arg_0+Arg_1<=1 && 0<=Arg_1 && 0<=Arg_0+Arg_1 && Arg_0<=1+Arg_1 && Arg_0<=1 && 0<=Arg_0 && Arg_2<=1 && Arg_2<=1+Arg_1 && Arg_1+Arg_2<=1 && Arg_2<=1+Arg_0 && Arg_0+Arg_2<=1 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && Arg_1<=Arg_2 && 0<=Arg_0+Arg_2 && Arg_0<=1+Arg_2 && Arg_1<=0 && Arg_1<=Arg_0 && Arg_0+Arg_1<=1 && 0<=Arg_1 && 0<=Arg_0+Arg_1 && Arg_0<=1+Arg_1 && Arg_0<=1 && 0<=Arg_0
ac_end(Arg_0,Arg_1,Arg_2) -{0}> bc(Arg_0,Arg_1,Arg_2) :|: Arg_2<=1 && 1<=Arg_2 && Arg_2<=1 && Arg_2<=1+Arg_1 && Arg_1+Arg_2<=1 && Arg_2<=1+Arg_0 && Arg_0+Arg_2<=1 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && Arg_1<=Arg_2 && 0<=Arg_0+Arg_2 && Arg_0<=Arg_2 && Arg_1<=0 && Arg_1<=Arg_0 && Arg_0+Arg_1<=0 && 0<=Arg_1 && 0<=Arg_0+Arg_1 && Arg_0<=Arg_1 && Arg_0<=0 && 0<=Arg_0 && Arg_2<=1 && Arg_2<=1+Arg_1 && Arg_1+Arg_2<=1 && Arg_2<=1+Arg_0 && Arg_0+Arg_2<=1 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && Arg_1<=Arg_2 && 0<=Arg_0+Arg_2 && Arg_0<=Arg_2 && Arg_1<=0 && Arg_1<=Arg_0 && Arg_0+Arg_1<=0 && 0<=Arg_1 && 0<=Arg_0+Arg_1 && Arg_0<=Arg_1 && Arg_0<=0 && 0<=Arg_0
ac_end(Arg_0,Arg_1,Arg_2) -{0}> bc_end(Arg_0,Arg_1,Arg_2) :|: Arg_2<=0 && 0<=Arg_2 && Arg_2<=1 && Arg_2<=1+Arg_1 && Arg_1+Arg_2<=1 && Arg_2<=1+Arg_0 && Arg_0+Arg_2<=1 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && Arg_1<=Arg_2 && 0<=Arg_0+Arg_2 && Arg_0<=Arg_2 && Arg_1<=0 && Arg_1<=Arg_0 && Arg_0+Arg_1<=0 && 0<=Arg_1 && 0<=Arg_0+Arg_1 && Arg_0<=Arg_1 && Arg_0<=0 && 0<=Arg_0 && Arg_2<=1 && Arg_2<=1+Arg_1 && Arg_1+Arg_2<=1 && Arg_2<=1+Arg_0 && Arg_0+Arg_2<=1 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && Arg_1<=Arg_2 && 0<=Arg_0+Arg_2 && Arg_0<=Arg_2 && Arg_1<=0 && Arg_1<=Arg_0 && Arg_0+Arg_1<=0 && 0<=Arg_1 && 0<=Arg_0+Arg_1 && Arg_0<=Arg_1 && Arg_0<=0 && 0<=Arg_0
ab(Arg_0,Arg_1,Arg_2) -{0}> ac_end(Arg_0,Arg_1,Arg_2) :|: Arg_0<1 && Arg_2<=0 && Arg_2<=Arg_1 && Arg_1+Arg_2<=0 && Arg_2<=Arg_0 && Arg_0+Arg_2<=1 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && Arg_1<=Arg_2 && 0<=Arg_0+Arg_2 && Arg_0<=1+Arg_2 && Arg_1<=0 && Arg_1<=Arg_0 && Arg_0+Arg_1<=1 && 0<=Arg_1 && 0<=Arg_0+Arg_1 && Arg_0<=1+Arg_1 && Arg_0<=1 && 0<=Arg_0 && Arg_1<=0 && 0<=Arg_1 && Arg_2<=1 && Arg_2<=1+Arg_1 && Arg_1+Arg_2<=1 && Arg_2<=1+Arg_0 && Arg_0+Arg_2<=1 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && Arg_1<=Arg_2 && 0<=Arg_0+Arg_2 && Arg_0<=Arg_2 && Arg_1<=0 && Arg_1<=Arg_0 && Arg_0+Arg_1<=0 && 0<=Arg_1 && 0<=Arg_0+Arg_1 && Arg_0<=Arg_1 && Arg_0<=0 && 0<=Arg_0 && Arg_2<=0 && Arg_2<=Arg_1 && Arg_1+Arg_2<=0 && Arg_2<=Arg_0 && Arg_0+Arg_2<=1 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && Arg_1<=Arg_2 && 0<=Arg_0+Arg_2 && Arg_0<=1+Arg_2 && Arg_1<=0 && Arg_1<=Arg_0 && Arg_0+Arg_1<=1 && 0<=Arg_1 && 0<=Arg_0+Arg_1 && Arg_0<=1+Arg_1 && Arg_0<=1 && 0<=Arg_0
abc_end(Arg_0,Arg_1,Arg_2) -{0}> ac_end(Arg_0,Arg_1,Arg_2) :|: Arg_0<=0 && 0<=Arg_0 && Arg_2<=1 && Arg_2<=1+Arg_1 && Arg_1+Arg_2<=1 && Arg_2<=1+Arg_0 && Arg_0+Arg_2<=1 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && Arg_1<=Arg_2 && 0<=Arg_0+Arg_2 && Arg_0<=1+Arg_2 && Arg_1<=0 && Arg_1<=Arg_0 && Arg_0+Arg_1<=1 && 0<=Arg_1 && 0<=Arg_0+Arg_1 && Arg_0<=1+Arg_1 && Arg_0<=1 && 0<=Arg_0 && Arg_1<=0 && 0<=Arg_1 && Arg_2<=1 && Arg_2<=1+Arg_1 && Arg_1+Arg_2<=1 && Arg_2<=1+Arg_0 && Arg_0+Arg_2<=1 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && Arg_1<=Arg_2 && 0<=Arg_0+Arg_2 && Arg_0<=Arg_2 && Arg_1<=0 && Arg_1<=Arg_0 && Arg_0+Arg_1<=0 && 0<=Arg_1 && 0<=Arg_0+Arg_1 && Arg_0<=Arg_1 && Arg_0<=0 && 0<=Arg_0 && Arg_2<=1 && Arg_2<=1+Arg_1 && Arg_1+Arg_2<=1 && Arg_2<=1+Arg_0 && Arg_0+Arg_2<=1 && 0<=Arg_2 && 0<=Arg_1+Arg_2 && Arg_1<=Arg_2 && 0<=Arg_0+Arg_2 && Arg_0<=1+Arg_2 && Arg_1<=0 && Arg_1<=Arg_0 && Arg_0+Arg_1<=1 && 0<=Arg_1 && 0<=Arg_0+Arg_1 && Arg_0<=1+Arg_1 && Arg_0<=1 && 0<=Arg_0
f(Arg_0,Arg_1,Arg_2) -> 1/6:abc_end(1,0,0) :+: 1/6:abc_end(0,0,0) :+: 1/3:abc_end(1,0,0) :+: 1/3:abc_end(0,0,1) :|: 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0 && 0<=0

G ab ab ab->ab t₄ ∈ g₁ p = 1/3 η (Arg_0) = 0 τ = 0<Arg_0 ab->ab t₅ ∈ g₁ p = 1/3 η (Arg_0) = 0 τ = 0<Arg_0 ab->ab t₆ ∈ g₁ p = 1/3 η (Arg_0) = 1 τ = 0<Arg_0 ab_end ab_end ab->ab_end t₇ ∈ g₂ τ = Arg_0<1 {0} ac_end ac_end ab->ac_end t₂₁ ∈ g₁₄ τ = Arg_0<1 && Arg_1<=0 && 0<=Arg_1 {0} abc abc abc_end abc_end abc_end->ab t₁₅ ∈ g₈ τ = Arg_0<=1 && 1<=Arg_0 {0} abc_end->ab_end t₁₆ ∈ g₉ τ = Arg_0<=0 && 0<=Arg_0 {0} abc_end->ac_end t₂₂ ∈ g₁₅ τ = Arg_0<=0 && 0<=Arg_0 && Arg_1<=0 && 0<=Arg_1 {0} bc bc ac_end->bc t₁₉ ∈ g₁₂ τ = Arg_2<=1 && 1<=Arg_2 {0} bc_end bc_end ac_end->bc_end t₂₀ ∈ g₁₃ τ = Arg_2<=0 && 0<=Arg_2 {0} bc->bc t₁₁ ∈ g₅ p = 1/2 η (Arg_2) = 0 τ = 0<Arg_2 bc->bc t₁₂ ∈ g₅ p = 1/2 η (Arg_2) = 0 τ = 0<Arg_2 bc->bc_end t₁₃ ∈ g₆ τ = Arg_2<1 {0} f f f->abc t₁₄ ∈ g₇ η (Arg_0) = 1 η (Arg_1) = 1 η (Arg_2) = 1 {0} f->abc_end t₂₃ ∈ g₁₆ p = 1/6 η (Arg_0) = 1 η (Arg_1) = 0 η (Arg_2) = 0 f->abc_end t₂₄ ∈ g₁₆ p = 1/6 η (Arg_0) = 0 η (Arg_1) = 0 η (Arg_2) = 0 f->abc_end t₂₅ ∈ g₁₆ p = 1/3 η (Arg_0) = 1 η (Arg_1) = 0 η (Arg_2) = 0 f->abc_end t₂₆ ∈ g₁₆ p = 1/3 η (Arg_0) = 0 η (Arg_1) = 0 η (Arg_2) = 1

Timebounds:

Overall timebound:inf {Infinity}
4,1: ab->ab: 1 {O(1)}
5,1: ab->ab: 1 {O(1)}
6,1: ab->ab: inf {Infinity}
7,2: ab->ab_end: 1 {O(1)}
21,14: ab->ac_end: 1 {O(1)}
15,8: abc_end->ab: 1 {O(1)}
16,9: abc_end->ab_end: 1 {O(1)}
22,15: abc_end->ac_end: 1 {O(1)}
19,12: ac_end->bc: 1 {O(1)}
20,13: ac_end->bc_end: 1 {O(1)}
11,5: bc->bc: 1 {O(1)}
12,5: bc->bc: 1 {O(1)}
13,6: bc->bc_end: 1 {O(1)}
14,7: f->abc: 1 {O(1)}
23,16: f->abc_end: 1 {O(1)}
24,16: f->abc_end: 1 {O(1)}
25,16: f->abc_end: 1 {O(1)}
26,16: f->abc_end: 1 {O(1)}

Expected Timebounds:

Overall expected timebound: 27/2 {O(1)}
1: ab->[1/3:ab; 1/3:ab; 1/3:ab]: 3/2 {O(1)}
2: ab->[1:ab_end]: 1 {O(1)}
5: bc->[1/2:bc; 1/2:bc]: 2 {O(1)}
6: bc->[1:bc_end]: 1 {O(1)}
7: f->[1:abc]: 1 {O(1)}
8: abc_end->[1:ab]: 1 {O(1)}
9: abc_end->[1:ab_end]: 1 {O(1)}
12: ac_end->[1:bc]: 1 {O(1)}
13: ac_end->[1:bc_end]: 1 {O(1)}
14: ab->[1:ac_end]: 1 {O(1)}
15: abc_end->[1:ac_end]: 1 {O(1)}
16: f->[1/6:abc_end; 1/6:abc_end; 1/3:abc_end; 1/3:abc_end]: 1 {O(1)}

Costbounds:

Overall costbound: inf {Infinity}
4,1: ab->ab: inf {Infinity}
5,1: ab->ab: inf {Infinity}
6,1: ab->ab: inf {Infinity}
7,2: ab->ab_end: inf {Infinity}
21,14: ab->ac_end: inf {Infinity}
15,8: abc_end->ab: inf {Infinity}
16,9: abc_end->ab_end: inf {Infinity}
22,15: abc_end->ac_end: inf {Infinity}
19,12: ac_end->bc: inf {Infinity}
20,13: ac_end->bc_end: inf {Infinity}
11,5: bc->bc: inf {Infinity}
12,5: bc->bc: inf {Infinity}
13,6: bc->bc_end: inf {Infinity}
14,7: f->abc: inf {Infinity}
23,16: f->abc_end: inf {Infinity}
24,16: f->abc_end: inf {Infinity}
25,16: f->abc_end: inf {Infinity}
26,16: f->abc_end: inf {Infinity}

Expected Costbounds:

Overall expected costbound: 9/2 {O(1)}
1: ab->[1/3:ab; 1/3:ab; 1/3:ab]: 3/2 {O(1)}
2: ab->[1:ab_end]: 0 {O(1)}
5: bc->[1/2:bc; 1/2:bc]: 2 {O(1)}
6: bc->[1:bc_end]: 0 {O(1)}
7: f->[1:abc]: 0 {O(1)}
8: abc_end->[1:ab]: 0 {O(1)}
9: abc_end->[1:ab_end]: 0 {O(1)}
12: ac_end->[1:bc]: 0 {O(1)}
13: ac_end->[1:bc_end]: 0 {O(1)}
14: ab->[1:ac_end]: 0 {O(1)}
15: abc_end->[1:ac_end]: 0 {O(1)}
16: f->[1/6:abc_end; 1/6:abc_end; 1/3:abc_end; 1/3:abc_end]: 1 {O(1)}

Sizebounds:

4,1: ab->ab, Arg_0: 0 {O(1)}
4,1: ab->ab, Arg_1: 0 {O(1)}
4,1: ab->ab, Arg_2: 0 {O(1)}
5,1: ab->ab, Arg_0: 0 {O(1)}
5,1: ab->ab, Arg_1: 0 {O(1)}
5,1: ab->ab, Arg_2: 0 {O(1)}
6,1: ab->ab, Arg_0: 1 {O(1)}
6,1: ab->ab, Arg_1: 0 {O(1)}
6,1: ab->ab, Arg_2: 0 {O(1)}
7,2: ab->ab_end, Arg_0: 0 {O(1)}
7,2: ab->ab_end, Arg_1: 0 {O(1)}
7,2: ab->ab_end, Arg_2: 0 {O(1)}
21,14: ab->ac_end, Arg_0: 0 {O(1)}
21,14: ab->ac_end, Arg_1: 0 {O(1)}
21,14: ab->ac_end, Arg_2: 0 {O(1)}
15,8: abc_end->ab, Arg_0: 1 {O(1)}
15,8: abc_end->ab, Arg_1: 0 {O(1)}
15,8: abc_end->ab, Arg_2: 0 {O(1)}
16,9: abc_end->ab_end, Arg_0: 0 {O(1)}
16,9: abc_end->ab_end, Arg_1: 0 {O(1)}
16,9: abc_end->ab_end, Arg_2: 1 {O(1)}
22,15: abc_end->ac_end, Arg_0: 0 {O(1)}
22,15: abc_end->ac_end, Arg_1: 0 {O(1)}
22,15: abc_end->ac_end, Arg_2: 1 {O(1)}
19,12: ac_end->bc, Arg_0: 0 {O(1)}
19,12: ac_end->bc, Arg_1: 0 {O(1)}
19,12: ac_end->bc, Arg_2: 1 {O(1)}
20,13: ac_end->bc_end, Arg_0: 0 {O(1)}
20,13: ac_end->bc_end, Arg_1: 0 {O(1)}
20,13: ac_end->bc_end, Arg_2: 0 {O(1)}
11,5: bc->bc, Arg_0: 0 {O(1)}
11,5: bc->bc, Arg_1: 0 {O(1)}
11,5: bc->bc, Arg_2: 0 {O(1)}
12,5: bc->bc, Arg_0: 0 {O(1)}
12,5: bc->bc, Arg_1: 0 {O(1)}
12,5: bc->bc, Arg_2: 0 {O(1)}
13,6: bc->bc_end, Arg_0: 0 {O(1)}
13,6: bc->bc_end, Arg_1: 0 {O(1)}
13,6: bc->bc_end, Arg_2: 0 {O(1)}
14,7: f->abc, Arg_0: 1 {O(1)}
14,7: f->abc, Arg_1: 1 {O(1)}
14,7: f->abc, Arg_2: 1 {O(1)}
23,16: f->abc_end, Arg_1: 0 {O(1)}
23,16: f->abc_end, Arg_2: 0 {O(1)}
24,16: f->abc_end, Arg_0: 0 {O(1)}
24,16: f->abc_end, Arg_1: 0 {O(1)}
24,16: f->abc_end, Arg_2: 0 {O(1)}
25,16: f->abc_end, Arg_1: 0 {O(1)}
25,16: f->abc_end, Arg_2: 0 {O(1)}
26,16: f->abc_end, Arg_0: 0 {O(1)}
26,16: f->abc_end, Arg_1: 0 {O(1)}

ExpSizeBounds:

(1: ab->[1/3:ab; 1/3:ab; 1/3:ab], ab), Arg_0: 1 {O(1)}
(1: ab->[1/3:ab; 1/3:ab; 1/3:ab], ab), Arg_1: 0 {O(1)}
(1: ab->[1/3:ab; 1/3:ab; 1/3:ab], ab), Arg_2: 0 {O(1)}
(2: ab->[1:ab_end], ab_end), Arg_0: 0 {O(1)}
(2: ab->[1:ab_end], ab_end), Arg_1: 0 {O(1)}
(2: ab->[1:ab_end], ab_end), Arg_2: 0 {O(1)}
(5: bc->[1/2:bc; 1/2:bc], bc), Arg_0: 0 {O(1)}
(5: bc->[1/2:bc; 1/2:bc], bc), Arg_1: 0 {O(1)}
(5: bc->[1/2:bc; 1/2:bc], bc), Arg_2: 0 {O(1)}
(6: bc->[1:bc_end], bc_end), Arg_0: 0 {O(1)}
(6: bc->[1:bc_end], bc_end), Arg_1: 0 {O(1)}
(6: bc->[1:bc_end], bc_end), Arg_2: 0 {O(1)}
(7: f->[1:abc], abc), Arg_0: 1 {O(1)}
(7: f->[1:abc], abc), Arg_1: 1 {O(1)}
(7: f->[1:abc], abc), Arg_2: 1 {O(1)}
(8: abc_end->[1:ab], ab), Arg_0: 1 {O(1)}
(8: abc_end->[1:ab], ab), Arg_1: 0 {O(1)}
(8: abc_end->[1:ab], ab), Arg_2: 0 {O(1)}
(9: abc_end->[1:ab_end], ab_end), Arg_0: 0 {O(1)}
(9: abc_end->[1:ab_end], ab_end), Arg_1: 0 {O(1)}
(9: abc_end->[1:ab_end], ab_end), Arg_2: 1 {O(1)}
(12: ac_end->[1:bc], bc), Arg_0: 0 {O(1)}
(12: ac_end->[1:bc], bc), Arg_1: 0 {O(1)}
(12: ac_end->[1:bc], bc), Arg_2: 1 {O(1)}
(13: ac_end->[1:bc_end], bc_end), Arg_0: 0 {O(1)}
(13: ac_end->[1:bc_end], bc_end), Arg_1: 0 {O(1)}
(13: ac_end->[1:bc_end], bc_end), Arg_2: 0 {O(1)}
(14: ab->[1:ac_end], ac_end), Arg_0: 0 {O(1)}
(14: ab->[1:ac_end], ac_end), Arg_1: 0 {O(1)}
(14: ab->[1:ac_end], ac_end), Arg_2: 0 {O(1)}
(15: abc_end->[1:ac_end], ac_end), Arg_0: 0 {O(1)}
(15: abc_end->[1:ac_end], ac_end), Arg_1: 0 {O(1)}
(15: abc_end->[1:ac_end], ac_end), Arg_2: 1 {O(1)}
(16: f->[1/6:abc_end; 1/6:abc_end; 1/3:abc_end; 1/3:abc_end], abc_end), Arg_0: 1/2*(1+Arg_0)+3/2*Arg_0 {O(n)}
(16: f->[1/6:abc_end; 1/6:abc_end; 1/3:abc_end; 1/3:abc_end], abc_end), Arg_1: 0 {O(1)}
(16: f->[1/6:abc_end; 1/6:abc_end; 1/3:abc_end; 1/3:abc_end], abc_end), Arg_2: 1/3*(1+Arg_2)+5/3*Arg_2 {O(n)}