THEORY OPOBalanceX IS
  SimulationImp,21;
  ValuesLemmas,1;
  InstanciatedConstraintsLemmas,0;
  Initialisation,1;
  main,19
END
&
THEORY OPOProofList IS
  btrue & main.19,(_of(18) & _of(19) => _of(2));
  btrue & main.18,(_f(14) & _of(5) => _of(17));
  btrue & main.17,(_f(13) & _of(5) => _of(17));
  btrue & main.16,(_f(12) & _of(5) => _of(17));
  btrue & main.15,(_f(11) & _of(5) => _of(17));
  btrue & main.14,(_f(8) & _of(5) => _of(17));
  btrue & main.13,(_f(3) & _of(5) => _of(16));
  btrue & main.12,(_f(3) & _of(5) => _of(15));
  btrue & main.11,(_f(3) & _of(5) => _of(14));
  btrue & main.10,(_f(3) & _of(5) => _of(13));
  btrue & main.9,(_f(3) & _of(5) => _of(12));
  btrue & main.8,(_f(3) & _of(5) => _of(10));
  btrue & main.7,(_of(9) & _of(5) => _of(11));
  btrue & main.6,(_of(9) & _of(5) => _of(10));
  btrue & main.5,(_of(5) => _of(8));
  btrue & main.4,(_of(5) => _of(7));
  btrue & main.3,(_of(5) => _of(6));
  btrue & main.2,(_of(5) => _of(2));
  btrue & main.1,(_of(4) => _of(2));
  Initialisation.1,(_of(3) => _of(2));
  ValuesLemmas.1,(_of(1) => _of(2))
END
&
THEORY OPOFormulas IS
  "`Check that the property (btrue) is preserved by the valuations - ref 5.2'";
  (btrue);
  "`Check preconditions of called operation, or While loop construction, or Assert predicates'" & "`Check initialisation refinement - ref 4.3, 5.4'" & "`Check that the invariant (btrue) is established by the initialisation - ref 4.3, 5.4'";
  "`Check precondition (btrue) deduction'";
  "`Check preconditions of called operation, or While loop construction, or Assert predicates'";
  (2147483647: INTEGER);
  (0<=2147483647);
  (2147483647<=2147483647);
  ("`Local hypotheses'" & ch: 0..3 & ctr: INTEGER & 0<=ctr & ctr<=2147483647);
  (ctr: INTEGER);
  (0<=ctr);
  (ctr<=2147483647);
  (1: INTEGER);
  (-2147483647<=1);
  (3: INTEGER);
  (0: INTEGER);
  (bb$0: 0..3);
  ("`Local hypotheses'" & not(not(ch$7777 = 0) & 1<=ctr$7777) & ch$7777: 0..3 & ctr$7777: INTEGER & 0<=ctr$7777 & ctr$7777<=2147483647);
  "`Check operation refinement - ref 4.4, 5.5'" & "`Check that the invariant (btrue) is preserved by the operation - ref 4.4, 5.5'"
END
&
THEORY Version IS
  POVersion(V3.6.8)(CLT == "V3.7.2")(local_op == OK)
END