THEORY ProofList IS
  btrue & main.38,(_f(17) & _f(1) => _f(5));
  btrue & main.37,(_f(17) & _f(1) => _f(15));
  btrue & main.36,(_f(17) & _f(1) => _f(4));
  btrue & main.35,(_f(17) & _f(1) => _f(14));
  btrue & main.34,(_f(17) & _f(1) => _f(13));
  btrue & main.33,(_f(16) & _f(1) => _f(5));
  btrue & main.32,(_f(16) & _f(1) => _f(15));
  btrue & main.31,(_f(16) & _f(1) => _f(4));
  btrue & main.30,(_f(16) & _f(1) => _f(14));
  btrue & main.29,(_f(16) & _f(1) => _f(13));
  btrue & main.28,(_f(11) & _f(1) => _f(5));
  btrue & main.27,(_f(11) & _f(1) => _f(15));
  btrue & main.26,(_f(11) & _f(1) => _f(4));
  btrue & main.25,(_f(11) & _f(1) => _f(14));
  btrue & main.24,(_f(11) & _f(1) => _f(13));
  btrue & main.23,(_f(10) & _f(1) => _f(5));
  btrue & main.22,(_f(10) & _f(1) => _f(15));
  btrue & main.21,(_f(10) & _f(1) => _f(4));
  btrue & main.20,(_f(10) & _f(1) => _f(14));
  btrue & main.19,(_f(10) & _f(1) => _f(13));
  btrue & main.18,(_f(8) & _f(1) => _f(5));
  btrue & main.17,(_f(8) & _f(1) => _f(15));
  btrue & main.16,(_f(8) & _f(1) => _f(4));
  btrue & main.15,(_f(8) & _f(1) => _f(14));
  btrue & main.14,(_f(8) & _f(1) => _f(13));
  btrue & main.13,(_f(12) & _f(1) => _f(5));
  btrue & main.12,(_f(12) & _f(1) => _f(15));
  btrue & main.11,(_f(12) & _f(1) => _f(4));
  btrue & main.10,(_f(12) & _f(1) => _f(14));
  btrue & main.9,(_f(12) & _f(1) => _f(13));
  btrue & main.8,(_f(11) & _f(1) => _f(9));
  btrue & main.7,(_f(10) & _f(1) => _f(9));
  btrue & main.6,(_f(8) & _f(1) => _f(9));
  btrue & main.5,(_f(3) & _f(1) => _f(7));
  btrue & main.4,(_f(3) & _f(1) => _f(6));
  btrue & main.3,(_f(3) & _f(1) => _f(5));
  btrue & main.2,(_f(3) & _f(1) => _f(4));
  btrue & main.1,(_f(1) => _f(2))
END
&
THEORY Formulas IS
  "`Check preconditions of called operation, or While loop construction, or Assert predicates'";
  (1: 0..3);
  ("`Local hypotheses'" & ch: 0..3 & ctr: INTEGER & 0<=ctr & ctr<=2147483647 & not(ch = 0) & 1<=ctr);
  (ctr-1: INTEGER);
  (ctr-1<=2147483647);
  (-2147483647<=ctr-1);
  (-2147483647<=ctr);
  ("`Local hypotheses'" & ch: 0..3 & ctr: INTEGER & 0<=ctr & ctr<=2147483647 & not(ch = 0) & 1<=ctr & bb$0: 0..4 & not(bb$0 = 0) & not(bb$0 = 4) & not(bb$0 = 3) & not(bb$0 = 2) & bb$0 = 1);
  (IdParking: 0..10);
  ("`Local hypotheses'" & ch: 0..3 & ctr: INTEGER & 0<=ctr & ctr<=2147483647 & not(ch = 0) & 1<=ctr & bb$0: 0..4 & not(bb$0 = 0) & not(bb$0 = 1) & not(bb$0 = 4) & not(bb$0 = 3) & bb$0 = 2);
  ("`Local hypotheses'" & ch: 0..3 & ctr: INTEGER & 0<=ctr & ctr<=2147483647 & not(ch = 0) & 1<=ctr & bb$0: 0..4 & not(bb$0 = 0) & not(bb$0 = 1) & not(bb$0 = 2) & not(bb$0 = 4) & bb$0 = 3);
  ("`Local hypotheses'" & ch: 0..3 & ctr: INTEGER & 0<=ctr & ctr<=2147483647 & not(ch = 0) & 1<=ctr & bb$0: 0..4 & not(bb$0 = 4) & not(bb$0 = 3) & not(bb$0 = 2) & not(bb$0 = 1) & bb$0 = 0);
  (ctr-1+1<=ctr);
  (bb$0: 0..3);
  (0<=ctr-1);
  ("`Local hypotheses'" & ch: 0..3 & ctr: INTEGER & 0<=ctr & ctr<=2147483647 & not(ch = 0) & 1<=ctr & bb$0: 0..4 & not(bb$0 = 0) & not(bb$0 = 1) & not(bb$0 = 2) & not(bb$0 = 3) & bb$1: 0..10 & bb$0 = 4);
  ("`Local hypotheses'" & ch: 0..3 & ctr: INTEGER & 0<=ctr & ctr<=2147483647 & not(ch = 0) & 1<=ctr & bb$0: 0..4 & not(bb$0 = 0) & not(bb$0 = 1) & not(bb$0 = 2) & not(bb$0 = 3) & not(bb$0 = 4))
END
&
THEORY EnumerateX 
END
&
THEORY Version IS
  POVersion(V3.6.8)(CLT == "V3.7.2")(local_op == OK)
END