Theory Tuple16

theory Tuple16
  imports More_Sepref.WB_More_Refinement IsaSAT_Literals
begin


datatype ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o, 'p) tuple16 = Tuple16
  (Tuple16_get_a: 'a)
  (Tuple16_get_b: 'b)
  (Tuple16_get_c: 'c)
  (Tuple16_get_d: 'd)
  (Tuple16_get_e: 'e)
  (Tuple16_get_f: 'f)
  (Tuple16_get_g: 'g)
  (Tuple16_get_h: 'h)
  (Tuple16_get_i: 'i)
  (Tuple16_get_j: 'j)
  (Tuple16_get_k: 'k)
  (Tuple16_get_l: 'l)
  (Tuple16_get_m: 'm)
  (Tuple16_get_n: 'n)
  (Tuple16_get_o: 'o)
  (Tuple16_get_p: 'p)

paragraph ‹Accessors›

context
begin
qualified fun set_a :: ‹'a ⇒ ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o, 'p) tuple16 ⇒ _› where
  ‹set_a M (Tuple16 _ N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts arena) = (Tuple16 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts arena)›

fun set_b :: ‹'b ⇒('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o, 'p) tuple16 ⇒ _› where
  ‹set_b N (Tuple16 M _ D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts arena) = (Tuple16 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts arena)›

fun set_c :: ‹'c ⇒('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o, 'p) tuple16 ⇒ _› where
  ‹set_c D (Tuple16 M N _ i W ivmtf icount ccach lbd outl heur stats aivdom clss opts arena) = (Tuple16 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts arena)›

fun set_d :: ‹'d ⇒('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o, 'p) tuple16 ⇒ _› where
  ‹set_d i (Tuple16 M N D _ W ivmtf icount ccach lbd outl heur stats aivdom clss opts arena) = (Tuple16 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts arena)›

fun set_e :: ‹'e ⇒('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o, 'p) tuple16 ⇒ _› where
  ‹set_e W (Tuple16 M N D i _ ivmtf icount ccach lbd outl heur stats aivdom clss opts arena) = (Tuple16 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts arena)›

fun set_f :: ‹'f ⇒('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o, 'p) tuple16 ⇒ _› where
  ‹set_f ivmtf (Tuple16 M N D i W _ icount ccach lbd outl heur stats aivdom clss opts arena) = (Tuple16 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts arena)›

fun set_g :: ‹'g ⇒('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o, 'p) tuple16 ⇒ _› where
  ‹set_g icount (Tuple16 M N D i W ivmtf _ ccach lbd outl heur stats aivdom clss opts arena) = (Tuple16 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts arena)›

fun set_h :: ‹'h ⇒('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o, 'p) tuple16 ⇒ _› where
  ‹set_h ccach (Tuple16 M N D i W ivmtf icount _ lbd outl heur stats aivdom clss opts arena) = (Tuple16 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts arena)›

fun set_i :: ‹'i ⇒('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o, 'p) tuple16 ⇒ _› where
  ‹set_i lbd (Tuple16 M N D i W ivmtf icount ccach _ outl heur stats aivdom clss opts arena) = (Tuple16 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts arena)›

fun set_j :: ‹'j ⇒('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o, 'p) tuple16 ⇒ _› where
  ‹set_j outl (Tuple16 M N D i W ivmtf icount ccach lbd _ heur stats aivdom clss opts arena) = (Tuple16 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts arena)›

fun set_k :: ‹'k ⇒('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o, 'p) tuple16 ⇒ _› where
  ‹set_k stats (Tuple16 M N D i W ivmtf icount ccach lbd outl _ heur aivdom clss opts arena) = (Tuple16 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts arena)›

fun set_l :: ‹'l ⇒('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o, 'p) tuple16 ⇒ _› where
  ‹set_l heur (Tuple16 M N D i W ivmtf icount ccach lbd outl stats _ aivdom clss opts arena) = (Tuple16 M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts arena)›

fun set_m :: ‹'m ⇒('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o, 'p) tuple16 ⇒ _› where
  ‹set_m aivdom (Tuple16 M N D i W ivmtf icount ccach lbd outl heur stats _ clss opts arena) = (Tuple16 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts arena)›

fun set_n :: ‹'n ⇒('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o, 'p) tuple16 ⇒ _› where
  ‹set_n clss (Tuple16 M N D i W ivmtf icount ccach lbd outl heur stats aivdom _ opts arena) = (Tuple16 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts arena)›

fun set_o :: ‹'o ⇒('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o, 'p) tuple16 ⇒ _› where
  ‹set_o opts (Tuple16 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss _ arena) = (Tuple16 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts arena)›

fun set_p :: ‹'p ⇒('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o, 'p) tuple16 ⇒ _› where
  ‹set_p arena (Tuple16 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts _) = (Tuple16 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts arena)›

end

named_theorems tuple16_state_simp
lemma [tuple16_state_simp]:
  ‹Tuple16_get_a (Tuple16.set_a M S) = M›
  ‹Tuple16_get_b (Tuple16.set_a M S) = Tuple16_get_b S›
  ‹Tuple16_get_c(Tuple16.set_a M S) = Tuple16_get_c S›
  ‹Tuple16_get_d (Tuple16.set_a M S) = Tuple16_get_d S›
  ‹Tuple16_get_e (Tuple16.set_a M S) = Tuple16_get_e S›
  ‹Tuple16_get_f (Tuple16.set_a M S) = Tuple16_get_f S›
  ‹Tuple16_get_g (Tuple16.set_a M S) = Tuple16_get_g S›
  ‹Tuple16_get_h (Tuple16.set_a M S) = Tuple16_get_h S›
  ‹Tuple16_get_i (Tuple16.set_a M S) = Tuple16_get_i S›
  ‹Tuple16_get_j (Tuple16.set_a M S) = Tuple16_get_j S›
  ‹Tuple16_get_k (Tuple16.set_a M S) = Tuple16_get_k S›
  ‹Tuple16_get_l (Tuple16.set_a M S) = Tuple16_get_l S›
  ‹Tuple16_get_m (Tuple16.set_a M S) = Tuple16_get_m S›
  ‹Tuple16_get_n (Tuple16.set_a M S) = Tuple16_get_n S›
  ‹Tuple16_get_o (Tuple16.set_a M S) = Tuple16_get_o S›
  ‹Tuple16_get_p (Tuple16.set_a M S) = Tuple16_get_p S›
  by (solves ‹cases S; auto simp:›)+

lemma [tuple16_state_simp]:
  ‹Tuple16_get_a (Tuple16.set_b N S) = Tuple16_get_a S›
  ‹Tuple16_get_b (Tuple16.set_b N S) = N›
  ‹Tuple16_get_c(Tuple16.set_b N S) = Tuple16_get_c S›
  ‹Tuple16_get_d (Tuple16.set_b N S) = Tuple16_get_d S›
  ‹Tuple16_get_e (Tuple16.set_b N S) = Tuple16_get_e S›
  ‹Tuple16_get_f (Tuple16.set_b N S) = Tuple16_get_f S›
  ‹Tuple16_get_g (Tuple16.set_b N S) = Tuple16_get_g S›
  ‹Tuple16_get_h (Tuple16.set_b N S) = Tuple16_get_h S›
  ‹Tuple16_get_i (Tuple16.set_b N S) = Tuple16_get_i S›
  ‹Tuple16_get_j (Tuple16.set_b N S) = Tuple16_get_j S›
  ‹Tuple16_get_k (Tuple16.set_b N S) = Tuple16_get_k S›
  ‹Tuple16_get_l (Tuple16.set_b N S) = Tuple16_get_l S›
  ‹Tuple16_get_m (Tuple16.set_b N S) = Tuple16_get_m S›
  ‹Tuple16_get_n (Tuple16.set_b N S) = Tuple16_get_n S›
  ‹Tuple16_get_o (Tuple16.set_b N S) = Tuple16_get_o S›
  ‹Tuple16_get_p (Tuple16.set_b N S) = Tuple16_get_p S›

  ‹Tuple16_get_a (Tuple16.set_c D S) = Tuple16_get_a S›
  ‹Tuple16_get_b (Tuple16.set_c D S) = Tuple16_get_b S›
  ‹Tuple16_get_c(Tuple16.set_c D S) = D›
  ‹Tuple16_get_d (Tuple16.set_c D S) = Tuple16_get_d S›
  ‹Tuple16_get_e (Tuple16.set_c D S) = Tuple16_get_e S›
  ‹Tuple16_get_f (Tuple16.set_c D S) = Tuple16_get_f S›
  ‹Tuple16_get_g (Tuple16.set_c D S) = Tuple16_get_g S›
  ‹Tuple16_get_h (Tuple16.set_c D S) = Tuple16_get_h S›
  ‹Tuple16_get_i (Tuple16.set_c D S) = Tuple16_get_i S›
  ‹Tuple16_get_j (Tuple16.set_c D S) = Tuple16_get_j S›
  ‹Tuple16_get_k (Tuple16.set_c D S) = Tuple16_get_k S›
  ‹Tuple16_get_l (Tuple16.set_c D S) = Tuple16_get_l S›
  ‹Tuple16_get_m (Tuple16.set_c D S) = Tuple16_get_m S›
  ‹Tuple16_get_n (Tuple16.set_c D S) = Tuple16_get_n S›
  ‹Tuple16_get_o (Tuple16.set_c D S) = Tuple16_get_o S›
  ‹Tuple16_get_p (Tuple16.set_c D S) = Tuple16_get_p S›
  by (solves ‹cases S; auto simp:›)+

lemma [tuple16_state_simp]:
  ‹Tuple16_get_a (Tuple16.set_d j S) = Tuple16_get_a S›
  ‹Tuple16_get_b (Tuple16.set_d j S) = Tuple16_get_b S›
  ‹Tuple16_get_c(Tuple16.set_d j S) = Tuple16_get_c S›
  ‹Tuple16_get_d (Tuple16.set_d j S) = j›
  ‹Tuple16_get_e (Tuple16.set_d j S) = Tuple16_get_e S›
  ‹Tuple16_get_f (Tuple16.set_d j S) = Tuple16_get_f S›
  ‹Tuple16_get_g (Tuple16.set_d j S) = Tuple16_get_g S›
  ‹Tuple16_get_h (Tuple16.set_d j S) = Tuple16_get_h S›
  ‹Tuple16_get_i (Tuple16.set_d j S) = Tuple16_get_i S›
  ‹Tuple16_get_j (Tuple16.set_d j S) = Tuple16_get_j S›
  ‹Tuple16_get_k (Tuple16.set_d j S) = Tuple16_get_k S›
  ‹Tuple16_get_l (Tuple16.set_d j S) = Tuple16_get_l S›
  ‹Tuple16_get_m (Tuple16.set_d j S) = Tuple16_get_m S›
  ‹Tuple16_get_n (Tuple16.set_d j S) = Tuple16_get_n S›
  ‹Tuple16_get_o (Tuple16.set_d j S) = Tuple16_get_o S›
  ‹Tuple16_get_p (Tuple16.set_d j S) = Tuple16_get_p S›
  by (solves ‹cases S; auto simp:›)+

lemma [tuple16_state_simp]:
  ‹Tuple16_get_a (Tuple16.set_e W S) = Tuple16_get_a S›
  ‹Tuple16_get_b (Tuple16.set_e W S) = Tuple16_get_b S›
  ‹Tuple16_get_c(Tuple16.set_e W S) = Tuple16_get_c S›
  ‹Tuple16_get_d (Tuple16.set_e W S) = Tuple16_get_d S›
  ‹Tuple16_get_e (Tuple16.set_e W S) = W›
  ‹Tuple16_get_f (Tuple16.set_e W S) = Tuple16_get_f S›
  ‹Tuple16_get_g (Tuple16.set_e W S) = Tuple16_get_g S›
  ‹Tuple16_get_h (Tuple16.set_e W S) = Tuple16_get_h S›
  ‹Tuple16_get_i (Tuple16.set_e W S) = Tuple16_get_i S›
  ‹Tuple16_get_j (Tuple16.set_e W S) = Tuple16_get_j S›
  ‹Tuple16_get_k (Tuple16.set_e W S) = Tuple16_get_k S›
  ‹Tuple16_get_l (Tuple16.set_e W S) = Tuple16_get_l S›
  ‹Tuple16_get_m (Tuple16.set_e W S) = Tuple16_get_m S›
  ‹Tuple16_get_n (Tuple16.set_e W S) = Tuple16_get_n S›
  ‹Tuple16_get_o (Tuple16.set_e W S) = Tuple16_get_o S›
  ‹Tuple16_get_p (Tuple16.set_e W S) = Tuple16_get_p S›
  by (solves ‹cases S; auto simp:›)+

lemma [tuple16_state_simp]:
  ‹Tuple16_get_a (Tuple16.set_f vmtf' S) = Tuple16_get_a S›
  ‹Tuple16_get_b (Tuple16.set_f vmtf' S) = Tuple16_get_b S›
  ‹Tuple16_get_c(Tuple16.set_f vmtf' S) = Tuple16_get_c S›
  ‹Tuple16_get_d (Tuple16.set_f vmtf' S) = Tuple16_get_d S›
  ‹Tuple16_get_e (Tuple16.set_f vmtf' S) = Tuple16_get_e S›
  ‹Tuple16_get_f (Tuple16.set_f vmtf' S) = vmtf'›
  ‹Tuple16_get_g (Tuple16.set_f vmtf' S) = Tuple16_get_g S›
  ‹Tuple16_get_h (Tuple16.set_f vmtf' S) = Tuple16_get_h S›
  ‹Tuple16_get_i (Tuple16.set_f vmtf' S) = Tuple16_get_i S›
  ‹Tuple16_get_j (Tuple16.set_f vmtf' S) = Tuple16_get_j S›
  ‹Tuple16_get_k (Tuple16.set_f vmtf' S) = Tuple16_get_k S›
  ‹Tuple16_get_l (Tuple16.set_f vmtf' S) = Tuple16_get_l S›
  ‹Tuple16_get_m (Tuple16.set_f vmtf' S) = Tuple16_get_m S›
  ‹Tuple16_get_n (Tuple16.set_f vmtf' S) = Tuple16_get_n S›
  ‹Tuple16_get_o (Tuple16.set_f vmtf' S) = Tuple16_get_o S›
  ‹Tuple16_get_p (Tuple16.set_f vmtf' S) = Tuple16_get_p S›
  by (solves ‹cases S; auto simp:›)+

lemma [tuple16_state_simp]:
  ‹Tuple16_get_a (Tuple16.set_g count' S) = Tuple16_get_a S›
  ‹Tuple16_get_b (Tuple16.set_g count' S) = Tuple16_get_b S›
  ‹Tuple16_get_c(Tuple16.set_g count' S) = Tuple16_get_c S›
  ‹Tuple16_get_d (Tuple16.set_g count' S) = Tuple16_get_d S›
  ‹Tuple16_get_e (Tuple16.set_g count' S) = Tuple16_get_e S›
  ‹Tuple16_get_f (Tuple16.set_g count' S) = Tuple16_get_f S›
  ‹Tuple16_get_g (Tuple16.set_g count' S) = count'›
  ‹Tuple16_get_h (Tuple16.set_g count' S) = Tuple16_get_h S›
  ‹Tuple16_get_i (Tuple16.set_g count' S) = Tuple16_get_i S›
  ‹Tuple16_get_j (Tuple16.set_g count' S) = Tuple16_get_j S›
  ‹Tuple16_get_k (Tuple16.set_g count' S) = Tuple16_get_k S›
  ‹Tuple16_get_l (Tuple16.set_g count' S) = Tuple16_get_l S›
  ‹Tuple16_get_m (Tuple16.set_g count' S) = Tuple16_get_m S›
  ‹Tuple16_get_n (Tuple16.set_g count' S) = Tuple16_get_n S›
  ‹Tuple16_get_o (Tuple16.set_g count' S) = Tuple16_get_o S›
  ‹Tuple16_get_p (Tuple16.set_g count' S) = Tuple16_get_p S›
  by (solves ‹cases S; auto simp: ›)+

lemma [tuple16_state_simp]:
  ‹Tuple16_get_a (Tuple16.set_h ccach S) = Tuple16_get_a S›
  ‹Tuple16_get_b (Tuple16.set_h ccach S) = Tuple16_get_b S›
  ‹Tuple16_get_c(Tuple16.set_h ccach S) = Tuple16_get_c S›
  ‹Tuple16_get_d (Tuple16.set_h ccach S) = Tuple16_get_d S›
  ‹Tuple16_get_e (Tuple16.set_h ccach S) = Tuple16_get_e S›
  ‹Tuple16_get_f (Tuple16.set_h ccach S) = Tuple16_get_f S›
  ‹Tuple16_get_g (Tuple16.set_h ccach S) = Tuple16_get_g S›
  ‹Tuple16_get_h (Tuple16.set_h ccach S) = ccach›
  ‹Tuple16_get_i (Tuple16.set_h ccach S) = Tuple16_get_i S›
  ‹Tuple16_get_j (Tuple16.set_h ccach S) = Tuple16_get_j S›
  ‹Tuple16_get_k (Tuple16.set_h ccach S) = Tuple16_get_k S›
  ‹Tuple16_get_l (Tuple16.set_h ccach S) = Tuple16_get_l S›
  ‹Tuple16_get_m (Tuple16.set_h ccach S) = Tuple16_get_m S›
  ‹Tuple16_get_n (Tuple16.set_h ccach S) = Tuple16_get_n S›
  ‹Tuple16_get_o (Tuple16.set_h ccach S) = Tuple16_get_o S›
  ‹Tuple16_get_p (Tuple16.set_h ccach S) = Tuple16_get_p S›
  by (solves ‹cases S; auto simp:›)+

lemma [tuple16_state_simp]:
  ‹Tuple16_get_a (Tuple16.set_i lbd S) = Tuple16_get_a S›
  ‹Tuple16_get_b (Tuple16.set_i lbd S) = Tuple16_get_b S›
  ‹Tuple16_get_c(Tuple16.set_i lbd S) = Tuple16_get_c S›
  ‹Tuple16_get_d (Tuple16.set_i lbd S) = Tuple16_get_d S›
  ‹Tuple16_get_e (Tuple16.set_i lbd S) = Tuple16_get_e S›
  ‹Tuple16_get_f (Tuple16.set_i lbd S) = Tuple16_get_f S›
  ‹Tuple16_get_g (Tuple16.set_i lbd S) = Tuple16_get_g S›
  ‹Tuple16_get_h (Tuple16.set_i lbd S) = Tuple16_get_h S›
  ‹Tuple16_get_i (Tuple16.set_i lbd S) = lbd›
  ‹Tuple16_get_j (Tuple16.set_i lbd S) = Tuple16_get_j S›
  ‹Tuple16_get_k (Tuple16.set_i lbd S) = Tuple16_get_k S›
  ‹Tuple16_get_l (Tuple16.set_i lbd S) = Tuple16_get_l S›
  ‹Tuple16_get_m (Tuple16.set_i lbd S) = Tuple16_get_m S›
  ‹Tuple16_get_n (Tuple16.set_i lbd S) = Tuple16_get_n S›
  ‹Tuple16_get_o (Tuple16.set_i lbd S) = Tuple16_get_o S›
  ‹Tuple16_get_p (Tuple16.set_i lbd S) = Tuple16_get_p S›
  by (solves ‹cases S; auto simp:›)+

lemma [tuple16_state_simp]:
  ‹Tuple16_get_a (Tuple16.set_j outl S) = Tuple16_get_a S›
  ‹Tuple16_get_b (Tuple16.set_j outl S) = Tuple16_get_b S›
  ‹Tuple16_get_c(Tuple16.set_j outl S) = Tuple16_get_c S›
  ‹Tuple16_get_d (Tuple16.set_j outl S) = Tuple16_get_d S›
  ‹Tuple16_get_e (Tuple16.set_j outl S) = Tuple16_get_e S›
  ‹Tuple16_get_f (Tuple16.set_j outl S) = Tuple16_get_f S›
  ‹Tuple16_get_g (Tuple16.set_j outl S) = Tuple16_get_g S›
  ‹Tuple16_get_h (Tuple16.set_j outl S) = Tuple16_get_h S›
  ‹Tuple16_get_i (Tuple16.set_j outl S) = Tuple16_get_i S›
  ‹Tuple16_get_j (Tuple16.set_j outl S) = outl›
  ‹Tuple16_get_k (Tuple16.set_j outl S) = Tuple16_get_k S›
  ‹Tuple16_get_l (Tuple16.set_j outl S) = Tuple16_get_l S›
  ‹Tuple16_get_m (Tuple16.set_j outl S) = Tuple16_get_m S›
  ‹Tuple16_get_n (Tuple16.set_j outl S) = Tuple16_get_n S›
  ‹Tuple16_get_o (Tuple16.set_j outl S) = Tuple16_get_o S›
  ‹Tuple16_get_p (Tuple16.set_j outl S) = Tuple16_get_p S›
  by (solves ‹cases S; auto simp:›)+

lemma [tuple16_state_simp]:
  ‹Tuple16_get_a (Tuple16.set_k stats S) = Tuple16_get_a S›
  ‹Tuple16_get_b (Tuple16.set_k stats S) = Tuple16_get_b S›
  ‹Tuple16_get_c(Tuple16.set_k stats S) = Tuple16_get_c S›
  ‹Tuple16_get_d (Tuple16.set_k stats S) = Tuple16_get_d S›
  ‹Tuple16_get_e (Tuple16.set_k stats S) = Tuple16_get_e S›
  ‹Tuple16_get_f (Tuple16.set_k stats S) = Tuple16_get_f S›
  ‹Tuple16_get_g (Tuple16.set_k stats S) = Tuple16_get_g S›
  ‹Tuple16_get_h (Tuple16.set_k stats S) = Tuple16_get_h S›
  ‹Tuple16_get_i (Tuple16.set_k stats S) = Tuple16_get_i S›
  ‹Tuple16_get_j (Tuple16.set_k stats S) = Tuple16_get_j S›
  ‹Tuple16_get_k (Tuple16.set_k stats S) = stats›
  ‹Tuple16_get_l (Tuple16.set_k stats S) = Tuple16_get_l S›
  ‹Tuple16_get_m (Tuple16.set_k stats S) = Tuple16_get_m S›
  ‹Tuple16_get_n (Tuple16.set_k stats S) = Tuple16_get_n S›
  ‹Tuple16_get_o (Tuple16.set_k stats S) = Tuple16_get_o S›
  ‹Tuple16_get_p (Tuple16.set_k stats S) = Tuple16_get_p S›
  by (solves ‹cases S; auto simp:›)+

lemma [tuple16_state_simp]:
  ‹Tuple16_get_a (Tuple16.set_l heur S) = Tuple16_get_a S›
  ‹Tuple16_get_b (Tuple16.set_l heur S) = Tuple16_get_b S›
  ‹Tuple16_get_c(Tuple16.set_l heur S) = Tuple16_get_c S›
  ‹Tuple16_get_d (Tuple16.set_l heur S) = Tuple16_get_d S›
  ‹Tuple16_get_e (Tuple16.set_l heur S) = Tuple16_get_e S›
  ‹Tuple16_get_f (Tuple16.set_l heur S) = Tuple16_get_f S›
  ‹Tuple16_get_g (Tuple16.set_l heur S) = Tuple16_get_g S›
  ‹Tuple16_get_h (Tuple16.set_l heur S) = Tuple16_get_h S›
  ‹Tuple16_get_i (Tuple16.set_l heur S) = Tuple16_get_i S›
  ‹Tuple16_get_j (Tuple16.set_l heur S) = Tuple16_get_j S›
  ‹Tuple16_get_k (Tuple16.set_l heur S) = Tuple16_get_k S›
  ‹Tuple16_get_l (Tuple16.set_l heur S) = heur›
  ‹Tuple16_get_m (Tuple16.set_l heur S) = Tuple16_get_m S›
  ‹Tuple16_get_n (Tuple16.set_l heur S) = Tuple16_get_n S›
  ‹Tuple16_get_o (Tuple16.set_l heur S) = Tuple16_get_o S›
  ‹Tuple16_get_p (Tuple16.set_l heur S) = Tuple16_get_p S›
  by (solves ‹cases S; auto simp:›)+

lemma [tuple16_state_simp]:
  ‹Tuple16_get_a (Tuple16.set_m aivdom S) = Tuple16_get_a S›
  ‹Tuple16_get_b (Tuple16.set_m aivdom S) = Tuple16_get_b S›
  ‹Tuple16_get_c(Tuple16.set_m aivdom S) = Tuple16_get_c S›
  ‹Tuple16_get_d (Tuple16.set_m aivdom S) = Tuple16_get_d S›
  ‹Tuple16_get_e (Tuple16.set_m aivdom S) = Tuple16_get_e S›
  ‹Tuple16_get_f (Tuple16.set_m aivdom S) = Tuple16_get_f S›
  ‹Tuple16_get_g (Tuple16.set_m aivdom S) = Tuple16_get_g S›
  ‹Tuple16_get_h (Tuple16.set_m aivdom S) = Tuple16_get_h S›
  ‹Tuple16_get_i (Tuple16.set_m aivdom S) = Tuple16_get_i S›
  ‹Tuple16_get_j (Tuple16.set_m aivdom S) = Tuple16_get_j S›
  ‹Tuple16_get_k (Tuple16.set_m aivdom S) = Tuple16_get_k S›
  ‹Tuple16_get_l (Tuple16.set_m aivdom S) = Tuple16_get_l S›
  ‹Tuple16_get_m (Tuple16.set_m aivdom S) = aivdom›
  ‹Tuple16_get_n (Tuple16.set_m aivdom S) = Tuple16_get_n S›
  ‹Tuple16_get_o (Tuple16.set_m aivdom S) = Tuple16_get_o S›
  ‹Tuple16_get_p (Tuple16.set_m aivdom S) = Tuple16_get_p S›
  by (solves ‹cases S; auto simp:›)+

lemma [tuple16_state_simp]:
  ‹Tuple16_get_a (Tuple16.set_n lcount S) = Tuple16_get_a S›
  ‹Tuple16_get_b (Tuple16.set_n lcount S) = Tuple16_get_b S›
  ‹Tuple16_get_c(Tuple16.set_n lcount S) = Tuple16_get_c S›
  ‹Tuple16_get_d (Tuple16.set_n lcount S) = Tuple16_get_d S›
  ‹Tuple16_get_e (Tuple16.set_n lcount S) = Tuple16_get_e S›
  ‹Tuple16_get_f (Tuple16.set_n lcount S) = Tuple16_get_f S›
  ‹Tuple16_get_g (Tuple16.set_n lcount S) = Tuple16_get_g S›
  ‹Tuple16_get_h (Tuple16.set_n lcount S) = Tuple16_get_h S›
  ‹Tuple16_get_i (Tuple16.set_n lcount S) = Tuple16_get_i S›
  ‹Tuple16_get_j (Tuple16.set_n lcount S) = Tuple16_get_j S›
  ‹Tuple16_get_k (Tuple16.set_n lcount S) = Tuple16_get_k S›
  ‹Tuple16_get_l (Tuple16.set_n lcount S) = Tuple16_get_l S›
  ‹Tuple16_get_m (Tuple16.set_n lcount S) = Tuple16_get_m S›
  ‹Tuple16_get_o (Tuple16.set_n lcount S) = Tuple16_get_o S›
  ‹Tuple16_get_p (Tuple16.set_n lcount S) = Tuple16_get_p S›
  by (solves ‹cases S; auto simp:›)+

lemma [tuple16_state_simp]:
  ‹Tuple16_get_a (set_o lcount S) = Tuple16_get_a S›
  ‹Tuple16_get_b (set_o lcount S) = Tuple16_get_b S›
  ‹Tuple16_get_c(set_o lcount S) = Tuple16_get_c S›
  ‹Tuple16_get_d (set_o lcount S) = Tuple16_get_d S›
  ‹Tuple16_get_e (set_o lcount S) = Tuple16_get_e S›
  ‹Tuple16_get_f (set_o lcount S) = Tuple16_get_f S›
  ‹Tuple16_get_g (set_o lcount S) = Tuple16_get_g S›
  ‹Tuple16_get_h (set_o lcount S) = Tuple16_get_h S›
  ‹Tuple16_get_i (set_o lcount S) = Tuple16_get_i S›
  ‹Tuple16_get_j (set_o lcount S) = Tuple16_get_j S›
  ‹Tuple16_get_k (set_o lcount S) = Tuple16_get_k S›
  ‹Tuple16_get_l (set_o lcount S) = Tuple16_get_l S›
  ‹Tuple16_get_m (set_o lcount S) = Tuple16_get_m S›
  ‹Tuple16_get_n (set_o lcount S) = Tuple16_get_n S›
  ‹Tuple16_get_o (set_o lcount S) = lcount›
  ‹Tuple16_get_p (set_o lcount S) = Tuple16_get_p S›
  by (solves ‹cases S; auto simp:›)+

lemma [tuple16_state_simp]:
  ‹Tuple16_get_a (set_p old_arena S) = Tuple16_get_a S›
  ‹Tuple16_get_b (set_p old_arena S) = Tuple16_get_b S›
  ‹Tuple16_get_c(set_p old_arena S) = Tuple16_get_c S›
  ‹Tuple16_get_d (set_p old_arena S) = Tuple16_get_d S›
  ‹Tuple16_get_e (set_p old_arena S) = Tuple16_get_e S›
  ‹Tuple16_get_f (set_p old_arena S) = Tuple16_get_f S›
  ‹Tuple16_get_g (set_p old_arena S) = Tuple16_get_g S›
  ‹Tuple16_get_h (set_p old_arena S) = Tuple16_get_h S›
  ‹Tuple16_get_i (set_p old_arena S) = Tuple16_get_i S›
  ‹Tuple16_get_j (set_p old_arena S) = Tuple16_get_j S›
  ‹Tuple16_get_k (set_p old_arena S) = Tuple16_get_k S›
  ‹Tuple16_get_l (set_p old_arena S) = Tuple16_get_l S›
  ‹Tuple16_get_m (set_p old_arena S) = Tuple16_get_m S›
  ‹Tuple16_get_n (set_p old_arena S) = Tuple16_get_n S›
  ‹Tuple16_get_o (set_p old_arena S) = Tuple16_get_o S›
  ‹Tuple16_get_p (set_p old_arena S) = old_arena›
  by (solves ‹cases S; auto simp:›)+

lemmas [simp] = tuple16_state_simp

named_theorems tuple16_getters_setters ‹Definition of getters and setters›

end