Inferring Expected Runtimes Using Sizes


KoAT2 Proof WORST_CASE( ?, 282*Arg_4+9 {O(n)})

Initial Complexity Problem (after preprocessing)

Start:f0
Program_Vars:Arg_0, Arg_1, Arg_2, Arg_3, Arg_4, Arg_5, Arg_6, Arg_7, Arg_8, Arg_9
Temp_Vars:K, L
Locations:f0, f17, f27, f37, f45, f55, f65, f75, f83, f93
Transitions:
f0(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,Arg_7,Arg_8,Arg_9) -> f17(0,K,L,0,Arg_4,Arg_5,Arg_6,Arg_7,Arg_8,Arg_9)
f17(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,Arg_7,Arg_8,Arg_9) -> 3/4:f17(Arg_0,Arg_1,Arg_2,Arg_3+1,Arg_4,Arg_5,Arg_6,Arg_7,Arg_8,Arg_9) :+: 1/4:f17(Arg_0,Arg_1,Arg_2,Arg_3-1,Arg_4,Arg_5,Arg_6,Arg_7,Arg_8,Arg_9) :|: Arg_3+1<=Arg_4 && Arg_0<=0 && 0<=Arg_0
f27(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,Arg_7,Arg_8,Arg_9) -> 3/4:f27(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5+1,Arg_6,Arg_7,Arg_8,Arg_9) :+: 1/4:f27(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5-1,Arg_6,Arg_7,Arg_8,Arg_9) :|: Arg_5+1<=Arg_4 && Arg_4<=Arg_3 && Arg_0<=0 && 0<=Arg_0
f37(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,Arg_7,Arg_8,Arg_9) -> 3/4:f37(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6+1,Arg_7,Arg_8,Arg_9) :+: 1/4:f37(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6-1,Arg_7,Arg_8,Arg_9) :|: Arg_6+1<=Arg_4 && Arg_4<=Arg_5 && Arg_4<=Arg_3 && Arg_0<=0 && 0<=Arg_0
f45(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,Arg_7,Arg_8,Arg_9) -> 3/4:f45(Arg_0+1,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,Arg_7,Arg_8,Arg_9) :+: 1/4:f45(Arg_0-1,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,Arg_7,Arg_8,Arg_9) :|: Arg_0+1<=Arg_4 && Arg_4<=Arg_6 && Arg_4<=Arg_5 && Arg_4<=Arg_3
f55(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,Arg_7,Arg_8,Arg_9) -> 3/4:f55(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,Arg_7+1,Arg_8,Arg_9) :+: 1/4:f55(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,Arg_7-1,Arg_8,Arg_9) :|: Arg_7+1<=Arg_4 && Arg_4<=Arg_6 && Arg_4<=Arg_5 && Arg_4<=Arg_3 && Arg_4<=Arg_0
f65(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,Arg_7,Arg_8,Arg_9) -> 3/4:f65(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,Arg_7,Arg_8+1,Arg_9) :+: 1/4:f65(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,Arg_7,Arg_8-1,Arg_9) :|: Arg_8+1<=Arg_4 && Arg_4<=Arg_7 && Arg_4<=Arg_6 && Arg_4<=Arg_5 && Arg_4<=Arg_3 && Arg_4<=Arg_0
f75(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,Arg_7,Arg_8,Arg_9) -> 3/4:f75(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,Arg_7,Arg_8,Arg_9+1) :+: 1/4:f75(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,Arg_7,Arg_8,Arg_9-1) :|: Arg_9+1<=Arg_4 && Arg_4<=Arg_8 && Arg_4<=Arg_7 && Arg_4<=Arg_6 && Arg_4<=Arg_5 && Arg_4<=Arg_3 && Arg_4<=Arg_0
f83(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,Arg_7,Arg_8,Arg_9) -> 3/4:f83(Arg_0+1,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,Arg_7,Arg_8,Arg_9) :+: 1/4:f83(Arg_0-1,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,Arg_7,Arg_8,Arg_9) :|: Arg_0+1<=Arg_4 && Arg_4<=Arg_9 && Arg_4<=Arg_8 && Arg_4<=Arg_7 && Arg_4<=Arg_6 && Arg_4<=Arg_5 && Arg_4<=Arg_3
f83(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,Arg_7,Arg_8,Arg_9) -> f93(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,Arg_7,Arg_8,Arg_9) :|: Arg_4<=Arg_0 && Arg_4<=Arg_9 && Arg_4<=Arg_8 && Arg_4<=Arg_7 && Arg_4<=Arg_6 && Arg_4<=Arg_5 && Arg_4<=Arg_3
f75(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,Arg_7,Arg_8,Arg_9) -> f83(0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,Arg_7,Arg_8,Arg_9) :|: Arg_4<=Arg_9 && Arg_4<=Arg_8 && Arg_4<=Arg_7 && Arg_4<=Arg_6 && Arg_4<=Arg_5 && Arg_4<=Arg_3 && Arg_4<=Arg_0
f65(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,Arg_7,Arg_8,Arg_9) -> f75(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,Arg_7,Arg_8,0) :|: Arg_4<=Arg_8 && Arg_4<=Arg_7 && Arg_4<=Arg_6 && Arg_4<=Arg_5 && Arg_4<=Arg_3 && Arg_4<=Arg_0
f55(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,Arg_7,Arg_8,Arg_9) -> f65(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,Arg_7,0,Arg_9) :|: Arg_4<=Arg_7 && Arg_4<=Arg_6 && Arg_4<=Arg_5 && Arg_4<=Arg_3 && Arg_4<=Arg_0
f45(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,Arg_7,Arg_8,Arg_9) -> f55(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,0,Arg_8,Arg_9) :|: Arg_4<=Arg_0 && Arg_4<=Arg_6 && Arg_4<=Arg_5 && Arg_4<=Arg_3
f37(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,Arg_7,Arg_8,Arg_9) -> f45(0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,Arg_7,Arg_8,Arg_9) :|: Arg_4<=Arg_6 && Arg_4<=Arg_5 && Arg_4<=Arg_3 && Arg_0<=0 && 0<=Arg_0
f27(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,Arg_7,Arg_8,Arg_9) -> f37(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,0,Arg_7,Arg_8,Arg_9) :|: Arg_4<=Arg_5 && Arg_4<=Arg_3 && Arg_0<=0 && 0<=Arg_0
f17(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,Arg_5,Arg_6,Arg_7,Arg_8,Arg_9) -> f27(Arg_0,Arg_1,Arg_2,Arg_3,Arg_4,0,Arg_6,Arg_7,Arg_8,Arg_9) :|: Arg_4<=Arg_3 && Arg_0<=0 && 0<=Arg_0

G f0 f0 f17 f17 f0->f17 t₀ ∈ g₀ η (Arg_0) = 0 η (Arg_1) = K η (Arg_2) = L η (Arg_3) = 0 f17->f17 t₁ ∈ g₁ p = 3/4 η (Arg_3) = Arg_3+1 τ = Arg_3+1<=Arg_4 f17->f17 t₂ ∈ g₁ p = 1/4 η (Arg_3) = Arg_3-1 τ = Arg_3+1<=Arg_4 f27 f27 f17->f27 t₂₄ ∈ g₁₆ η (Arg_5) = 0 τ = Arg_4<=Arg_3 f27->f27 t₃ ∈ g₂ p = 3/4 η (Arg_5) = Arg_5+1 τ = Arg_5+1<=Arg_4 f27->f27 t₄ ∈ g₂ p = 1/4 η (Arg_5) = Arg_5-1 τ = Arg_5+1<=Arg_4 f37 f37 f27->f37 t₂₃ ∈ g₁₅ η (Arg_6) = 0 τ = Arg_4<=Arg_5 f37->f37 t₅ ∈ g₃ p = 3/4 η (Arg_6) = Arg_6+1 τ = Arg_6+1<=Arg_4 f37->f37 t₆ ∈ g₃ p = 1/4 η (Arg_6) = Arg_6-1 τ = Arg_6+1<=Arg_4 f45 f45 f37->f45 t₂₂ ∈ g₁₄ η (Arg_0) = 0 τ = Arg_4<=Arg_6 f45->f45 t₇ ∈ g₄ p = 3/4 η (Arg_0) = Arg_0+1 τ = Arg_0+1<=Arg_4 f45->f45 t₈ ∈ g₄ p = 1/4 η (Arg_0) = Arg_0-1 τ = Arg_0+1<=Arg_4 f55 f55 f45->f55 t₂₁ ∈ g₁₃ η (Arg_7) = 0 τ = Arg_4<=Arg_0 f55->f55 t₉ ∈ g₅ p = 3/4 η (Arg_7) = Arg_7+1 τ = Arg_7+1<=Arg_4 f55->f55 t₁₀ ∈ g₅ p = 1/4 η (Arg_7) = Arg_7-1 τ = Arg_7+1<=Arg_4 f65 f65 f55->f65 t₂₀ ∈ g₁₂ η (Arg_8) = 0 τ = Arg_4<=Arg_7 f65->f65 t₁₁ ∈ g₆ p = 3/4 η (Arg_8) = Arg_8+1 τ = Arg_8+1<=Arg_4 f65->f65 t₁₂ ∈ g₆ p = 1/4 η (Arg_8) = Arg_8-1 τ = Arg_8+1<=Arg_4 f75 f75 f65->f75 t₁₉ ∈ g₁₁ η (Arg_9) = 0 τ = Arg_4<=Arg_8 f75->f75 t₁₃ ∈ g₇ p = 3/4 η (Arg_9) = Arg_9+1 τ = Arg_9+1<=Arg_4 f75->f75 t₁₄ ∈ g₇ p = 1/4 η (Arg_9) = Arg_9-1 τ = Arg_9+1<=Arg_4 f83 f83 f75->f83 t₁₈ ∈ g₁₀ η (Arg_0) = 0 τ = Arg_4<=Arg_9 f83->f83 t₁₅ ∈ g₈ p = 3/4 η (Arg_0) = Arg_0+1 τ = Arg_0+1<=Arg_4 f83->f83 t₁₆ ∈ g₈ p = 1/4 η (Arg_0) = Arg_0-1 τ = Arg_0+1<=Arg_4 f93 f93 f83->f93 t₁₇ ∈ g₉ τ = Arg_4<=Arg_0

Timebounds:

Overall timebound:inf {Infinity}
0,0: f0->f17: 1 {O(1)}
1,1: f17->f17: inf {Infinity}
2,1: f17->f17: inf {Infinity}
24,16: f17->f27: 1 {O(1)}
3,2: f27->f27: inf {Infinity}
4,2: f27->f27: inf {Infinity}
23,15: f27->f37: 1 {O(1)}
5,3: f37->f37: inf {Infinity}
6,3: f37->f37: inf {Infinity}
22,14: f37->f45: 1 {O(1)}
7,4: f45->f45: inf {Infinity}
8,4: f45->f45: inf {Infinity}
21,13: f45->f55: 1 {O(1)}
9,5: f55->f55: inf {Infinity}
10,5: f55->f55: inf {Infinity}
20,12: f55->f65: 1 {O(1)}
11,6: f65->f65: inf {Infinity}
12,6: f65->f65: inf {Infinity}
19,11: f65->f75: 1 {O(1)}
13,7: f75->f75: inf {Infinity}
14,7: f75->f75: inf {Infinity}
18,10: f75->f83: 1 {O(1)}
15,8: f83->f83: inf {Infinity}
16,8: f83->f83: inf {Infinity}
17,9: f83->f93: 1 {O(1)}

Expected Timebounds:

Overall expected timebound: 282*Arg_4+9 {O(n)}
0: f0->[1:f17]: 1 {O(1)}
1: f17->[3/4:f17; 1/4:f17]: 2*Arg_4 {O(n)}
2: f27->[3/4:f27; 1/4:f27]: 4*Arg_4 {O(n)}
3: f37->[3/4:f37; 1/4:f37]: 2*Arg_4 {O(n)}
4: f45->[3/4:f45; 1/4:f45]: 16*Arg_4 {O(n)}
5: f55->[3/4:f55; 1/4:f55]: 2*Arg_4 {O(n)}
6: f65->[3/4:f65; 1/4:f65]: 64*Arg_4 {O(n)}
7: f75->[3/4:f75; 1/4:f75]: 128*Arg_4 {O(n)}
8: f83->[3/4:f83; 1/4:f83]: 64*Arg_4 {O(n)}
9: f83->[1:f93]: 1 {O(1)}
10: f75->[1:f83]: 1 {O(1)}
11: f65->[1:f75]: 1 {O(1)}
12: f55->[1:f65]: 1 {O(1)}
13: f45->[1:f55]: 1 {O(1)}
14: f37->[1:f45]: 1 {O(1)}
15: f27->[1:f37]: 1 {O(1)}
16: f17->[1:f27]: 1 {O(1)}

Costbounds:

Overall costbound: inf {Infinity}
0,0: f0->f17: inf {Infinity}
1,1: f17->f17: inf {Infinity}
2,1: f17->f17: inf {Infinity}
24,16: f17->f27: inf {Infinity}
3,2: f27->f27: inf {Infinity}
4,2: f27->f27: inf {Infinity}
23,15: f27->f37: inf {Infinity}
5,3: f37->f37: inf {Infinity}
6,3: f37->f37: inf {Infinity}
22,14: f37->f45: inf {Infinity}
7,4: f45->f45: inf {Infinity}
8,4: f45->f45: inf {Infinity}
21,13: f45->f55: inf {Infinity}
9,5: f55->f55: inf {Infinity}
10,5: f55->f55: inf {Infinity}
20,12: f55->f65: inf {Infinity}
11,6: f65->f65: inf {Infinity}
12,6: f65->f65: inf {Infinity}
19,11: f65->f75: inf {Infinity}
13,7: f75->f75: inf {Infinity}
14,7: f75->f75: inf {Infinity}
18,10: f75->f83: inf {Infinity}
15,8: f83->f83: inf {Infinity}
16,8: f83->f83: inf {Infinity}
17,9: f83->f93: inf {Infinity}

Expected Costbounds:

Overall expected costbound: 282*Arg_4+9 {O(n)}
0: f0->[1:f17]: 1 {O(1)}
1: f17->[3/4:f17; 1/4:f17]: 2*Arg_4 {O(n)}
2: f27->[3/4:f27; 1/4:f27]: 4*Arg_4 {O(n)}
3: f37->[3/4:f37; 1/4:f37]: 2*Arg_4 {O(n)}
4: f45->[3/4:f45; 1/4:f45]: 16*Arg_4 {O(n)}
5: f55->[3/4:f55; 1/4:f55]: 2*Arg_4 {O(n)}
6: f65->[3/4:f65; 1/4:f65]: 64*Arg_4 {O(n)}
7: f75->[3/4:f75; 1/4:f75]: 128*Arg_4 {O(n)}
8: f83->[3/4:f83; 1/4:f83]: 64*Arg_4 {O(n)}
9: f83->[1:f93]: 1 {O(1)}
10: f75->[1:f83]: 1 {O(1)}
11: f65->[1:f75]: 1 {O(1)}
12: f55->[1:f65]: 1 {O(1)}
13: f45->[1:f55]: 1 {O(1)}
14: f37->[1:f45]: 1 {O(1)}
15: f27->[1:f37]: 1 {O(1)}
16: f17->[1:f27]: 1 {O(1)}

Sizebounds:

0,0: f0->f17, Arg_0: 0 {O(1)}
0,0: f0->f17, Arg_3: 0 {O(1)}
0,0: f0->f17, Arg_4: Arg_4 {O(n)}
0,0: f0->f17, Arg_5: Arg_5 {O(n)}
0,0: f0->f17, Arg_6: Arg_6 {O(n)}
0,0: f0->f17, Arg_7: Arg_7 {O(n)}
0,0: f0->f17, Arg_8: Arg_8 {O(n)}
0,0: f0->f17, Arg_9: Arg_9 {O(n)}
1,1: f17->f17, Arg_0: 0 {O(1)}
1,1: f17->f17, Arg_4: Arg_4 {O(n)}
1,1: f17->f17, Arg_5: Arg_5 {O(n)}
1,1: f17->f17, Arg_6: Arg_6 {O(n)}
1,1: f17->f17, Arg_7: Arg_7 {O(n)}
1,1: f17->f17, Arg_8: Arg_8 {O(n)}
1,1: f17->f17, Arg_9: Arg_9 {O(n)}
2,1: f17->f17, Arg_0: 0 {O(1)}
2,1: f17->f17, Arg_4: Arg_4 {O(n)}
2,1: f17->f17, Arg_5: Arg_5 {O(n)}
2,1: f17->f17, Arg_6: Arg_6 {O(n)}
2,1: f17->f17, Arg_7: Arg_7 {O(n)}
2,1: f17->f17, Arg_8: Arg_8 {O(n)}
2,1: f17->f17, Arg_9: Arg_9 {O(n)}
24,16: f17->f27, Arg_0: 0 {O(1)}
24,16: f17->f27, Arg_4: Arg_4 {O(n)}
24,16: f17->f27, Arg_5: 0 {O(1)}
24,16: f17->f27, Arg_6: Arg_6 {O(n)}
24,16: f17->f27, Arg_7: Arg_7 {O(n)}
24,16: f17->f27, Arg_8: Arg_8 {O(n)}
24,16: f17->f27, Arg_9: Arg_9 {O(n)}
3,2: f27->f27, Arg_0: 0 {O(1)}
3,2: f27->f27, Arg_4: Arg_4 {O(n)}
3,2: f27->f27, Arg_6: Arg_6 {O(n)}
3,2: f27->f27, Arg_7: Arg_7 {O(n)}
3,2: f27->f27, Arg_8: Arg_8 {O(n)}
3,2: f27->f27, Arg_9: Arg_9 {O(n)}
4,2: f27->f27, Arg_0: 0 {O(1)}
4,2: f27->f27, Arg_4: Arg_4 {O(n)}
4,2: f27->f27, Arg_6: Arg_6 {O(n)}
4,2: f27->f27, Arg_7: Arg_7 {O(n)}
4,2: f27->f27, Arg_8: Arg_8 {O(n)}
4,2: f27->f27, Arg_9: Arg_9 {O(n)}
23,15: f27->f37, Arg_0: 0 {O(1)}
23,15: f27->f37, Arg_4: Arg_4 {O(n)}
23,15: f27->f37, Arg_6: 0 {O(1)}
23,15: f27->f37, Arg_7: Arg_7 {O(n)}
23,15: f27->f37, Arg_8: Arg_8 {O(n)}
23,15: f27->f37, Arg_9: Arg_9 {O(n)}
5,3: f37->f37, Arg_0: 0 {O(1)}
5,3: f37->f37, Arg_4: Arg_4 {O(n)}
5,3: f37->f37, Arg_7: Arg_7 {O(n)}
5,3: f37->f37, Arg_8: Arg_8 {O(n)}
5,3: f37->f37, Arg_9: Arg_9 {O(n)}
6,3: f37->f37, Arg_0: 0 {O(1)}
6,3: f37->f37, Arg_4: Arg_4 {O(n)}
6,3: f37->f37, Arg_7: Arg_7 {O(n)}
6,3: f37->f37, Arg_8: Arg_8 {O(n)}
6,3: f37->f37, Arg_9: Arg_9 {O(n)}
22,14: f37->f45, Arg_0: 0 {O(1)}
22,14: f37->f45, Arg_4: Arg_4 {O(n)}
22,14: f37->f45, Arg_7: Arg_7 {O(n)}
22,14: f37->f45, Arg_8: Arg_8 {O(n)}
22,14: f37->f45, Arg_9: Arg_9 {O(n)}
7,4: f45->f45, Arg_4: Arg_4 {O(n)}
7,4: f45->f45, Arg_7: Arg_7 {O(n)}
7,4: f45->f45, Arg_8: Arg_8 {O(n)}
7,4: f45->f45, Arg_9: Arg_9 {O(n)}
8,4: f45->f45, Arg_4: Arg_4 {O(n)}
8,4: f45->f45, Arg_7: Arg_7 {O(n)}
8,4: f45->f45, Arg_8: Arg_8 {O(n)}
8,4: f45->f45, Arg_9: Arg_9 {O(n)}
21,13: f45->f55, Arg_4: Arg_4 {O(n)}
21,13: f45->f55, Arg_7: 0 {O(1)}
21,13: f45->f55, Arg_8: Arg_8 {O(n)}
21,13: f45->f55, Arg_9: Arg_9 {O(n)}
9,5: f55->f55, Arg_4: Arg_4 {O(n)}
9,5: f55->f55, Arg_8: Arg_8 {O(n)}
9,5: f55->f55, Arg_9: Arg_9 {O(n)}
10,5: f55->f55, Arg_4: Arg_4 {O(n)}
10,5: f55->f55, Arg_8: Arg_8 {O(n)}
10,5: f55->f55, Arg_9: Arg_9 {O(n)}
20,12: f55->f65, Arg_4: Arg_4 {O(n)}
20,12: f55->f65, Arg_8: 0 {O(1)}
20,12: f55->f65, Arg_9: Arg_9 {O(n)}
11,6: f65->f65, Arg_4: Arg_4 {O(n)}
11,6: f65->f65, Arg_9: Arg_9 {O(n)}
12,6: f65->f65, Arg_4: Arg_4 {O(n)}
12,6: f65->f65, Arg_9: Arg_9 {O(n)}
19,11: f65->f75, Arg_4: Arg_4 {O(n)}
19,11: f65->f75, Arg_9: 0 {O(1)}
13,7: f75->f75, Arg_4: Arg_4 {O(n)}
14,7: f75->f75, Arg_4: Arg_4 {O(n)}
18,10: f75->f83, Arg_0: 0 {O(1)}
18,10: f75->f83, Arg_4: Arg_4 {O(n)}
15,8: f83->f83, Arg_4: Arg_4 {O(n)}
16,8: f83->f83, Arg_4: Arg_4 {O(n)}
17,9: f83->f93, Arg_4: Arg_4 {O(n)}

ExpSizeBounds:

(0: f0->[1:f17], f17), K: K {O(n)}
(0: f0->[1:f17], f17), L: L {O(n)}
(0: f0->[1:f17], f17), Arg_0: 0 {O(1)}
(0: f0->[1:f17], f17), Arg_3: 0 {O(1)}
(0: f0->[1:f17], f17), Arg_4: Arg_4 {O(n)}
(0: f0->[1:f17], f17), Arg_5: Arg_5 {O(n)}
(0: f0->[1:f17], f17), Arg_6: Arg_6 {O(n)}
(0: f0->[1:f17], f17), Arg_7: Arg_7 {O(n)}
(0: f0->[1:f17], f17), Arg_8: Arg_8 {O(n)}
(0: f0->[1:f17], f17), Arg_9: Arg_9 {O(n)}
(1: f17->[3/4:f17; 1/4:f17], f17), K: K {O(n)}
(1: f17->[3/4:f17; 1/4:f17], f17), L: L {O(n)}
(1: f17->[3/4:f17; 1/4:f17], f17), Arg_0: 0 {O(1)}
(1: f17->[3/4:f17; 1/4:f17], f17), Arg_3: 2*Arg_4 {O(n)}
(1: f17->[3/4:f17; 1/4:f17], f17), Arg_4: Arg_4 {O(n)}
(1: f17->[3/4:f17; 1/4:f17], f17), Arg_5: Arg_5 {O(n)}
(1: f17->[3/4:f17; 1/4:f17], f17), Arg_6: Arg_6 {O(n)}
(1: f17->[3/4:f17; 1/4:f17], f17), Arg_7: Arg_7 {O(n)}
(1: f17->[3/4:f17; 1/4:f17], f17), Arg_8: Arg_8 {O(n)}
(1: f17->[3/4:f17; 1/4:f17], f17), Arg_9: Arg_9 {O(n)}
(2: f27->[3/4:f27; 1/4:f27], f27), K: 2*K {O(n)}
(2: f27->[3/4:f27; 1/4:f27], f27), L: 2*L {O(n)}
(2: f27->[3/4:f27; 1/4:f27], f27), Arg_0: 0 {O(1)}
(2: f27->[3/4:f27; 1/4:f27], f27), Arg_3: 2*Arg_4 {O(n)}
(2: f27->[3/4:f27; 1/4:f27], f27), Arg_4: Arg_4 {O(n)}
(2: f27->[3/4:f27; 1/4:f27], f27), Arg_5: 4*Arg_4 {O(n)}
(2: f27->[3/4:f27; 1/4:f27], f27), Arg_6: Arg_6 {O(n)}
(2: f27->[3/4:f27; 1/4:f27], f27), Arg_7: Arg_7 {O(n)}
(2: f27->[3/4:f27; 1/4:f27], f27), Arg_8: Arg_8 {O(n)}
(2: f27->[3/4:f27; 1/4:f27], f27), Arg_9: Arg_9 {O(n)}
(3: f37->[3/4:f37; 1/4:f37], f37), K: 4*K {O(n)}
(3: f37->[3/4:f37; 1/4:f37], f37), L: 4*L {O(n)}
(3: f37->[3/4:f37; 1/4:f37], f37), Arg_0: 0 {O(1)}
(3: f37->[3/4:f37; 1/4:f37], f37), Arg_3: 4*Arg_4 {O(n)}
(3: f37->[3/4:f37; 1/4:f37], f37), Arg_4: Arg_4 {O(n)}
(3: f37->[3/4:f37; 1/4:f37], f37), Arg_5: 4*Arg_4 {O(n)}
(3: f37->[3/4:f37; 1/4:f37], f37), Arg_6: 2*Arg_4 {O(n)}
(3: f37->[3/4:f37; 1/4:f37], f37), Arg_7: Arg_7 {O(n)}
(3: f37->[3/4:f37; 1/4:f37], f37), Arg_8: Arg_8 {O(n)}
(3: f37->[3/4:f37; 1/4:f37], f37), Arg_9: Arg_9 {O(n)}
(4: f45->[3/4:f45; 1/4:f45], f45), K: 8*K {O(n)}
(4: f45->[3/4:f45; 1/4:f45], f45), L: 8*L {O(n)}
(4: f45->[3/4:f45; 1/4:f45], f45), Arg_0: 16*Arg_4 {O(n)}
(4: f45->[3/4:f45; 1/4:f45], f45), Arg_3: 8*Arg_4 {O(n)}
(4: f45->[3/4:f45; 1/4:f45], f45), Arg_4: Arg_4 {O(n)}
(4: f45->[3/4:f45; 1/4:f45], f45), Arg_5: 8*Arg_4 {O(n)}
(4: f45->[3/4:f45; 1/4:f45], f45), Arg_6: 2*Arg_4 {O(n)}
(4: f45->[3/4:f45; 1/4:f45], f45), Arg_7: Arg_7 {O(n)}
(4: f45->[3/4:f45; 1/4:f45], f45), Arg_8: Arg_8 {O(n)}
(4: f45->[3/4:f45; 1/4:f45], f45), Arg_9: Arg_9 {O(n)}
(5: f55->[3/4:f55; 1/4:f55], f55), K: 16*K {O(n)}
(5: f55->[3/4:f55; 1/4:f55], f55), L: 16*L {O(n)}
(5: f55->[3/4:f55; 1/4:f55], f55), Arg_0: 16*Arg_4 {O(n)}
(5: f55->[3/4:f55; 1/4:f55], f55), Arg_3: 16*Arg_4 {O(n)}
(5: f55->[3/4:f55; 1/4:f55], f55), Arg_4: Arg_4 {O(n)}
(5: f55->[3/4:f55; 1/4:f55], f55), Arg_5: 16*Arg_4 {O(n)}
(5: f55->[3/4:f55; 1/4:f55], f55), Arg_6: 4*Arg_4 {O(n)}
(5: f55->[3/4:f55; 1/4:f55], f55), Arg_7: 2*Arg_4 {O(n)}
(5: f55->[3/4:f55; 1/4:f55], f55), Arg_8: Arg_8 {O(n)}
(5: f55->[3/4:f55; 1/4:f55], f55), Arg_9: Arg_9 {O(n)}
(6: f65->[3/4:f65; 1/4:f65], f65), K: 32*K {O(n)}
(6: f65->[3/4:f65; 1/4:f65], f65), L: 32*L {O(n)}
(6: f65->[3/4:f65; 1/4:f65], f65), Arg_0: 32*Arg_4 {O(n)}
(6: f65->[3/4:f65; 1/4:f65], f65), Arg_3: 32*Arg_4 {O(n)}
(6: f65->[3/4:f65; 1/4:f65], f65), Arg_4: Arg_4 {O(n)}
(6: f65->[3/4:f65; 1/4:f65], f65), Arg_5: 32*Arg_4 {O(n)}
(6: f65->[3/4:f65; 1/4:f65], f65), Arg_6: 8*Arg_4 {O(n)}
(6: f65->[3/4:f65; 1/4:f65], f65), Arg_7: 2*Arg_4 {O(n)}
(6: f65->[3/4:f65; 1/4:f65], f65), Arg_8: 64*Arg_4 {O(n)}
(6: f65->[3/4:f65; 1/4:f65], f65), Arg_9: Arg_9 {O(n)}
(7: f75->[3/4:f75; 1/4:f75], f75), K: 64*K {O(n)}
(7: f75->[3/4:f75; 1/4:f75], f75), L: 64*L {O(n)}
(7: f75->[3/4:f75; 1/4:f75], f75), Arg_0: 64*Arg_4 {O(n)}
(7: f75->[3/4:f75; 1/4:f75], f75), Arg_3: 64*Arg_4 {O(n)}
(7: f75->[3/4:f75; 1/4:f75], f75), Arg_4: Arg_4 {O(n)}
(7: f75->[3/4:f75; 1/4:f75], f75), Arg_5: 64*Arg_4 {O(n)}
(7: f75->[3/4:f75; 1/4:f75], f75), Arg_6: 16*Arg_4 {O(n)}
(7: f75->[3/4:f75; 1/4:f75], f75), Arg_7: 4*Arg_4 {O(n)}
(7: f75->[3/4:f75; 1/4:f75], f75), Arg_8: 64*Arg_4 {O(n)}
(7: f75->[3/4:f75; 1/4:f75], f75), Arg_9: 128*Arg_4 {O(n)}
(8: f83->[3/4:f83; 1/4:f83], f83), K: 128*K {O(n)}
(8: f83->[3/4:f83; 1/4:f83], f83), L: 128*L {O(n)}
(8: f83->[3/4:f83; 1/4:f83], f83), Arg_0: 64*Arg_4 {O(n)}
(8: f83->[3/4:f83; 1/4:f83], f83), Arg_3: 128*Arg_4 {O(n)}
(8: f83->[3/4:f83; 1/4:f83], f83), Arg_4: Arg_4 {O(n)}
(8: f83->[3/4:f83; 1/4:f83], f83), Arg_5: 128*Arg_4 {O(n)}
(8: f83->[3/4:f83; 1/4:f83], f83), Arg_6: 32*Arg_4 {O(n)}
(8: f83->[3/4:f83; 1/4:f83], f83), Arg_7: 8*Arg_4 {O(n)}
(8: f83->[3/4:f83; 1/4:f83], f83), Arg_8: 128*Arg_4 {O(n)}
(8: f83->[3/4:f83; 1/4:f83], f83), Arg_9: 128*Arg_4 {O(n)}
(9: f83->[1:f93], f93), K: 256*K {O(n)}
(9: f83->[1:f93], f93), L: 256*L {O(n)}
(9: f83->[1:f93], f93), Arg_0: 64*Arg_4 {O(n)}
(9: f83->[1:f93], f93), Arg_3: 256*Arg_4 {O(n)}
(9: f83->[1:f93], f93), Arg_4: Arg_4 {O(n)}
(9: f83->[1:f93], f93), Arg_5: 256*Arg_4 {O(n)}
(9: f83->[1:f93], f93), Arg_6: 64*Arg_4 {O(n)}
(9: f83->[1:f93], f93), Arg_7: 16*Arg_4 {O(n)}
(9: f83->[1:f93], f93), Arg_8: 256*Arg_4 {O(n)}
(9: f83->[1:f93], f93), Arg_9: 256*Arg_4 {O(n)}
(10: f75->[1:f83], f83), K: 128*K {O(n)}
(10: f75->[1:f83], f83), L: 128*L {O(n)}
(10: f75->[1:f83], f83), Arg_0: 0 {O(1)}
(10: f75->[1:f83], f83), Arg_3: 128*Arg_4 {O(n)}
(10: f75->[1:f83], f83), Arg_4: Arg_4 {O(n)}
(10: f75->[1:f83], f83), Arg_5: 128*Arg_4 {O(n)}
(10: f75->[1:f83], f83), Arg_6: 32*Arg_4 {O(n)}
(10: f75->[1:f83], f83), Arg_7: 8*Arg_4 {O(n)}
(10: f75->[1:f83], f83), Arg_8: 128*Arg_4 {O(n)}
(10: f75->[1:f83], f83), Arg_9: 128*Arg_4 {O(n)}
(11: f65->[1:f75], f75), K: 64*K {O(n)}
(11: f65->[1:f75], f75), L: 64*L {O(n)}
(11: f65->[1:f75], f75), Arg_0: 64*Arg_4 {O(n)}
(11: f65->[1:f75], f75), Arg_3: 64*Arg_4 {O(n)}
(11: f65->[1:f75], f75), Arg_4: Arg_4 {O(n)}
(11: f65->[1:f75], f75), Arg_5: 64*Arg_4 {O(n)}
(11: f65->[1:f75], f75), Arg_6: 16*Arg_4 {O(n)}
(11: f65->[1:f75], f75), Arg_7: 4*Arg_4 {O(n)}
(11: f65->[1:f75], f75), Arg_8: 64*Arg_4 {O(n)}
(11: f65->[1:f75], f75), Arg_9: 0 {O(1)}
(12: f55->[1:f65], f65), K: 32*K {O(n)}
(12: f55->[1:f65], f65), L: 32*L {O(n)}
(12: f55->[1:f65], f65), Arg_0: 32*Arg_4 {O(n)}
(12: f55->[1:f65], f65), Arg_3: 32*Arg_4 {O(n)}
(12: f55->[1:f65], f65), Arg_4: Arg_4 {O(n)}
(12: f55->[1:f65], f65), Arg_5: 32*Arg_4 {O(n)}
(12: f55->[1:f65], f65), Arg_6: 8*Arg_4 {O(n)}
(12: f55->[1:f65], f65), Arg_7: 2*Arg_4 {O(n)}
(12: f55->[1:f65], f65), Arg_8: 0 {O(1)}
(12: f55->[1:f65], f65), Arg_9: Arg_9 {O(n)}
(13: f45->[1:f55], f55), K: 16*K {O(n)}
(13: f45->[1:f55], f55), L: 16*L {O(n)}
(13: f45->[1:f55], f55), Arg_0: 16*Arg_4 {O(n)}
(13: f45->[1:f55], f55), Arg_3: 16*Arg_4 {O(n)}
(13: f45->[1:f55], f55), Arg_4: Arg_4 {O(n)}
(13: f45->[1:f55], f55), Arg_5: 16*Arg_4 {O(n)}
(13: f45->[1:f55], f55), Arg_6: 4*Arg_4 {O(n)}
(13: f45->[1:f55], f55), Arg_7: 0 {O(1)}
(13: f45->[1:f55], f55), Arg_8: Arg_8 {O(n)}
(13: f45->[1:f55], f55), Arg_9: Arg_9 {O(n)}
(14: f37->[1:f45], f45), K: 8*K {O(n)}
(14: f37->[1:f45], f45), L: 8*L {O(n)}
(14: f37->[1:f45], f45), Arg_0: 0 {O(1)}
(14: f37->[1:f45], f45), Arg_3: 8*Arg_4 {O(n)}
(14: f37->[1:f45], f45), Arg_4: Arg_4 {O(n)}
(14: f37->[1:f45], f45), Arg_5: 8*Arg_4 {O(n)}
(14: f37->[1:f45], f45), Arg_6: 2*Arg_4 {O(n)}
(14: f37->[1:f45], f45), Arg_7: Arg_7 {O(n)}
(14: f37->[1:f45], f45), Arg_8: Arg_8 {O(n)}
(14: f37->[1:f45], f45), Arg_9: Arg_9 {O(n)}
(15: f27->[1:f37], f37), K: 4*K {O(n)}
(15: f27->[1:f37], f37), L: 4*L {O(n)}
(15: f27->[1:f37], f37), Arg_0: 0 {O(1)}
(15: f27->[1:f37], f37), Arg_3: 4*Arg_4 {O(n)}
(15: f27->[1:f37], f37), Arg_4: Arg_4 {O(n)}
(15: f27->[1:f37], f37), Arg_5: 4*Arg_4 {O(n)}
(15: f27->[1:f37], f37), Arg_6: 0 {O(1)}
(15: f27->[1:f37], f37), Arg_7: Arg_7 {O(n)}
(15: f27->[1:f37], f37), Arg_8: Arg_8 {O(n)}
(15: f27->[1:f37], f37), Arg_9: Arg_9 {O(n)}
(16: f17->[1:f27], f27), K: 2*K {O(n)}
(16: f17->[1:f27], f27), L: 2*L {O(n)}
(16: f17->[1:f27], f27), Arg_0: 0 {O(1)}
(16: f17->[1:f27], f27), Arg_3: 2*Arg_4 {O(n)}
(16: f17->[1:f27], f27), Arg_4: Arg_4 {O(n)}
(16: f17->[1:f27], f27), Arg_5: 0 {O(1)}
(16: f17->[1:f27], f27), Arg_6: Arg_6 {O(n)}
(16: f17->[1:f27], f27), Arg_7: Arg_7 {O(n)}
(16: f17->[1:f27], f27), Arg_8: Arg_8 {O(n)}
(16: f17->[1:f27], f27), Arg_9: Arg_9 {O(n)}