Theory Test_Iterings

(* Title:      Test Iterings
   Author:     Walter Guttmann
   Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

section ‹Test Iterings›

theory Test_Iterings

imports Stone_Kleene_Relation_Algebras.Iterings Tests

begin

class test_itering = itering + tests + while +
  assumes while_def: "p ⋆ y = (p * y)⇧∘ * -p"
begin

lemma wnf_lemma_5:
  "(-p ⊔ -q) * (-q * x ⊔ --q * y) = -q * x ⊔ --q * -p * y"
  by (smt (z3) mult_left_dist_sup sup_commute tests_dual.sba_dual.sub_sup_closed tests_dual.sba_dual.sup_complement_intro tests_dual.sba_dual.sup_idempotent tests_dual.sup_idempotent mult_assoc tests_dual.wnf_lemma_3)

lemma test_case_split_left_equal:
  "-z * x = -z * y ⟹ --z * x = --z * y ⟹ x = y"
  by (metis case_split_left_equal tests_dual.inf_complement)

lemma preserves_equation:
  "-y * x ≤ x * -y ⟷ -y * x = -y * x * -y"
  apply (rule iffI)
  apply (simp add: test_preserves_equation tests_dual.sub_bot_least)
  by (simp add: test_preserves_equation tests_dual.sub_bot_least)

text ‹Theorem 5›

lemma preserve_test:
  "-y * x ≤ x * -y ⟹ -y * x⇧∘ = -y * x⇧∘ * -y"
  using circ_simulate preserves_equation by blast

text ‹Theorem 5›

lemma import_test:
  "-y * x ≤ x * -y ⟹ -y * x⇧∘ = -y * (-y * x)⇧∘"
  by (simp add: circ_import tests_dual.sub_bot_least)

definition ite :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" (‹_ ⊲ _ ⊳ _› [58,58,58] 57)
  where "x ⊲ p ⊳ y ≡ p * x ⊔ -p * y"

definition it :: "'a ⇒ 'a ⇒ 'a" (‹_ ⊳ _› [58,58] 57)
  where "p ⊳ x ≡ p * x ⊔ -p"

(*
definition while :: "'a ⇒ 'a ⇒ 'a" (infixr "⋆" 59)
  where "p ⋆ y ≡ (p * y)⇧∘ * -p"
*)

definition assigns :: "'a ⇒ 'a ⇒ 'a ⇒ bool"
  where "assigns x p q ≡ x = x * (p * q ⊔ -p * -q)"

definition preserves :: "'a ⇒ 'a ⇒ bool"
  where "preserves x p ≡ p * x ≤ x * p ∧ -p * x ≤ x * -p"

lemma ite_neg:
  "x ⊲ -p ⊳ y = y ⊲ --p ⊳ x"
  by (simp add: ite_def sup_commute)

lemma ite_import_true:
  "x ⊲ -p ⊳ y = -p * x ⊲ -p ⊳ y"
  by (metis ite_def tests_dual.sup_idempotent mult_assoc)

lemma ite_import_false:
  "x ⊲ -p ⊳ y = x ⊲ -p ⊳ --p * y"
  by (metis ite_import_true ite_neg)

lemma ite_import_true_false:
  "x ⊲ -p ⊳ y = -p * x ⊲ -p ⊳ --p * y"
  using ite_import_false ite_import_true by auto

lemma ite_context_true:
  "-p * (x ⊲ -p ⊳ y) = -p * x"
  by (metis sup_monoid.add_0_left tests_dual.sup_right_zero tests_dual.top_double_complement wnf_lemma_5 sup_bot_right ite_def mult_assoc mult_left_zero)

lemma ite_context_false:
  "--p * (x ⊲ -p ⊳ y) = --p * y"
  by (metis ite_neg ite_context_true)

lemma ite_context_import:
  "-p * (x ⊲ -q ⊳ y) = -p * (x ⊲ -p * -q ⊳ y)"
  by (smt ite_def mult_assoc tests_dual.sup_complement_intro tests_dual.sub_sup_demorgan tests_dual.sup_idempotent mult_left_dist_sup)

lemma ite_conjunction:
  "(x ⊲ -q ⊳ y) ⊲ -p ⊳ y = x ⊲ -p * -q ⊳ y"
  by (smt sup_assoc sup_commute ite_def mult_assoc tests_dual.sub_sup_demorgan mult_left_dist_sup mult_right_dist_sup tests_dual.inf_complement_intro)

lemma ite_disjunction:
  "x ⊲ -p ⊳ (x ⊲ -q ⊳ y) = x ⊲ -p ⊔ -q ⊳ y"
  by (smt (z3) tests_dual.sba_dual.sub_sup_closed sup_assoc ite_def mult_assoc tests_dual.sup_complement_intro tests_dual.sub_sup_demorgan mult_left_dist_sup mult_right_dist_sup tests_dual.inf_demorgan)

lemma wnf_lemma_6:
  "(-p ⊔ -q) * (x ⊲ --p * -q ⊳ y) = (-p ⊔ -q) * (y ⊲ -p ⊳ x)"
  by (smt (z3) ite_conjunction ite_context_false ite_context_true semiring.distrib_right tests_dual.sba_dual.inf_cases_2 tests_dual.sba_dual.sub_inf_def tests_dual.sba_dual.sup_complement_intro tests_dual.sub_complement)

lemma it_ite:
  "-p ⊳ x = x ⊲ -p ⊳ 1"
  by (simp add: it_def ite_def)

lemma it_neg:
  "--p ⊳ x = 1 ⊲ -p ⊳ x"
  using it_ite ite_neg by auto

lemma it_import_true:
  "-p ⊳ x = -p ⊳ -p * x"
  using it_ite ite_import_true by auto

lemma it_context_true:
  "-p * (-p ⊳ x) = -p * x"
  by (simp add: it_ite ite_context_true)

lemma it_context_false:
  "--p * (-p ⊳ x) = --p"
  using it_ite ite_context_false by force

lemma while_unfold_it:
  "-p ⋆ x = -p ⊳ x * (-p ⋆ x)"
  by (metis circ_loop_fixpoint it_def mult_assoc while_def)

lemma while_context_false:
  "--p * (-p ⋆ x) = --p"
  by (metis it_context_false while_unfold_it)

lemma while_context_true:
  "-p * (-p ⋆ x) = -p * x * (-p ⋆ x)"
  by (metis it_context_true mult_assoc while_unfold_it)

lemma while_zero:
  "bot ⋆ x = 1"
  by (metis circ_zero mult_left_one mult_left_zero one_def while_def)

lemma wnf_lemma_7:
  "1 * (bot ⋆ 1) = 1"
  by (simp add: while_zero)

lemma while_import_condition:
  "-p ⋆ x = -p ⋆ -p * x"
  by (metis mult_assoc tests_dual.sup_idempotent while_def)

lemma while_import_condition_2:
  "-p * -q ⋆ x = -p * -q ⋆ -p * x"
  by (metis mult_assoc tests_dual.sup_idempotent sub_comm while_def)

lemma wnf_lemma_8:
  "-r * (-p ⊔ --p * -q) ⋆ (x ⊲ --p * -q ⊳ y) = -r * (-p ⊔ -q) ⋆ (y ⊲ -p ⊳ x)"
  by (metis mult_assoc while_def wnf_lemma_6 tests_dual.sba_dual.sup_complement_intro)

text ‹Theorem 6 - see Theorem 31 on page 329 of Back and von Wright, Acta Informatica 36:295-334, 1999›

lemma split_merge_loops:
  assumes "--p * y ≤ y * --p"
    shows "(-p ⊔ -q) ⋆ (x ⊲ -p ⊳ y) = (-p ⋆ x) * (-q ⋆ y)"
proof -
  have "-p ⊔ -q ⋆ (x ⊲ -p ⊳ y) = (-p * x ⊔ --p * -q * y)⇧∘ * --p * --q"
    by (smt ite_def mult_assoc sup_commute tests_dual.inf_demorgan while_def wnf_lemma_5)
  thus ?thesis
    by (smt assms circ_sup_1 circ_slide import_test mult_assoc preserves_equation sub_comm while_context_false while_def)
qed

lemma assigns_same:
  "assigns x (-p) (-p)"
  by (simp add: assigns_def)

lemma preserves_equation_test:
  "preserves x (-p) ⟷ -p * x = -p * x * -p ∧ --p * x = --p * x * --p"
  using preserves_def preserves_equation by auto

lemma preserves_test:
  "preserves (-q) (-p)"
  using tests_dual.sub_commutative preserves_def by auto

lemma preserves_zero:
  "preserves bot (-p)"
  using tests_dual.sba_dual.sub_bot_def preserves_test by blast

lemma preserves_one:
  "preserves 1 (-p)"
  using preserves_def by force

lemma preserves_sup:
  "preserves x (-p) ⟹ preserves y (-p) ⟹ preserves (x ⊔ y) (-p)"
  by (simp add: mult_left_dist_sup mult_right_dist_sup preserves_equation_test)

lemma preserves_mult:
  "preserves x (-p) ⟹ preserves y (-p) ⟹ preserves (x * y) (-p)"
  by (smt (verit, best) mult_assoc preserves_equation_test)

lemma preserves_ite:
  "preserves x (-p) ⟹ preserves y (-p) ⟹ preserves (x ⊲ -q ⊳ y) (-p)"
  by (simp add: ite_def preserves_mult preserves_sup preserves_test)

lemma preserves_it:
  "preserves x (-p) ⟹ preserves (-q ⊳ x) (-p)"
  by (simp add: it_ite preserves_ite preserves_one)

lemma preserves_circ:
  "preserves x (-p) ⟹ preserves (x⇧∘) (-p)"
  by (meson circ_simulate preserves_def)

lemma preserves_while:
  "preserves x (-p) ⟹ preserves (-q ⋆ x) (-p)"
  using while_def preserves_circ preserves_mult preserves_test by auto

lemma preserves_test_neg:
  "preserves x (-p) ⟹ preserves x (--p)"
  using preserves_def by auto

lemma preserves_import_circ:
  "preserves x (-p) ⟹ -p * x⇧∘ = -p * (-p * x)⇧∘"
  using import_test preserves_def by blast

lemma preserves_simulate:
  "preserves x (-p) ⟹ -p * x⇧∘ = -p * x⇧∘ * -p"
  using preserve_test preserves_def by auto

lemma preserves_import_ite:
  assumes "preserves z (-p)"
    shows "z * (x ⊲ -p ⊳ y) = z * x ⊲ -p ⊳ z * y"
proof -
  have 1: "-p * z * (x ⊲ -p ⊳ y) = -p * (z * x ⊲ -p ⊳ z * y)"
    by (smt assms ite_context_true mult_assoc preserves_equation_test)
  have "--p * z * (x ⊲ -p ⊳ y) = --p * (z * x ⊲ -p ⊳ z * y)"
    by (smt (z3) assms ite_context_false mult_assoc preserves_equation_test)
  thus ?thesis
    using 1 by (metis mult_assoc test_case_split_left_equal)
qed

lemma preserves_while_context:
  "preserves x (-p) ⟹ -p * (-q ⋆ x) = -p * (-p * -q ⋆ x)"
  by (smt (verit, del_insts) mult_assoc tests_dual.sup_complement_intro tests_dual.sub_sup_demorgan preserves_import_circ preserves_mult preserves_simulate preserves_test while_def)

lemma while_ite_context_false:
  assumes "preserves y (-p)"
    shows "--p * (-p ⊔ -q ⋆ (x ⊲ -p ⊳ y)) = --p * (-q ⋆ y)"
proof -
  have "--p * (-p ⊔ -q ⋆ (x ⊲ -p ⊳ y)) = --p * (--p * -q * y)⇧∘ * -(-p ⊔ -q)"
    by (smt (z3) assms import_test mult_assoc preserves_equation preserves_equation_test sub_comm while_def tests_dual.sba_dual.sub_sup_demorgan preserves_test split_merge_loops while_context_false)
  thus ?thesis
    by (metis (no_types, lifting) assms preserves_def mult.assoc split_merge_loops while_context_false)
qed

text ‹Theorem 7.1›

lemma while_ite_norm:
  assumes "assigns z (-p) (-q)"
      and "preserves x1 (-q)"
      and "preserves x2 (-q)"
      and "preserves y1 (-q)"
      and "preserves y2 (-q)"
    shows "z * (x1 * (-r1 ⋆ y1) ⊲ -p ⊳ x2 * (-r2 ⋆ y2)) = z * (x1 ⊲ -q ⊳ x2) * ((-q * -r1 ⊔ --q * -r2) ⋆ (y1 ⊲ -q ⊳ y2))"
proof -
  have 1: "-(-q * -r1 ⊔ --q * -r2) = -q * --r1 ⊔ --q * --r2"
    by (smt (z3) tests_dual.complement_2 tests_dual.sub_sup_closed tests_dual.case_duality tests_dual.sub_sup_demorgan)
  have "-p * -q * x1 * (-q * -r1 * y1 ⊔ --q * -r2 * y2)⇧∘ * (-q * --r1 ⊔ --q * --r2) = -p * -q * x1 * -q * (-q * (-q * -r1 * y1 ⊔ --q * -r2 * y2))⇧∘ * (-q * --r1 ⊔ --q * --r2)"
    by (smt (verit, del_insts) assms(2,4,5) mult_assoc preserves_sup preserves_equation_test preserves_import_circ preserves_mult preserves_test)
  also have "... = -p * -q * x1 * -q * (-q * -r1 * y1)⇧∘ * (-q * --r1 ⊔ --q * --r2)"
    using ite_context_true ite_def mult_assoc by auto
  finally have 2: "-p * -q * x1 * (-q * -r1 * y1 ⊔ --q * -r2 * y2)⇧∘ * (-q * --r1 ⊔ --q * --r2) = -p * -q * x1 * (-r1 * y1)⇧∘ * --r1"
    by (smt (verit, del_insts) assms ite_context_true ite_def mult_assoc preserves_equation_test preserves_import_circ preserves_mult preserves_simulate preserves_test)
  have "--p * --q * x2 * (-q * -r1 * y1 ⊔ --q * -r2 * y2)⇧∘ * (-q * --r1 ⊔ --q * --r2) = --p * --q * x2 * --q * (--q * (-q * -r1 * y1 ⊔ --q * -r2 * y2))⇧∘ * (-q * --r1 ⊔ --q * --r2)"
    by (smt (verit, del_insts) assms mult_assoc preserves_sup preserves_equation_test preserves_import_circ preserves_mult preserves_test preserves_test_neg)
  also have "... = --p * --q * x2 * --q * (--q * -r2 * y2)⇧∘ * (-q * --r1 ⊔ --q * --r2)"
    using ite_context_false ite_def mult_assoc by auto
  finally have "--p * --q * x2 * (-q * -r1 * y1 ⊔ --q * -r2 * y2)⇧∘ * (-q * --r1 ⊔ --q * --r2) = --p * --q * x2 * (-r2 * y2)⇧∘ * --r2"
    by (smt (verit, del_insts) assms(3,5) ite_context_false ite_def mult_assoc preserves_equation_test preserves_import_circ preserves_mult preserves_simulate preserves_test preserves_test_neg)
  thus ?thesis
    using 1 2 by (smt (z3) assms(1) assigns_def mult_assoc mult_right_dist_sup while_def ite_context_false ite_context_true tests_dual.sub_commutative)
qed

lemma while_it_norm:
  "assigns z (-p) (-q) ⟹ preserves x (-q) ⟹ preserves y (-q) ⟹ z * (-p ⊳ x * (-r ⋆ y)) = z * (-q ⊳ x) * (-q * -r ⋆ y)"
  by (metis sup_bot_right tests_dual.sup_right_zero it_context_true it_ite tests_dual.complement_bot preserves_one while_import_condition_2 while_ite_norm wnf_lemma_7)

lemma while_else_norm:
  "assigns z (-p) (-q) ⟹ preserves x (-q) ⟹ preserves y (-q) ⟹ z * (1 ⊲ -p ⊳ x * (-r ⋆ y)) = z * (1 ⊲ -q ⊳ x) * (--q * -r ⋆ y)"
  by (metis sup_bot_left tests_dual.sup_right_zero ite_context_false tests_dual.complement_bot preserves_one while_import_condition_2 while_ite_norm wnf_lemma_7)

lemma while_while_pre_norm:
  "-p ⋆ x * (-q ⋆ y) = -p ⊳ x * (-p ⊔ -q ⋆ (y ⊲ -q ⊳ x))"
  by (smt sup_commute circ_sup_1 circ_left_unfold circ_slide it_def ite_def mult_assoc mult_left_one mult_right_dist_sup tests_dual.inf_demorgan while_def wnf_lemma_5)

text ‹Theorem 7.2›

lemma while_while_norm:
  "assigns z (-p) (-r) ⟹ preserves x (-r) ⟹ preserves y (-r) ⟹ z * (-p ⋆ x * (-q ⋆ y)) = z * (-r ⊳ x) * (-r * (-p ⊔ -q) ⋆ (y ⊲ -q ⊳ x))"
  by (smt tests_dual.double_negation tests_dual.sub_sup_demorgan tests_dual.inf_demorgan preserves_ite while_it_norm while_while_pre_norm)

lemma while_seq_replace:
  "assigns z (-p) (-q) ⟹ z * (-p ⋆ x * z) * y = z * (-q ⋆ x * z) * y"
  by (smt assigns_def circ_slide mult_assoc tests_dual.wnf_lemma_1 tests_dual.wnf_lemma_2 tests_dual.wnf_lemma_3 tests_dual.wnf_lemma_4 while_def)

lemma while_ite_replace:
  "assigns z (-p) (-q) ⟹ z * (x ⊲ -p ⊳ y) = z * (x ⊲ -q ⊳ y)"
  by (smt assigns_def ite_def mult_assoc mult_left_dist_sup sub_comm tests_dual.wnf_lemma_1 tests_dual.wnf_lemma_3)

lemma while_post_norm_an:
  assumes "preserves y (-p)"
    shows "(-p ⋆ x) * y = y ⊲ --p ⊳ (-p ⋆ x * (--p ⊳ y))"
proof -
  have "-p * (-p * x * (--p * y ⊔ -p))⇧∘ * --p = -p * x * ((--p * y ⊔ -p) * -p * x)⇧∘ * (--p * y ⊔ -p) * --p"
    by (metis circ_slide_1 while_def mult_assoc while_context_true)
  also have "... = -p * x * (--p * y * bot ⊔ -p * x)⇧∘ * --p * y"
    by (smt assms sup_bot_right mult_assoc tests_dual.sup_complement tests_dual.sup_idempotent mult_left_zero mult_right_dist_sup preserves_equation_test sub_comm)
  finally have "-p * (-p * x * (--p * y ⊔ -p))⇧∘ * --p = -p * x * (-p * x)⇧∘ * --p * y"
    by (metis circ_sup_mult_zero sup_commute mult_assoc)
  thus ?thesis
    by (smt circ_left_unfold tests_dual.double_negation it_def ite_def mult_assoc mult_left_one mult_right_dist_sup while_def)
qed

lemma while_post_norm:
  "preserves y (-p) ⟹ (-p ⋆ x) * y = -p ⋆ x * (1 ⊲ -p ⊳ y) ⊲ -p ⊳ y"
  using it_neg ite_neg while_post_norm_an by force

lemma wnf_lemma_9:
  assumes "assigns z (-p) (-q)"
      and "preserves x1 (-q)"
      and "preserves y1 (-q)"
      and "preserves x2 (-q)"
      and "preserves y2 (-q)"
      and "preserves x2 (-p)"
      and "preserves y2 (-p)"
    shows "z * (x1 ⊲ -q ⊳ x2) * (-q * -p ⊔ -r ⋆ (y1 ⊲ -q * -p ⊳ y2)) = z * (x1 ⊲ -p ⊳ x2) * (-p ⊔ -r ⋆ (y1 ⊲ -p ⊳ y2))"
proof -
  have "z * --p * --q * (x1 ⊲ -q ⊳ x2) * (-q * -p ⊔ -r ⋆ (y1 ⊲ -q * -p ⊳ y2)) = z * --p * --q * x2 * --q * (--q * (-q * -p ⊔ -r) ⋆ (y1 ⊲ -q * -p ⊳ y2))"
    by (smt (verit, del_insts) assms(3-5) tests_dual.double_negation ite_context_false mult_assoc tests_dual.sub_sup_demorgan tests_dual.inf_demorgan preserves_equation_test preserves_ite preserves_while_context)
  also have "... = z * --p * --q * x2 * --q * (--q * -r ⋆ --q * y2)"
    by (smt sup_bot_left tests_dual.double_negation ite_conjunction ite_context_false mult_assoc tests_dual.sup_complement mult_left_dist_sup mult_left_zero while_import_condition_2)
  also have "... = z * --p * --q * x2 * (-r ⋆ y2)"
    by (metis assms(4,5) mult_assoc preserves_equation_test preserves_test_neg preserves_while_context while_import_condition_2)
  finally have 1: "z * --p * --q * (x1 ⊲ -q ⊳ x2) * (-q * -p ⊔ -r ⋆ (y1 ⊲ -q * -p ⊳ y2)) = z * --p * --q * (x1 ⊲ -q ⊳ x2) * (-p ⊔ -r ⋆ (y1 ⊲ -p ⊳ y2))"
    by (smt assms(6,7) ite_context_false mult_assoc preserves_equation_test sub_comm while_ite_context_false)
  have "z * -p * -q * (x1 ⊲ -q ⊳ x2) * (-q * -p ⊔ -r ⋆ (y1 ⊲ -q * -p ⊳ y2)) = z * -p * -q * (x1 ⊲ -q ⊳ x2) * -q * (-q * (-p ⊔ -r) ⋆ -q * (y1 ⊲ -p ⊳ y2))"
    by (smt (verit, del_insts) assms(2-5) tests_dual.double_negation ite_context_import mult_assoc tests_dual.sub_sup_demorgan tests_dual.sup_idempotent mult_left_dist_sup tests_dual.inf_demorgan preserves_equation_test preserves_ite preserves_while_context while_import_condition_2)
  hence "z * -p * -q * (x1 ⊲ -q ⊳ x2) * (-q * -p ⊔ -r ⋆ (y1 ⊲ -q * -p ⊳ y2)) = z * -p * -q * (x1 ⊲ -q ⊳ x2) * (-p ⊔ -r ⋆ (y1 ⊲ -p ⊳ y2))"
    by (smt assms(2-5) tests_dual.double_negation mult_assoc tests_dual.sub_sup_demorgan tests_dual.sup_idempotent preserves_equation_test preserves_ite preserves_while_context while_import_condition_2)
  thus ?thesis
    using 1 by (smt assms(1) assigns_def mult_assoc mult_left_dist_sup mult_right_dist_sup while_ite_replace)
qed

text ‹Theorem 7.3›

lemma while_seq_norm:
  assumes "assigns z1 (-r1) (-q)"
      and "preserves x2 (-q)"
      and "preserves y2 (-q)"
      and "preserves z2 (-q)"
      and "z1 * z2 = z2 * z1"
      and "assigns z2 (-q) (-r)"
      and "preserves y1 (-r)"
      and "preserves z1 (-r)"
      and "preserves x2 (-r)"
      and "preserves y2 (-r)"
    shows "x1 * z1 * z2 * (-r1 ⋆ y1 * z1) * x2 * (-r2 ⋆ y2) = x1 * z1 * z2 * (y1 * z1 * (1 ⊲ -q ⊳ x2) ⊲ -q ⊳ x2) * (-q ⊔ -r2 ⋆ (y1 * z1 * (1 ⊲ -q ⊳ x2) ⊲ -q ⊳ y2))"
proof -
  have 1: "preserves (y1 * z1 * (1 ⊲ -q ⊳ x2)) (-r)"
    by (simp add: assms(7-9) ite_def preserves_mult preserves_sup preserves_test)
  hence 2: "preserves (y1 * z1 * (1 ⊲ -q ⊳ x2) ⊲ -q ⊳ y2) (-r)"
    by (simp add: assms(10) preserves_ite)
  have "x1 * z1 * z2 * (-r1 ⋆ y1 * z1) * x2 * (-r2 ⋆ y2) = x1 * z1 * z2 * (-q ⋆ y1 * z1) * x2 * (-r2 ⋆ y2)"
    using assms(1,5) mult_assoc while_seq_replace by auto
  also have "... = x1 * z1 * z2 * (-q ⋆ y1 * z1 * (1 ⊲ -q ⊳ x2 * (-r2 ⋆ y2)) ⊲ -q ⊳ x2 * (-r2 ⋆ y2))"
    by (smt assms(2,3) mult_assoc preserves_mult preserves_while while_post_norm)
  also have "... = x1 * z1 * (z2 * (-q ⋆ y1 * z1 * (1 ⊲ -q ⊳ x2) * (--q * -r2 ⋆ y2)) ⊲ -q ⊳ z2 * x2 * (-r2 ⋆ y2))"
    by (smt assms(2-4) assigns_same mult_assoc preserves_import_ite while_else_norm)
  also have "... = x1 * z1 * (z2 * (-r ⊳ y1 * z1 * (1 ⊲ -q ⊳ x2)) * (-r * (-q ⊔ -r2) ⋆ (y1 * z1 * (1 ⊲ -q ⊳ x2) ⊲ -q ⊳ y2)) ⊲ -q ⊳ z2 * x2 * (-r2 ⋆ y2))"
    by (smt assms(6-10) tests_dual.double_negation tests_dual.sub_sup_demorgan tests_dual.inf_demorgan preserves_ite preserves_mult preserves_one while_while_norm wnf_lemma_8)
  also have "... = x1 * z1 * z2 * ((-r ⊳ y1 * z1 * (1 ⊲ -q ⊳ x2)) * (-r * (-q ⊔ -r2) ⋆ (y1 * z1 * (1 ⊲ -q ⊳ x2) ⊲ -q ⊳ y2)) ⊲ -r ⊳ x2 * (-r2 ⋆ y2))"
    by (smt assms(4,6) mult_assoc preserves_import_ite while_ite_replace)
  also have "... = x1 * z1 * z2 * (-r * (y1 * z1 * (1 ⊲ -q ⊳ x2)) * (-r * (-q ⊔ -r2) ⋆ (y1 * z1 * (1 ⊲ -q ⊳ x2) ⊲ -q ⊳ y2)) ⊲ -r ⊳ x2 * (-r2 ⋆ y2))"
    by (smt mult_assoc it_context_true ite_import_true)
  also have "... = x1 * z1 * z2 * (-r * (y1 * z1 * (1 ⊲ -q ⊳ x2)) * -r * (-r * (-q ⊔ -r2) ⋆ (y1 * z1 * (1 ⊲ -q ⊳ x2) ⊲ -q ⊳ y2)) ⊲ -r ⊳ x2 * (-r2 ⋆ y2))"
    using 1 by (simp add: preserves_equation_test)
  also have "... = x1 * z1 * z2 * (-r * (y1 * z1 * (1 ⊲ -q ⊳ x2)) * -r * (-q ⊔ -r2 ⋆ (y1 * z1 * (1 ⊲ -q ⊳ x2) ⊲ -q ⊳ y2)) ⊲ -r ⊳ x2 * (-r2 ⋆ y2))"
    using 2 by (smt (z3) tests_dual.sba_dual.sub_sup_closed mult_assoc preserves_while_context)
  also have "... = x1 * z1 * z2 * (y1 * z1 * (1 ⊲ -q ⊳ x2) * (-q ⊔ -r2 ⋆ (y1 * z1 * (1 ⊲ -q ⊳ x2) ⊲ -q ⊳ y2)) ⊲ -q ⊳ x2 * (-r2 ⋆ y2))"
    by (smt assms(6-9) tests_dual.double_negation ite_import_true mult_assoc tests_dual.sup_idempotent preserves_equation_test preserves_ite preserves_one while_ite_replace)
  also have "... = x1 * z1 * z2 * (y1 * z1 * (1 ⊲ -q ⊳ x2) ⊲ -r ⊳ x2) * ((-r * (-q ⊔ -r2) ⊔ --r * -r2) ⋆ ((y1 * z1 * (1 ⊲ -q ⊳ x2) ⊲ -q ⊳ y2) ⊲ -r ⊳ y2))"
    by (smt assms(6-10) tests_dual.double_negation mult_assoc tests_dual.sub_sup_demorgan tests_dual.inf_demorgan preserves_ite preserves_mult preserves_one while_ite_norm)
  also have "... = x1 * z1 * z2 * (y1 * z1 * (1 ⊲ -q ⊳ x2) ⊲ -r ⊳ x2) * ((-r * (-q ⊔ -r2) ⊔ --r * -r2) ⋆ (y1 * z1 * (1 ⊲ -q ⊳ x2) ⊲ -r * -q ⊳ y2))"
    using ite_conjunction by simp
  also have "... = x1 * z1 * z2 * (y1 * z1 * (1 ⊲ -q ⊳ x2) ⊲ -r ⊳ x2) * ((-r * -q ⊔ -r2) ⋆ (y1 * z1 * (1 ⊲ -q ⊳ x2) ⊲ -r * -q ⊳ y2))"
    by (smt (z3) mult_left_dist_sup sup_assoc tests_dual.sba_dual.sup_cases tests_dual.sub_commutative)
  also have "... = x1 * z1 * z2 * (y1 * z1 * (1 ⊲ -q ⊳ x2) ⊲ -q ⊳ x2) * (-q ⊔ -r2 ⋆ (y1 * z1 * (1 ⊲ -q ⊳ x2) ⊲ -q ⊳ y2))"
    using 1 by (metis assms(2,3,6,9,10) mult_assoc wnf_lemma_9)
  finally show ?thesis
    .
qed

end

end