Theory Tuple17

theory Tuple17
  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, 'q) tuple17 = Tuple17
  (Tuple17_get_a: 'a)
  (Tuple17_get_b: 'b)
  (Tuple17_get_c: 'c)
  (Tuple17_get_d: 'd)
  (Tuple17_get_e: 'e)
  (Tuple17_get_f: 'f)
  (Tuple17_get_g: 'g)
  (Tuple17_get_h: 'h)
  (Tuple17_get_i: 'i)
  (Tuple17_get_j: 'j)
  (Tuple17_get_k: 'k)
  (Tuple17_get_l: 'l)
  (Tuple17_get_m: 'm)
  (Tuple17_get_n: 'n)
  (Tuple17_get_o: 'o)
  (Tuple17_get_p: 'p)
  (Tuple17_get_q: 'q)

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, 'q) tuple17 ⇒ _› where
  ‹set_a M (Tuple17 _ N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts arena occs) = (Tuple17 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts arena occs)›

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

named_theorems tuple17_state_simp
lemma [tuple17_state_simp]:
  ‹Tuple17_get_a (Tuple17.set_a M S) = M›
  ‹Tuple17_get_b (Tuple17.set_a M S) = Tuple17_get_b S›
  ‹Tuple17_get_c(Tuple17.set_a M S) = Tuple17_get_c S›
  ‹Tuple17_get_d (Tuple17.set_a M S) = Tuple17_get_d S›
  ‹Tuple17_get_e (Tuple17.set_a M S) = Tuple17_get_e S›
  ‹Tuple17_get_f (Tuple17.set_a M S) = Tuple17_get_f S›
  ‹Tuple17_get_g (Tuple17.set_a M S) = Tuple17_get_g S›
  ‹Tuple17_get_h (Tuple17.set_a M S) = Tuple17_get_h S›
  ‹Tuple17_get_i (Tuple17.set_a M S) = Tuple17_get_i S›
  ‹Tuple17_get_j (Tuple17.set_a M S) = Tuple17_get_j S›
  ‹Tuple17_get_k (Tuple17.set_a M S) = Tuple17_get_k S›
  ‹Tuple17_get_l (Tuple17.set_a M S) = Tuple17_get_l S›
  ‹Tuple17_get_m (Tuple17.set_a M S) = Tuple17_get_m S›
  ‹Tuple17_get_n (Tuple17.set_a M S) = Tuple17_get_n S›
  ‹Tuple17_get_o (Tuple17.set_a M S) = Tuple17_get_o S›
  ‹Tuple17_get_p (Tuple17.set_a M S) = Tuple17_get_p S›
  ‹Tuple17_get_q (Tuple17.set_a M S) = Tuple17_get_q S›
  by (solves ‹cases S; auto simp:›)+

lemma [tuple17_state_simp]:
  ‹Tuple17_get_a (Tuple17.set_b N S) = Tuple17_get_a S›
  ‹Tuple17_get_b (Tuple17.set_b N S) = N›
  ‹Tuple17_get_c(Tuple17.set_b N S) = Tuple17_get_c S›
  ‹Tuple17_get_d (Tuple17.set_b N S) = Tuple17_get_d S›
  ‹Tuple17_get_e (Tuple17.set_b N S) = Tuple17_get_e S›
  ‹Tuple17_get_f (Tuple17.set_b N S) = Tuple17_get_f S›
  ‹Tuple17_get_g (Tuple17.set_b N S) = Tuple17_get_g S›
  ‹Tuple17_get_h (Tuple17.set_b N S) = Tuple17_get_h S›
  ‹Tuple17_get_i (Tuple17.set_b N S) = Tuple17_get_i S›
  ‹Tuple17_get_j (Tuple17.set_b N S) = Tuple17_get_j S›
  ‹Tuple17_get_k (Tuple17.set_b N S) = Tuple17_get_k S›
  ‹Tuple17_get_l (Tuple17.set_b N S) = Tuple17_get_l S›
  ‹Tuple17_get_m (Tuple17.set_b N S) = Tuple17_get_m S›
  ‹Tuple17_get_n (Tuple17.set_b N S) = Tuple17_get_n S›
  ‹Tuple17_get_o (Tuple17.set_b N S) = Tuple17_get_o S›
  ‹Tuple17_get_p (Tuple17.set_b N S) = Tuple17_get_p S›
  ‹Tuple17_get_q (Tuple17.set_b N S) = Tuple17_get_q S›

  ‹Tuple17_get_a (Tuple17.set_c D S) = Tuple17_get_a S›
  ‹Tuple17_get_b (Tuple17.set_c D S) = Tuple17_get_b S›
  ‹Tuple17_get_c(Tuple17.set_c D S) = D›
  ‹Tuple17_get_d (Tuple17.set_c D S) = Tuple17_get_d S›
  ‹Tuple17_get_e (Tuple17.set_c D S) = Tuple17_get_e S›
  ‹Tuple17_get_f (Tuple17.set_c D S) = Tuple17_get_f S›
  ‹Tuple17_get_g (Tuple17.set_c D S) = Tuple17_get_g S›
  ‹Tuple17_get_h (Tuple17.set_c D S) = Tuple17_get_h S›
  ‹Tuple17_get_i (Tuple17.set_c D S) = Tuple17_get_i S›
  ‹Tuple17_get_j (Tuple17.set_c D S) = Tuple17_get_j S›
  ‹Tuple17_get_k (Tuple17.set_c D S) = Tuple17_get_k S›
  ‹Tuple17_get_l (Tuple17.set_c D S) = Tuple17_get_l S›
  ‹Tuple17_get_m (Tuple17.set_c D S) = Tuple17_get_m S›
  ‹Tuple17_get_n (Tuple17.set_c D S) = Tuple17_get_n S›
  ‹Tuple17_get_o (Tuple17.set_c D S) = Tuple17_get_o S›
  ‹Tuple17_get_p (Tuple17.set_c D S) = Tuple17_get_p S›
  ‹Tuple17_get_q (Tuple17.set_c D S) = Tuple17_get_q S›
  by (solves ‹cases S; auto simp:›)+

lemma [tuple17_state_simp]:
  ‹Tuple17_get_a (Tuple17.set_d j S) = Tuple17_get_a S›
  ‹Tuple17_get_b (Tuple17.set_d j S) = Tuple17_get_b S›
  ‹Tuple17_get_c(Tuple17.set_d j S) = Tuple17_get_c S›
  ‹Tuple17_get_d (Tuple17.set_d j S) = j›
  ‹Tuple17_get_e (Tuple17.set_d j S) = Tuple17_get_e S›
  ‹Tuple17_get_f (Tuple17.set_d j S) = Tuple17_get_f S›
  ‹Tuple17_get_g (Tuple17.set_d j S) = Tuple17_get_g S›
  ‹Tuple17_get_h (Tuple17.set_d j S) = Tuple17_get_h S›
  ‹Tuple17_get_i (Tuple17.set_d j S) = Tuple17_get_i S›
  ‹Tuple17_get_j (Tuple17.set_d j S) = Tuple17_get_j S›
  ‹Tuple17_get_k (Tuple17.set_d j S) = Tuple17_get_k S›
  ‹Tuple17_get_l (Tuple17.set_d j S) = Tuple17_get_l S›
  ‹Tuple17_get_m (Tuple17.set_d j S) = Tuple17_get_m S›
  ‹Tuple17_get_n (Tuple17.set_d j S) = Tuple17_get_n S›
  ‹Tuple17_get_o (Tuple17.set_d j S) = Tuple17_get_o S›
  ‹Tuple17_get_p (Tuple17.set_d j S) = Tuple17_get_p S›
  ‹Tuple17_get_q (Tuple17.set_d j S) = Tuple17_get_q S›
  by (solves ‹cases S; auto simp:›)+

lemma [tuple17_state_simp]:
  ‹Tuple17_get_a (Tuple17.set_e W S) = Tuple17_get_a S›
  ‹Tuple17_get_b (Tuple17.set_e W S) = Tuple17_get_b S›
  ‹Tuple17_get_c(Tuple17.set_e W S) = Tuple17_get_c S›
  ‹Tuple17_get_d (Tuple17.set_e W S) = Tuple17_get_d S›
  ‹Tuple17_get_e (Tuple17.set_e W S) = W›
  ‹Tuple17_get_f (Tuple17.set_e W S) = Tuple17_get_f S›
  ‹Tuple17_get_g (Tuple17.set_e W S) = Tuple17_get_g S›
  ‹Tuple17_get_h (Tuple17.set_e W S) = Tuple17_get_h S›
  ‹Tuple17_get_i (Tuple17.set_e W S) = Tuple17_get_i S›
  ‹Tuple17_get_j (Tuple17.set_e W S) = Tuple17_get_j S›
  ‹Tuple17_get_k (Tuple17.set_e W S) = Tuple17_get_k S›
  ‹Tuple17_get_l (Tuple17.set_e W S) = Tuple17_get_l S›
  ‹Tuple17_get_m (Tuple17.set_e W S) = Tuple17_get_m S›
  ‹Tuple17_get_n (Tuple17.set_e W S) = Tuple17_get_n S›
  ‹Tuple17_get_o (Tuple17.set_e W S) = Tuple17_get_o S›
  ‹Tuple17_get_p (Tuple17.set_e W S) = Tuple17_get_p S›
  ‹Tuple17_get_q (Tuple17.set_e W S) = Tuple17_get_q S›
  by (solves ‹cases S; auto simp:›)+

lemma [tuple17_state_simp]:
  ‹Tuple17_get_a (Tuple17.set_f vmtf' S) = Tuple17_get_a S›
  ‹Tuple17_get_b (Tuple17.set_f vmtf' S) = Tuple17_get_b S›
  ‹Tuple17_get_c(Tuple17.set_f vmtf' S) = Tuple17_get_c S›
  ‹Tuple17_get_d (Tuple17.set_f vmtf' S) = Tuple17_get_d S›
  ‹Tuple17_get_e (Tuple17.set_f vmtf' S) = Tuple17_get_e S›
  ‹Tuple17_get_f (Tuple17.set_f vmtf' S) = vmtf'›
  ‹Tuple17_get_g (Tuple17.set_f vmtf' S) = Tuple17_get_g S›
  ‹Tuple17_get_h (Tuple17.set_f vmtf' S) = Tuple17_get_h S›
  ‹Tuple17_get_i (Tuple17.set_f vmtf' S) = Tuple17_get_i S›
  ‹Tuple17_get_j (Tuple17.set_f vmtf' S) = Tuple17_get_j S›
  ‹Tuple17_get_k (Tuple17.set_f vmtf' S) = Tuple17_get_k S›
  ‹Tuple17_get_l (Tuple17.set_f vmtf' S) = Tuple17_get_l S›
  ‹Tuple17_get_m (Tuple17.set_f vmtf' S) = Tuple17_get_m S›
  ‹Tuple17_get_n (Tuple17.set_f vmtf' S) = Tuple17_get_n S›
  ‹Tuple17_get_o (Tuple17.set_f vmtf' S) = Tuple17_get_o S›
  ‹Tuple17_get_p (Tuple17.set_f vmtf' S) = Tuple17_get_p S›
  ‹Tuple17_get_q (Tuple17.set_f vmtf' S) = Tuple17_get_q S›
  by (solves ‹cases S; auto simp:›)+

lemma [tuple17_state_simp]:
  ‹Tuple17_get_a (Tuple17.set_g count' S) = Tuple17_get_a S›
  ‹Tuple17_get_b (Tuple17.set_g count' S) = Tuple17_get_b S›
  ‹Tuple17_get_c(Tuple17.set_g count' S) = Tuple17_get_c S›
  ‹Tuple17_get_d (Tuple17.set_g count' S) = Tuple17_get_d S›
  ‹Tuple17_get_e (Tuple17.set_g count' S) = Tuple17_get_e S›
  ‹Tuple17_get_f (Tuple17.set_g count' S) = Tuple17_get_f S›
  ‹Tuple17_get_g (Tuple17.set_g count' S) = count'›
  ‹Tuple17_get_h (Tuple17.set_g count' S) = Tuple17_get_h S›
  ‹Tuple17_get_i (Tuple17.set_g count' S) = Tuple17_get_i S›
  ‹Tuple17_get_j (Tuple17.set_g count' S) = Tuple17_get_j S›
  ‹Tuple17_get_k (Tuple17.set_g count' S) = Tuple17_get_k S›
  ‹Tuple17_get_l (Tuple17.set_g count' S) = Tuple17_get_l S›
  ‹Tuple17_get_m (Tuple17.set_g count' S) = Tuple17_get_m S›
  ‹Tuple17_get_n (Tuple17.set_g count' S) = Tuple17_get_n S›
  ‹Tuple17_get_o (Tuple17.set_g count' S) = Tuple17_get_o S›
  ‹Tuple17_get_p (Tuple17.set_g count' S) = Tuple17_get_p S›
  ‹Tuple17_get_q (Tuple17.set_g count' S) = Tuple17_get_q S›
  by (solves ‹cases S; auto simp: ›)+

lemma [tuple17_state_simp]:
  ‹Tuple17_get_a (Tuple17.set_h ccach S) = Tuple17_get_a S›
  ‹Tuple17_get_b (Tuple17.set_h ccach S) = Tuple17_get_b S›
  ‹Tuple17_get_c(Tuple17.set_h ccach S) = Tuple17_get_c S›
  ‹Tuple17_get_d (Tuple17.set_h ccach S) = Tuple17_get_d S›
  ‹Tuple17_get_e (Tuple17.set_h ccach S) = Tuple17_get_e S›
  ‹Tuple17_get_f (Tuple17.set_h ccach S) = Tuple17_get_f S›
  ‹Tuple17_get_g (Tuple17.set_h ccach S) = Tuple17_get_g S›
  ‹Tuple17_get_h (Tuple17.set_h ccach S) = ccach›
  ‹Tuple17_get_i (Tuple17.set_h ccach S) = Tuple17_get_i S›
  ‹Tuple17_get_j (Tuple17.set_h ccach S) = Tuple17_get_j S›
  ‹Tuple17_get_k (Tuple17.set_h ccach S) = Tuple17_get_k S›
  ‹Tuple17_get_l (Tuple17.set_h ccach S) = Tuple17_get_l S›
  ‹Tuple17_get_m (Tuple17.set_h ccach S) = Tuple17_get_m S›
  ‹Tuple17_get_n (Tuple17.set_h ccach S) = Tuple17_get_n S›
  ‹Tuple17_get_o (Tuple17.set_h ccach S) = Tuple17_get_o S›
  ‹Tuple17_get_p (Tuple17.set_h ccach S) = Tuple17_get_p S›
  ‹Tuple17_get_q (Tuple17.set_h ccach S) = Tuple17_get_q S›
  by (solves ‹cases S; auto simp:›)+

lemma [tuple17_state_simp]:
  ‹Tuple17_get_a (Tuple17.set_i lbd S) = Tuple17_get_a S›
  ‹Tuple17_get_b (Tuple17.set_i lbd S) = Tuple17_get_b S›
  ‹Tuple17_get_c(Tuple17.set_i lbd S) = Tuple17_get_c S›
  ‹Tuple17_get_d (Tuple17.set_i lbd S) = Tuple17_get_d S›
  ‹Tuple17_get_e (Tuple17.set_i lbd S) = Tuple17_get_e S›
  ‹Tuple17_get_f (Tuple17.set_i lbd S) = Tuple17_get_f S›
  ‹Tuple17_get_g (Tuple17.set_i lbd S) = Tuple17_get_g S›
  ‹Tuple17_get_h (Tuple17.set_i lbd S) = Tuple17_get_h S›
  ‹Tuple17_get_i (Tuple17.set_i lbd S) = lbd›
  ‹Tuple17_get_j (Tuple17.set_i lbd S) = Tuple17_get_j S›
  ‹Tuple17_get_k (Tuple17.set_i lbd S) = Tuple17_get_k S›
  ‹Tuple17_get_l (Tuple17.set_i lbd S) = Tuple17_get_l S›
  ‹Tuple17_get_m (Tuple17.set_i lbd S) = Tuple17_get_m S›
  ‹Tuple17_get_n (Tuple17.set_i lbd S) = Tuple17_get_n S›
  ‹Tuple17_get_o (Tuple17.set_i lbd S) = Tuple17_get_o S›
  ‹Tuple17_get_p (Tuple17.set_i lbd S) = Tuple17_get_p S›
  ‹Tuple17_get_q (Tuple17.set_i lbd S) = Tuple17_get_q S›
  by (solves ‹cases S; auto simp:›)+

lemma [tuple17_state_simp]:
  ‹Tuple17_get_a (Tuple17.set_j outl S) = Tuple17_get_a S›
  ‹Tuple17_get_b (Tuple17.set_j outl S) = Tuple17_get_b S›
  ‹Tuple17_get_c(Tuple17.set_j outl S) = Tuple17_get_c S›
  ‹Tuple17_get_d (Tuple17.set_j outl S) = Tuple17_get_d S›
  ‹Tuple17_get_e (Tuple17.set_j outl S) = Tuple17_get_e S›
  ‹Tuple17_get_f (Tuple17.set_j outl S) = Tuple17_get_f S›
  ‹Tuple17_get_g (Tuple17.set_j outl S) = Tuple17_get_g S›
  ‹Tuple17_get_h (Tuple17.set_j outl S) = Tuple17_get_h S›
  ‹Tuple17_get_i (Tuple17.set_j outl S) = Tuple17_get_i S›
  ‹Tuple17_get_j (Tuple17.set_j outl S) = outl›
  ‹Tuple17_get_k (Tuple17.set_j outl S) = Tuple17_get_k S›
  ‹Tuple17_get_l (Tuple17.set_j outl S) = Tuple17_get_l S›
  ‹Tuple17_get_m (Tuple17.set_j outl S) = Tuple17_get_m S›
  ‹Tuple17_get_n (Tuple17.set_j outl S) = Tuple17_get_n S›
  ‹Tuple17_get_o (Tuple17.set_j outl S) = Tuple17_get_o S›
  ‹Tuple17_get_p (Tuple17.set_j outl S) = Tuple17_get_p S›
  ‹Tuple17_get_q (Tuple17.set_j outl S) = Tuple17_get_q S›
  by (solves ‹cases S; auto simp:›)+

lemma [tuple17_state_simp]:
  ‹Tuple17_get_a (Tuple17.set_k stats S) = Tuple17_get_a S›
  ‹Tuple17_get_b (Tuple17.set_k stats S) = Tuple17_get_b S›
  ‹Tuple17_get_c(Tuple17.set_k stats S) = Tuple17_get_c S›
  ‹Tuple17_get_d (Tuple17.set_k stats S) = Tuple17_get_d S›
  ‹Tuple17_get_e (Tuple17.set_k stats S) = Tuple17_get_e S›
  ‹Tuple17_get_f (Tuple17.set_k stats S) = Tuple17_get_f S›
  ‹Tuple17_get_g (Tuple17.set_k stats S) = Tuple17_get_g S›
  ‹Tuple17_get_h (Tuple17.set_k stats S) = Tuple17_get_h S›
  ‹Tuple17_get_i (Tuple17.set_k stats S) = Tuple17_get_i S›
  ‹Tuple17_get_j (Tuple17.set_k stats S) = Tuple17_get_j S›
  ‹Tuple17_get_k (Tuple17.set_k stats S) = stats›
  ‹Tuple17_get_l (Tuple17.set_k stats S) = Tuple17_get_l S›
  ‹Tuple17_get_m (Tuple17.set_k stats S) = Tuple17_get_m S›
  ‹Tuple17_get_n (Tuple17.set_k stats S) = Tuple17_get_n S›
  ‹Tuple17_get_o (Tuple17.set_k stats S) = Tuple17_get_o S›
  ‹Tuple17_get_p (Tuple17.set_k stats S) = Tuple17_get_p S›
  ‹Tuple17_get_q (Tuple17.set_k stats S) = Tuple17_get_q S›
  by (solves ‹cases S; auto simp:›)+

lemma [tuple17_state_simp]:
  ‹Tuple17_get_a (Tuple17.set_l heur S) = Tuple17_get_a S›
  ‹Tuple17_get_b (Tuple17.set_l heur S) = Tuple17_get_b S›
  ‹Tuple17_get_c(Tuple17.set_l heur S) = Tuple17_get_c S›
  ‹Tuple17_get_d (Tuple17.set_l heur S) = Tuple17_get_d S›
  ‹Tuple17_get_e (Tuple17.set_l heur S) = Tuple17_get_e S›
  ‹Tuple17_get_f (Tuple17.set_l heur S) = Tuple17_get_f S›
  ‹Tuple17_get_g (Tuple17.set_l heur S) = Tuple17_get_g S›
  ‹Tuple17_get_h (Tuple17.set_l heur S) = Tuple17_get_h S›
  ‹Tuple17_get_i (Tuple17.set_l heur S) = Tuple17_get_i S›
  ‹Tuple17_get_j (Tuple17.set_l heur S) = Tuple17_get_j S›
  ‹Tuple17_get_k (Tuple17.set_l heur S) = Tuple17_get_k S›
  ‹Tuple17_get_l (Tuple17.set_l heur S) = heur›
  ‹Tuple17_get_m (Tuple17.set_l heur S) = Tuple17_get_m S›
  ‹Tuple17_get_n (Tuple17.set_l heur S) = Tuple17_get_n S›
  ‹Tuple17_get_o (Tuple17.set_l heur S) = Tuple17_get_o S›
  ‹Tuple17_get_p (Tuple17.set_l heur S) = Tuple17_get_p S›
  ‹Tuple17_get_q (Tuple17.set_l heur S) = Tuple17_get_q S›
  by (solves ‹cases S; auto simp:›)+

lemma [tuple17_state_simp]:
  ‹Tuple17_get_a (Tuple17.set_m aivdom S) = Tuple17_get_a S›
  ‹Tuple17_get_b (Tuple17.set_m aivdom S) = Tuple17_get_b S›
  ‹Tuple17_get_c(Tuple17.set_m aivdom S) = Tuple17_get_c S›
  ‹Tuple17_get_d (Tuple17.set_m aivdom S) = Tuple17_get_d S›
  ‹Tuple17_get_e (Tuple17.set_m aivdom S) = Tuple17_get_e S›
  ‹Tuple17_get_f (Tuple17.set_m aivdom S) = Tuple17_get_f S›
  ‹Tuple17_get_g (Tuple17.set_m aivdom S) = Tuple17_get_g S›
  ‹Tuple17_get_h (Tuple17.set_m aivdom S) = Tuple17_get_h S›
  ‹Tuple17_get_i (Tuple17.set_m aivdom S) = Tuple17_get_i S›
  ‹Tuple17_get_j (Tuple17.set_m aivdom S) = Tuple17_get_j S›
  ‹Tuple17_get_k (Tuple17.set_m aivdom S) = Tuple17_get_k S›
  ‹Tuple17_get_l (Tuple17.set_m aivdom S) = Tuple17_get_l S›
  ‹Tuple17_get_m (Tuple17.set_m aivdom S) = aivdom›
  ‹Tuple17_get_n (Tuple17.set_m aivdom S) = Tuple17_get_n S›
  ‹Tuple17_get_o (Tuple17.set_m aivdom S) = Tuple17_get_o S›
  ‹Tuple17_get_p (Tuple17.set_m aivdom S) = Tuple17_get_p S›
  ‹Tuple17_get_q (Tuple17.set_m aivdom S) = Tuple17_get_q S›
  by (solves ‹cases S; auto simp:›)+

lemma [tuple17_state_simp]:
  ‹Tuple17_get_a (Tuple17.set_n lcount S) = Tuple17_get_a S›
  ‹Tuple17_get_b (Tuple17.set_n lcount S) = Tuple17_get_b S›
  ‹Tuple17_get_c(Tuple17.set_n lcount S) = Tuple17_get_c S›
  ‹Tuple17_get_d (Tuple17.set_n lcount S) = Tuple17_get_d S›
  ‹Tuple17_get_e (Tuple17.set_n lcount S) = Tuple17_get_e S›
  ‹Tuple17_get_f (Tuple17.set_n lcount S) = Tuple17_get_f S›
  ‹Tuple17_get_g (Tuple17.set_n lcount S) = Tuple17_get_g S›
  ‹Tuple17_get_h (Tuple17.set_n lcount S) = Tuple17_get_h S›
  ‹Tuple17_get_i (Tuple17.set_n lcount S) = Tuple17_get_i S›
  ‹Tuple17_get_j (Tuple17.set_n lcount S) = Tuple17_get_j S›
  ‹Tuple17_get_k (Tuple17.set_n lcount S) = Tuple17_get_k S›
  ‹Tuple17_get_l (Tuple17.set_n lcount S) = Tuple17_get_l S›
  ‹Tuple17_get_m (Tuple17.set_n lcount S) = Tuple17_get_m S›
  ‹Tuple17_get_o (Tuple17.set_n lcount S) = Tuple17_get_o S›
  ‹Tuple17_get_p (Tuple17.set_n lcount S) = Tuple17_get_p S›
  ‹Tuple17_get_q (Tuple17.set_n lcount S) = Tuple17_get_q S›
  by (solves ‹cases S; auto simp:›)+

lemma [tuple17_state_simp]:
  ‹Tuple17_get_a (set_o lcount S) = Tuple17_get_a S›
  ‹Tuple17_get_b (set_o lcount S) = Tuple17_get_b S›
  ‹Tuple17_get_c(set_o lcount S) = Tuple17_get_c S›
  ‹Tuple17_get_d (set_o lcount S) = Tuple17_get_d S›
  ‹Tuple17_get_e (set_o lcount S) = Tuple17_get_e S›
  ‹Tuple17_get_f (set_o lcount S) = Tuple17_get_f S›
  ‹Tuple17_get_g (set_o lcount S) = Tuple17_get_g S›
  ‹Tuple17_get_h (set_o lcount S) = Tuple17_get_h S›
  ‹Tuple17_get_i (set_o lcount S) = Tuple17_get_i S›
  ‹Tuple17_get_j (set_o lcount S) = Tuple17_get_j S›
  ‹Tuple17_get_k (set_o lcount S) = Tuple17_get_k S›
  ‹Tuple17_get_l (set_o lcount S) = Tuple17_get_l S›
  ‹Tuple17_get_m (set_o lcount S) = Tuple17_get_m S›
  ‹Tuple17_get_n (set_o lcount S) = Tuple17_get_n S›
  ‹Tuple17_get_o (set_o lcount S) = lcount›
  ‹Tuple17_get_p (set_o lcount S) = Tuple17_get_p S›
  ‹Tuple17_get_q (Tuple17.set_o lcount S) = Tuple17_get_q S›
  by (solves ‹cases S; auto simp:›)+

lemma [tuple17_state_simp]:
  ‹Tuple17_get_a (set_p old_arena S) = Tuple17_get_a S›
  ‹Tuple17_get_b (set_p old_arena S) = Tuple17_get_b S›
  ‹Tuple17_get_c(set_p old_arena S) = Tuple17_get_c S›
  ‹Tuple17_get_d (set_p old_arena S) = Tuple17_get_d S›
  ‹Tuple17_get_e (set_p old_arena S) = Tuple17_get_e S›
  ‹Tuple17_get_f (set_p old_arena S) = Tuple17_get_f S›
  ‹Tuple17_get_g (set_p old_arena S) = Tuple17_get_g S›
  ‹Tuple17_get_h (set_p old_arena S) = Tuple17_get_h S›
  ‹Tuple17_get_i (set_p old_arena S) = Tuple17_get_i S›
  ‹Tuple17_get_j (set_p old_arena S) = Tuple17_get_j S›
  ‹Tuple17_get_k (set_p old_arena S) = Tuple17_get_k S›
  ‹Tuple17_get_l (set_p old_arena S) = Tuple17_get_l S›
  ‹Tuple17_get_m (set_p old_arena S) = Tuple17_get_m S›
  ‹Tuple17_get_n (set_p old_arena S) = Tuple17_get_n S›
  ‹Tuple17_get_o (set_p old_arena S) = Tuple17_get_o S›
  ‹Tuple17_get_p (set_p old_arena S) = old_arena›
  ‹Tuple17_get_q (Tuple17.set_p old_arena S) = Tuple17_get_q S›
  by (solves ‹cases S; auto simp:›)+

lemma [tuple17_state_simp]:
  ‹Tuple17_get_a (set_q old_arena S) = Tuple17_get_a S›
  ‹Tuple17_get_b (set_q old_arena S) = Tuple17_get_b S›
  ‹Tuple17_get_c(set_q old_arena S) = Tuple17_get_c S›
  ‹Tuple17_get_d (set_q old_arena S) = Tuple17_get_d S›
  ‹Tuple17_get_e (set_q old_arena S) = Tuple17_get_e S›
  ‹Tuple17_get_f (set_q old_arena S) = Tuple17_get_f S›
  ‹Tuple17_get_g (set_q old_arena S) = Tuple17_get_g S›
  ‹Tuple17_get_h (set_q old_arena S) = Tuple17_get_h S›
  ‹Tuple17_get_i (set_q old_arena S) = Tuple17_get_i S›
  ‹Tuple17_get_j (set_q old_arena S) = Tuple17_get_j S›
  ‹Tuple17_get_k (set_q old_arena S) = Tuple17_get_k S›
  ‹Tuple17_get_l (set_q old_arena S) = Tuple17_get_l S›
  ‹Tuple17_get_m (set_q old_arena S) = Tuple17_get_m S›
  ‹Tuple17_get_n (set_q old_arena S) = Tuple17_get_n S›
  ‹Tuple17_get_o (set_q old_arena S) = Tuple17_get_o S›
  ‹Tuple17_get_p (Tuple17.set_q old_arena S) = Tuple17_get_p S›
  ‹Tuple17_get_q (set_q old_arena S) = old_arena›
  by (solves ‹cases S; auto simp:›)+

lemmas [simp] = tuple17_state_simp

named_theorems tuple17_getters_setters ‹Definition of getters and setters›

end