proc main() {
    assert(y >= 1 & x >= 0 & x == x0);
    assert(y >= 1 & x >= 0 & x == x0 & x*y == x0*y); % Implied (eq_i and eq_e)
    s := x * y;
    assert(y >= 1 & x >= 0 & x == x0 & s == x0*y);   % Asn
    t := x;
    assert(y >= 1 & x >= 0 & t == x0 & s == x0*y);   % Asn
    while y > 1 do {
        assert(y >= 1 & x >= 0 & t == x0 & s == x0*y & y > 1);    % OuterInv & Guard
        assert(y-1 > 0 & x >= 0 & t == x0 & s == x0*(y-1+1));   % Implied (VC1)
        y := y - 1;
        assert(y > 0 & x >= 0 & t == x0 & s == x0*(y+1));   % Asn
        x := t;
        assert(y > 0 & x >= 0 & t == x0 & x == x0 & s == x0*(y+1));   % Asn
        assert(y > 0 & t == x0 & s == x0*y + x);            % Implied (VC2)
        while !(x == 0) do {
            assert(y > 0 & t == x0 & s == x0*y + x & !(x==0));        % InnerInv & Guard
            assert(y > 0 & s-1 == x0*y + x - 1);            % Implied (VC3)
            x := x - 1;
            assert(y > 0 & s-1 == x0*y + x);                % Asn
            s := s - 1;
            assert(y > 0 & t == x0 & s == x0*y + x);                  % InnerInv by Asn
        };
        assert(y > 0 & t == x0 & s == x0*y + x & x == 0);             % InnerInv
        assert(y >= 1 & x >= 0 & t == x0 & s == x0*y);      % OuterInv, Implied (VC4)
    };
    assert(y >= 1 & x >= 0 & t == x0 & s == x0*y & !(y>1)); % While
    assert(s == x0);    % Implied (VC5)
}