//test curent rules
//max rule id:30

#include "int_array_def.h"

#include "verification_list.h"
#include "verification_stdlib.h"

id : 1
priority : core(1)
left : store_uint_array(?p, ?n, ?l) at 0
right : data_at(?p + (?i * sizeof(U32)), U32, ?v) at 1
check : infer(0 <= i);
        infer(i < n);
action : right_erase(1);
         left_erase(0);
         left_add(store_uint_array_missing_i_rec(p, i, 0, n, l));
         right_add(v == l[i]);

id : 2
priority : post(1)
left : store_uint_array_missing_i_rec(?p, ?i, 0, ?n, ?l) at 0
       data_at(p + i * sizeof(U32), U32, l[i]) at 1
check : infer(0 <= i);
        infer(i < n);
action : left_erase(1);
         left_erase(0);
         left_add(store_uint_array(p, n, l));

id : 3
priority : post(3)
left : store_uint_array_missing_i_rec(?p, ?i, 0, ?n, ?l) at 0
       data_at(p + i * sizeof(U32), U32, ?v) at 1
check : infer(0 <= i);
        infer(i < n);
action : left_erase(1);
         left_erase(0);
         left_add(store_uint_array(p, n, replace_Znth{Z}(i, v, l)));

id : 4
priority : core(1)
left : store_uint_array(?p, ?n, ?l1) at 0
right : store_uint_array(p, n, ?l2) at 1
action : right_erase(1);
         left_erase(0);
         right_add(l1 == l2);

id : 5
priority : core(1)
left : store_uint_array_missing_i_rec(?p, ?i, ?v, ?n, ?l) at 0
right : store_uint_array_missing_i_rec(p, i, v, n, l) at 1
action : left_erase(0);
         right_erase(1); 


id : 6
priority : core(1)
left : store_uint_array_rec(?p, ?x, ?y, ?l1) at 0 
right : store_uint_array_rec(?p, ?x, ?y, ?l2) at 1
action : right_erase(1);
         left_erase(0);
         right_add(l1 == l2);


id : 7
priority : core(1)
left : store_uint_array_rec(?p, ?x, ?y, ?l) at 0
right : data_at(?p + (?i * sizeof(U32)), U32, ?v) at 1
check : infer(x <= i);
        infer(i < y);
action : right_erase(1);
         left_erase(0);
         left_add(store_uint_array_missing_i_rec(p, i, x, y, l));
         right_add(v == l[i - x]);

id : 8
priority : core(1)
left : store_uint_array_rec(?p, ?x, ?y, ?l1) at 0 
        store_uint_array_rec(?p, ?y, ?z, ?l2) at 1 
right : store_uint_array_rec(?p, ?x, ?z, ?l3) at 2 
check : infer(y <= z);
        infer(x <= y);
action : right_erase(2);
         left_erase(0);
         left_erase(1);
         right_add(l3 == app{Z}(l1, l2));

id : 9
priority : core(1)
left : store_uint_array_rec(?p, ?x, ?z, ?l3) at 2 
right : store_uint_array_rec(?p, ?x, ?y, ?l1) at 0 
        store_uint_array_rec(?p, ?y, ?z, ?l2) at 1 
check : infer(y <= z);
        infer(x <= y);
action : left_erase(2);
         right_erase(0);
         right_erase(1);
         right_add(l3 == app{Z}(l1, l2));
         right_add(Zlength{Z}(l1) == y - x);

id : 10
priority : core(1)
right : store_uint_array_rec(?p, ?x, ?x, ?l) at 0
action : right_erase(0);
         right_add(l == nil{Z});


id : 11
priority : post(1)
left : store_uint_array_missing_i_rec(?p, ?i, ?x, ?y, ?l) at 0
       data_at(p + ?i * sizeof(U32), U32, l[?i - ?x]) at 1
check : infer(x <= i);
        infer(i < y);
action : left_erase(1);
         left_erase(0);
         left_add(store_uint_array_rec(p, x, y, l));

id : 12
priority : post(4)
left : store_uint_array_missing_i_rec(?p, ?i, ?x, ?y, ?l) at 0
       data_at(p + ?i * sizeof(U32), U32, ?v) at 1
check : infer(x <= i);
        infer(i < y);
action : left_erase(1);
         left_erase(0);
         left_add(store_uint_array_rec(p, x, y, replace_Znth{Z}(i - x, v, l)));