The symbolic WCET provided by the timing schema is evaluated by Maple to compute the WCET of the program.

push := (P,x) -> [x,op(P)]:
pow := (a,b) -> a^b:

`&U`:= proc() local i,L;
   L:=[(args[1])[i] $ i = 1 .. nops(args[1]) , (args[2])[i] $ i = 1.. nops(args[2])];
  RETURN(L)
end:

wcet_1 := proc(P)
  RETURN([[55,[]]]);
end:

wcet_2 := proc(P)
  RETURN([[4,[]]]);
end:

wcet_3 := proc(P)
  RETURN([[2,[0]]]);
end:

wcet_E3 := proc(P)
  RETURN([[2,[0]]]);
end:

wcet_42 := proc(P)
  RETURN(
    Mult( wcet_25(push(P,pow(2,(i42+1)))) &U
      wcet_39(push(P,pow(2,(i42+1)))) &U
      wcet_40(push(P,pow(2,(i42+1)))) ,
      11 , [2] , i42
    ) &U
    wcet_E25(push(P,pow(2,((11)+1)))) &U
    wcet_41(push(P,pow(2,((11)+1)))) ,
  );
end:

wcet_43 := proc(P)
RETURN([[6,[]]]);
end:

wcet_44 := proc(P)
  RETURN(
    wcet_1(P) &U
    wcet_2(P) &U
    wcet_7(P) &U
    wcet_8(P) &U
    wcet_9(P) &U
    wcet_23(P) &U
    wcet_24(P) &U
    wcet_42(P) &U
    wcet_43(P)
  );
end:

wcet_44([]):