[STATEMENT]
lemma invar_enqL: "invar deque \<Longrightarrow> invar (enqL x deque)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar deque \<Longrightarrow> invar (enqL x deque)
[PROOF STEP]
proof(induction x deque rule: enqL.induct)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x. invar Empty \<Longrightarrow> invar (enqL x Empty)
 2. \<And>x y. invar (One y) \<Longrightarrow> invar (enqL x (One y))
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> invar (enqL x (Two y z))
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> invar (enqL x (Three a b c))
 5. \<And>x left right length_right. invar (deque.Idle left (idle.Idle right length_right)) \<Longrightarrow> invar (enqL x (deque.Idle left (idle.Idle right length_right)))
 6. \<And>x big small. invar (Transforming (States direction.Left big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
 7. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
case (5 x left right length_right)
[PROOF STATE]
proof (state)
this:
invar (deque.Idle left (idle.Idle right length_right))

goal (7 subgoals):
 1. \<And>x. invar Empty \<Longrightarrow> invar (enqL x Empty)
 2. \<And>x y. invar (One y) \<Longrightarrow> invar (enqL x (One y))
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> invar (enqL x (Two y z))
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> invar (enqL x (Three a b c))
 5. \<And>x left right length_right. invar (deque.Idle left (idle.Idle right length_right)) \<Longrightarrow> invar (enqL x (deque.Idle left (idle.Idle right length_right)))
 6. \<And>x big small. invar (Transforming (States direction.Left big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
 7. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
obtain left' length_left' where pushed [simp]:
      "Idle.push x left = idle.Idle left' length_left'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>left' length_left'. Idle.push x left = idle.Idle left' length_left' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using is_empty_idle.cases
[PROOF STATE]
proof (prove)
using this:
(\<And>stack uu_. ?x = idle.Idle stack uu_ \<Longrightarrow> ?P) \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>left' length_left'. Idle.push x left = idle.Idle left' length_left' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Idle.push x left = idle.Idle left' length_left'

goal (7 subgoals):
 1. \<And>x. invar Empty \<Longrightarrow> invar (enqL x Empty)
 2. \<And>x y. invar (One y) \<Longrightarrow> invar (enqL x (One y))
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> invar (enqL x (Two y z))
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> invar (enqL x (Three a b c))
 5. \<And>x left right length_right. invar (deque.Idle left (idle.Idle right length_right)) \<Longrightarrow> invar (enqL x (deque.Idle left (idle.Idle right length_right)))
 6. \<And>x big small. invar (Transforming (States direction.Left big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
 7. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Idle.push x left = idle.Idle left' length_left'
[PROOF STEP]
have invar_left': "invar (idle.Idle left' length_left')"
[PROOF STATE]
proof (prove)
using this:
Idle.push x left = idle.Idle left' length_left'

goal (1 subgoal):
 1. invar (idle.Idle left' length_left')
[PROOF STEP]
using Idle_Proof.invar_push[of left x] 5
[PROOF STATE]
proof (prove)
using this:
Idle.push x left = idle.Idle left' length_left'
invar left \<Longrightarrow> invar (Idle.push x left)
invar (deque.Idle left (idle.Idle right length_right))

goal (1 subgoal):
 1. invar (idle.Idle left' length_left')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invar (idle.Idle left' length_left')

goal (7 subgoals):
 1. \<And>x. invar Empty \<Longrightarrow> invar (enqL x Empty)
 2. \<And>x y. invar (One y) \<Longrightarrow> invar (enqL x (One y))
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> invar (enqL x (Two y z))
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> invar (enqL x (Three a b c))
 5. \<And>x left right length_right. invar (deque.Idle left (idle.Idle right length_right)) \<Longrightarrow> invar (enqL x (deque.Idle left (idle.Idle right length_right)))
 6. \<And>x big small. invar (Transforming (States direction.Left big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
 7. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
have [simp]: "size left' = Suc (size left)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size left' = Suc (size left)
[PROOF STEP]
using Idle_Proof.size_push[of x left]
[PROOF STATE]
proof (prove)
using this:
size (Idle.push x left) = Suc (size left)

goal (1 subgoal):
 1. size left' = Suc (size left)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
size left' = Suc (size left)

goal (7 subgoals):
 1. \<And>x. invar Empty \<Longrightarrow> invar (enqL x Empty)
 2. \<And>x y. invar (One y) \<Longrightarrow> invar (enqL x (One y))
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> invar (enqL x (Two y z))
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> invar (enqL x (Three a b c))
 5. \<And>x left right length_right. invar (deque.Idle left (idle.Idle right length_right)) \<Longrightarrow> invar (enqL x (deque.Idle left (idle.Idle right length_right)))
 6. \<And>x big small. invar (Transforming (States direction.Left big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
 7. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar (enqL x (deque.Idle left (idle.Idle right length_right)))
[PROOF STEP]
proof(cases "length_left' \<le> 3 * length_right")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length_left' \<le> 3 * length_right \<Longrightarrow> invar (enqL x (deque.Idle left (idle.Idle right length_right)))
 2. \<not> length_left' \<le> 3 * length_right \<Longrightarrow> invar (enqL x (deque.Idle left (idle.Idle right length_right)))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
length_left' \<le> 3 * length_right

goal (2 subgoals):
 1. length_left' \<le> 3 * length_right \<Longrightarrow> invar (enqL x (deque.Idle left (idle.Idle right length_right)))
 2. \<not> length_left' \<le> 3 * length_right \<Longrightarrow> invar (enqL x (deque.Idle left (idle.Idle right length_right)))
[PROOF STEP]
with 5
[PROOF STATE]
proof (chain)
picking this:
invar (deque.Idle left (idle.Idle right length_right))
length_left' \<le> 3 * length_right
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
invar (deque.Idle left (idle.Idle right length_right))
length_left' \<le> 3 * length_right

goal (1 subgoal):
 1. invar (enqL x (deque.Idle left (idle.Idle right length_right)))
[PROOF STEP]
using invar_left' Idle_Proof.size_push[of x left] Stack_Proof.size_not_empty[of left']
[PROOF STATE]
proof (prove)
using this:
invar (deque.Idle left (idle.Idle right length_right))
length_left' \<le> 3 * length_right
invar (idle.Idle left' length_left')
size (Idle.push x left) = Suc (size left)
(0 < size left') = (\<not> is_empty left')

goal (1 subgoal):
 1. invar (enqL x (deque.Idle left (idle.Idle right length_right)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invar (enqL x (deque.Idle left (idle.Idle right length_right)))

goal (1 subgoal):
 1. \<not> length_left' \<le> 3 * length_right \<Longrightarrow> invar (enqL x (deque.Idle left (idle.Idle right length_right)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> length_left' \<le> 3 * length_right \<Longrightarrow> invar (enqL x (deque.Idle left (idle.Idle right length_right)))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> length_left' \<le> 3 * length_right

goal (1 subgoal):
 1. \<not> length_left' \<le> 3 * length_right \<Longrightarrow> invar (enqL x (deque.Idle left (idle.Idle right length_right)))
[PROOF STEP]
let ?length_left = "length_left' - length_right - 1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> length_left' \<le> 3 * length_right \<Longrightarrow> invar (enqL x (deque.Idle left (idle.Idle right length_right)))
[PROOF STEP]
let ?length_right = "Suc (2 * length_right)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> length_left' \<le> 3 * length_right \<Longrightarrow> invar (enqL x (deque.Idle left (idle.Idle right length_right)))
[PROOF STEP]
let ?states = "States Right
          (Reverse (Current [] 0 left' ?length_left) left' [] ?length_left)
          (Reverse1 (Current [] 0 right ?length_right) right [])"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> length_left' \<le> 3 * length_right \<Longrightarrow> invar (enqL x (deque.Idle left (idle.Idle right length_right)))
[PROOF STEP]
let ?states_stepped = "(step^^6) ?states"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> length_left' \<le> 3 * length_right \<Longrightarrow> invar (enqL x (deque.Idle left (idle.Idle right length_right)))
[PROOF STEP]
from invar_left' 5 False
[PROOF STATE]
proof (chain)
picking this:
invar (idle.Idle left' length_left')
invar (deque.Idle left (idle.Idle right length_right))
\<not> length_left' \<le> 3 * length_right
[PROOF STEP]
have invar: "invar ?states"
[PROOF STATE]
proof (prove)
using this:
invar (idle.Idle left' length_left')
invar (deque.Idle left (idle.Idle right length_right))
\<not> length_left' \<le> 3 * length_right

goal (1 subgoal):
 1. invar (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right []))
[PROOF STEP]
by(auto simp: rev_drop rev_take)
[PROOF STATE]
proof (state)
this:
invar (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right []))

goal (1 subgoal):
 1. \<not> length_left' \<le> 3 * length_right \<Longrightarrow> invar (enqL x (deque.Idle left (idle.Idle right length_right)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right []))
[PROOF STEP]
have invar_stepped: "invar ?states_stepped"
[PROOF STATE]
proof (prove)
using this:
invar (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right []))

goal (1 subgoal):
 1. invar ((step ^^ 6) (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right [])))
[PROOF STEP]
using invar_step_n
[PROOF STATE]
proof (prove)
using this:
invar (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right []))
invar ?states \<Longrightarrow> invar ((step ^^ ?n) ?states)

goal (1 subgoal):
 1. invar ((step ^^ 6) (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right [])))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
invar ((step ^^ 6) (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right [])))

goal (1 subgoal):
 1. \<not> length_left' \<le> 3 * length_right \<Longrightarrow> invar (enqL x (deque.Idle left (idle.Idle right length_right)))
[PROOF STEP]
from False invar_left' 5
[PROOF STATE]
proof (chain)
picking this:
\<not> length_left' \<le> 3 * length_right
invar (idle.Idle left' length_left')
invar (deque.Idle left (idle.Idle right length_right))
[PROOF STEP]
have remaining_steps: "6 < remaining_steps ?states"
[PROOF STATE]
proof (prove)
using this:
\<not> length_left' \<le> 3 * length_right
invar (idle.Idle left' length_left')
invar (deque.Idle left (idle.Idle right length_right))

goal (1 subgoal):
 1. 6 < remaining_steps (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right []))
[PROOF STEP]
using Stack_Proof.size_not_empty[of right]
[PROOF STATE]
proof (prove)
using this:
\<not> length_left' \<le> 3 * length_right
invar (idle.Idle left' length_left')
invar (deque.Idle left (idle.Idle right length_right))
(0 < size right) = (\<not> is_empty right)

goal (1 subgoal):
 1. 6 < remaining_steps (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right []))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
6 < remaining_steps (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right []))

goal (1 subgoal):
 1. \<not> length_left' \<le> 3 * length_right \<Longrightarrow> invar (enqL x (deque.Idle left (idle.Idle right length_right)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
6 < remaining_steps (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right []))
[PROOF STEP]
have remaining_steps_stepped: "0 < remaining_steps ?states_stepped"
[PROOF STATE]
proof (prove)
using this:
6 < remaining_steps (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right []))

goal (1 subgoal):
 1. 0 < remaining_steps ((step ^^ 6) (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right [])))
[PROOF STEP]
using invar remaining_steps_n_steps_sub
[PROOF STATE]
proof (prove)
using this:
6 < remaining_steps (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right []))
invar (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right []))
invar ?states \<Longrightarrow> remaining_steps ((step ^^ ?n) ?states) = remaining_steps ?states - ?n

goal (1 subgoal):
 1. 0 < remaining_steps ((step ^^ 6) (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right [])))
[PROOF STEP]
by (metis zero_less_diff)
[PROOF STATE]
proof (state)
this:
0 < remaining_steps ((step ^^ 6) (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right [])))

goal (1 subgoal):
 1. \<not> length_left' \<le> 3 * length_right \<Longrightarrow> invar (enqL x (deque.Idle left (idle.Idle right length_right)))
[PROOF STEP]
from False invar_left' 5
[PROOF STATE]
proof (chain)
picking this:
\<not> length_left' \<le> 3 * length_right
invar (idle.Idle left' length_left')
invar (deque.Idle left (idle.Idle right length_right))
[PROOF STEP]
have "size_ok' ?states (remaining_steps ?states - 6)"
[PROOF STATE]
proof (prove)
using this:
\<not> length_left' \<le> 3 * length_right
invar (idle.Idle left' length_left')
invar (deque.Idle left (idle.Idle right length_right))

goal (1 subgoal):
 1. size_ok' (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right [])) (remaining_steps (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right [])) - 6)
[PROOF STEP]
using Stack_Proof.size_not_empty[of right]
            size_not_empty
[PROOF STATE]
proof (prove)
using this:
\<not> length_left' \<le> 3 * length_right
invar (idle.Idle left' length_left')
invar (deque.Idle left (idle.Idle right length_right))
(0 < size right) = (\<not> is_empty right)
(0 < size ?idle) = (\<not> is_empty ?idle)

goal (1 subgoal):
 1. size_ok' (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right [])) (remaining_steps (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right [])) - 6)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
size_ok' (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right [])) (remaining_steps (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right [])) - 6)

goal (1 subgoal):
 1. \<not> length_left' \<le> 3 * length_right \<Longrightarrow> invar (enqL x (deque.Idle left (idle.Idle right length_right)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
size_ok' (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right [])) (remaining_steps (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right [])) - 6)
[PROOF STEP]
have size_ok_stepped: "size_ok ?states_stepped"
[PROOF STATE]
proof (prove)
using this:
size_ok' (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right [])) (remaining_steps (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right [])) - 6)

goal (1 subgoal):
 1. size_ok ((step ^^ 6) (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right [])))
[PROOF STEP]
using size_ok_steps[of ?states 6] remaining_steps invar
[PROOF STATE]
proof (prove)
using this:
size_ok' (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right [])) (remaining_steps (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right [])) - 6)
\<lbrakk>invar (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right [])); 6 < remaining_steps (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right [])); size_ok' (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right [])) (remaining_steps (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right [])) - 6)\<rbrakk> \<Longrightarrow> size_ok ((step ^^ 6) (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right [])))
6 < remaining_steps (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right []))
invar (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right []))

goal (1 subgoal):
 1. size_ok ((step ^^ 6) (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right [])))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
size_ok ((step ^^ 6) (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right [])))

goal (1 subgoal):
 1. \<not> length_left' \<le> 3 * length_right \<Longrightarrow> invar (enqL x (deque.Idle left (idle.Idle right length_right)))
[PROOF STEP]
from False
[PROOF STATE]
proof (chain)
picking this:
\<not> length_left' \<le> 3 * length_right
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> length_left' \<le> 3 * length_right

goal (1 subgoal):
 1. invar (enqL x (deque.Idle left (idle.Idle right length_right)))
[PROOF STEP]
using invar_stepped remaining_steps_stepped size_ok_stepped
[PROOF STATE]
proof (prove)
using this:
\<not> length_left' \<le> 3 * length_right
invar ((step ^^ 6) (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right [])))
0 < remaining_steps ((step ^^ 6) (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right [])))
size_ok ((step ^^ 6) (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (Suc (2 * length_right))) right [])))

goal (1 subgoal):
 1. invar (enqL x (deque.Idle left (idle.Idle right length_right)))
[PROOF STEP]
by(auto simp: Let_def)
[PROOF STATE]
proof (state)
this:
invar (enqL x (deque.Idle left (idle.Idle right length_right)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
invar (enqL x (deque.Idle left (idle.Idle right length_right)))

goal (6 subgoals):
 1. \<And>x. invar Empty \<Longrightarrow> invar (enqL x Empty)
 2. \<And>x y. invar (One y) \<Longrightarrow> invar (enqL x (One y))
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> invar (enqL x (Two y z))
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> invar (enqL x (Three a b c))
 5. \<And>x big small. invar (Transforming (States direction.Left big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
 6. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x. invar Empty \<Longrightarrow> invar (enqL x Empty)
 2. \<And>x y. invar (One y) \<Longrightarrow> invar (enqL x (One y))
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> invar (enqL x (Two y z))
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> invar (enqL x (Three a b c))
 5. \<And>x big small. invar (Transforming (States direction.Left big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
 6. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
case (6 x big small)
[PROOF STATE]
proof (state)
this:
invar (Transforming (States direction.Left big small))

goal (6 subgoals):
 1. \<And>x. invar Empty \<Longrightarrow> invar (enqL x Empty)
 2. \<And>x y. invar (One y) \<Longrightarrow> invar (enqL x (One y))
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> invar (enqL x (Two y z))
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> invar (enqL x (Three a b c))
 5. \<And>x big small. invar (Transforming (States direction.Left big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
 6. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
let ?small = "Small.push x small"
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x. invar Empty \<Longrightarrow> invar (enqL x Empty)
 2. \<And>x y. invar (One y) \<Longrightarrow> invar (enqL x (One y))
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> invar (enqL x (Two y z))
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> invar (enqL x (Three a b c))
 5. \<And>x big small. invar (Transforming (States direction.Left big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
 6. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
let ?states = "States Left big ?small"
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x. invar Empty \<Longrightarrow> invar (enqL x Empty)
 2. \<And>x y. invar (One y) \<Longrightarrow> invar (enqL x (One y))
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> invar (enqL x (Two y z))
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> invar (enqL x (Three a b c))
 5. \<And>x big small. invar (Transforming (States direction.Left big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
 6. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
let ?states_stepped = "(step^^4) ?states"
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x. invar Empty \<Longrightarrow> invar (enqL x Empty)
 2. \<And>x y. invar (One y) \<Longrightarrow> invar (enqL x (One y))
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> invar (enqL x (Two y z))
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> invar (enqL x (Three a b c))
 5. \<And>x big small. invar (Transforming (States direction.Left big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
 6. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
from 6
[PROOF STATE]
proof (chain)
picking this:
invar (Transforming (States direction.Left big small))
[PROOF STEP]
have invar: "invar ?states"
[PROOF STATE]
proof (prove)
using this:
invar (Transforming (States direction.Left big small))

goal (1 subgoal):
 1. invar (States direction.Left big (Small.push x small))
[PROOF STEP]
using invar_push_small[of Left big small x]
[PROOF STATE]
proof (prove)
using this:
invar (Transforming (States direction.Left big small))
invar (States direction.Left big small) \<Longrightarrow> invar (States direction.Left big (Small.push x small))

goal (1 subgoal):
 1. invar (States direction.Left big (Small.push x small))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invar (States direction.Left big (Small.push x small))

goal (6 subgoals):
 1. \<And>x. invar Empty \<Longrightarrow> invar (enqL x Empty)
 2. \<And>x y. invar (One y) \<Longrightarrow> invar (enqL x (One y))
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> invar (enqL x (Two y z))
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> invar (enqL x (Three a b c))
 5. \<And>x big small. invar (Transforming (States direction.Left big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
 6. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (States direction.Left big (Small.push x small))
[PROOF STEP]
have invar_stepped: "invar ?states_stepped"
[PROOF STATE]
proof (prove)
using this:
invar (States direction.Left big (Small.push x small))

goal (1 subgoal):
 1. invar ((step ^^ 4) (States direction.Left big (Small.push x small)))
[PROOF STEP]
using invar_step_n
[PROOF STATE]
proof (prove)
using this:
invar (States direction.Left big (Small.push x small))
invar ?states \<Longrightarrow> invar ((step ^^ ?n) ?states)

goal (1 subgoal):
 1. invar ((step ^^ 4) (States direction.Left big (Small.push x small)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
invar ((step ^^ 4) (States direction.Left big (Small.push x small)))

goal (6 subgoals):
 1. \<And>x. invar Empty \<Longrightarrow> invar (enqL x Empty)
 2. \<And>x y. invar (One y) \<Longrightarrow> invar (enqL x (One y))
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> invar (enqL x (Two y z))
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> invar (enqL x (Three a b c))
 5. \<And>x big small. invar (Transforming (States direction.Left big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
 6. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar (enqL x (Transforming (States direction.Left big small)))
[PROOF STEP]
proof(cases "4 < remaining_steps ?states")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 4 < remaining_steps (States direction.Left big (Small.push x small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
 2. \<not> 4 < remaining_steps (States direction.Left big (Small.push x small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
4 < remaining_steps (States direction.Left big (Small.push x small))

goal (2 subgoals):
 1. 4 < remaining_steps (States direction.Left big (Small.push x small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
 2. \<not> 4 < remaining_steps (States direction.Left big (Small.push x small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
[PROOF STEP]
obtain big_stepped small_stepped where stepped [simp]:
       "?states_stepped = States Left big_stepped small_stepped"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>big_stepped small_stepped. (step ^^ 4) (States direction.Left big (Small.push x small)) = States direction.Left big_stepped small_stepped \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis remaining_steps_states.cases step_n_same)
[PROOF STATE]
proof (state)
this:
(step ^^ 4) (States direction.Left big (Small.push x small)) = States direction.Left big_stepped small_stepped

goal (2 subgoals):
 1. 4 < remaining_steps (States direction.Left big (Small.push x small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
 2. \<not> 4 < remaining_steps (States direction.Left big (Small.push x small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
[PROOF STEP]
from True
[PROOF STATE]
proof (chain)
picking this:
4 < remaining_steps (States direction.Left big (Small.push x small))
[PROOF STEP]
have remaining_steps: "0 < remaining_steps ?states_stepped"
[PROOF STATE]
proof (prove)
using this:
4 < remaining_steps (States direction.Left big (Small.push x small))

goal (1 subgoal):
 1. 0 < remaining_steps ((step ^^ 4) (States direction.Left big (Small.push x small)))
[PROOF STEP]
using invar remaining_steps_n_steps_sub[of ?states 4]
[PROOF STATE]
proof (prove)
using this:
4 < remaining_steps (States direction.Left big (Small.push x small))
invar (States direction.Left big (Small.push x small))
invar (States direction.Left big (Small.push x small)) \<Longrightarrow> remaining_steps ((step ^^ 4) (States direction.Left big (Small.push x small))) = remaining_steps (States direction.Left big (Small.push x small)) - 4

goal (1 subgoal):
 1. 0 < remaining_steps ((step ^^ 4) (States direction.Left big (Small.push x small)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < remaining_steps ((step ^^ 4) (States direction.Left big (Small.push x small)))

goal (2 subgoals):
 1. 4 < remaining_steps (States direction.Left big (Small.push x small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
 2. \<not> 4 < remaining_steps (States direction.Left big (Small.push x small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
[PROOF STEP]
from True 6(1)
[PROOF STATE]
proof (chain)
picking this:
4 < remaining_steps (States direction.Left big (Small.push x small))
invar (Transforming (States direction.Left big small))
[PROOF STEP]
have size_ok: "size_ok ?states_stepped"
[PROOF STATE]
proof (prove)
using this:
4 < remaining_steps (States direction.Left big (Small.push x small))
invar (Transforming (States direction.Left big small))

goal (1 subgoal):
 1. size_ok ((step ^^ 4) (States direction.Left big (Small.push x small)))
[PROOF STEP]
using
          step_4_push_small_size_ok[of Left big small x]
          remaining_steps_push_small[of Left big small x]
[PROOF STATE]
proof (prove)
using this:
4 < remaining_steps (States direction.Left big (Small.push x small))
invar (Transforming (States direction.Left big small))
\<lbrakk>invar (States direction.Left big small); 4 \<le> remaining_steps (States direction.Left big small); size_ok (States direction.Left big small)\<rbrakk> \<Longrightarrow> size_ok ((step ^^ 4) (States direction.Left big (Small.push x small)))
invar (States direction.Left big small) \<Longrightarrow> remaining_steps (States direction.Left big small) = remaining_steps (States direction.Left big (Small.push x small))

goal (1 subgoal):
 1. size_ok ((step ^^ 4) (States direction.Left big (Small.push x small)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
size_ok ((step ^^ 4) (States direction.Left big (Small.push x small)))

goal (2 subgoals):
 1. 4 < remaining_steps (States direction.Left big (Small.push x small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
 2. \<not> 4 < remaining_steps (States direction.Left big (Small.push x small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
[PROOF STEP]
from remaining_steps size_ok invar_stepped
[PROOF STATE]
proof (chain)
picking this:
0 < remaining_steps ((step ^^ 4) (States direction.Left big (Small.push x small)))
size_ok ((step ^^ 4) (States direction.Left big (Small.push x small)))
invar ((step ^^ 4) (States direction.Left big (Small.push x small)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < remaining_steps ((step ^^ 4) (States direction.Left big (Small.push x small)))
size_ok ((step ^^ 4) (States direction.Left big (Small.push x small)))
invar ((step ^^ 4) (States direction.Left big (Small.push x small)))

goal (1 subgoal):
 1. invar (enqL x (Transforming (States direction.Left big small)))
[PROOF STEP]
by(cases big_stepped; cases small_stepped)
         (auto simp: Let_def split!: Common.state.split)
[PROOF STATE]
proof (state)
this:
invar (enqL x (Transforming (States direction.Left big small)))

goal (1 subgoal):
 1. \<not> 4 < remaining_steps (States direction.Left big (Small.push x small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 4 < remaining_steps (States direction.Left big (Small.push x small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 4 < remaining_steps (States direction.Left big (Small.push x small))

goal (1 subgoal):
 1. \<not> 4 < remaining_steps (States direction.Left big (Small.push x small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> 4 < remaining_steps (States direction.Left big (Small.push x small))
[PROOF STEP]
have remaining_steps_stepped: "remaining_steps ?states_stepped = 0"
[PROOF STATE]
proof (prove)
using this:
\<not> 4 < remaining_steps (States direction.Left big (Small.push x small))

goal (1 subgoal):
 1. remaining_steps ((step ^^ 4) (States direction.Left big (Small.push x small))) = 0
[PROOF STEP]
using invar
[PROOF STATE]
proof (prove)
using this:
\<not> 4 < remaining_steps (States direction.Left big (Small.push x small))
invar (States direction.Left big (Small.push x small))

goal (1 subgoal):
 1. remaining_steps ((step ^^ 4) (States direction.Left big (Small.push x small))) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
remaining_steps ((step ^^ 4) (States direction.Left big (Small.push x small))) = 0

goal (1 subgoal):
 1. \<not> 4 < remaining_steps (States direction.Left big (Small.push x small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
remaining_steps ((step ^^ 4) (States direction.Left big (Small.push x small))) = 0
[PROOF STEP]
obtain small_current small_idle big_current big_idle where idle [simp]: "
      ?states_stepped =
      States Left
          (Big.state.Common (state.Idle big_current big_idle))
          (Small.state.Common (state.Idle small_current small_idle))
      "
[PROOF STATE]
proof (prove)
using this:
remaining_steps ((step ^^ 4) (States direction.Left big (Small.push x small))) = 0

goal (1 subgoal):
 1. (\<And>big_current big_idle small_current small_idle. (step ^^ 4) (States direction.Left big (Small.push x small)) = States direction.Left (Big.state.Common (state.Idle big_current big_idle)) (Small.state.Common (state.Idle small_current small_idle)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using remaining_steps_idle' invar_stepped remaining_steps_stepped step_n_same
[PROOF STATE]
proof (prove)
using this:
remaining_steps ((step ^^ 4) (States direction.Left big (Small.push x small))) = 0
\<lbrakk>invar (States ?dir ?big ?small); remaining_steps (States ?dir ?big ?small) = 0\<rbrakk> \<Longrightarrow> \<exists>big_current big_idle small_current small_idle. States ?dir ?big ?small = States ?dir (Big.state.Common (state.Idle big_current big_idle)) (Small.state.Common (state.Idle small_current small_idle))
invar ((step ^^ 4) (States direction.Left big (Small.push x small)))
remaining_steps ((step ^^ 4) (States direction.Left big (Small.push x small))) = 0
(step ^^ ?n) (States ?dir ?big ?small) = States ?dir' ?big' ?small' \<Longrightarrow> ?dir = ?dir'

goal (1 subgoal):
 1. (\<And>big_current big_idle small_current small_idle. (step ^^ 4) (States direction.Left big (Small.push x small)) = States direction.Left (Big.state.Common (state.Idle big_current big_idle)) (Small.state.Common (state.Idle small_current small_idle)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (smt (verit) invar_states.elims(2))
[PROOF STATE]
proof (state)
this:
(step ^^ 4) (States direction.Left big (Small.push x small)) = States direction.Left (Big.state.Common (state.Idle big_current big_idle)) (Small.state.Common (state.Idle small_current small_idle))

goal (1 subgoal):
 1. \<not> 4 < remaining_steps (States direction.Left big (Small.push x small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
[PROOF STEP]
from 6
[PROOF STATE]
proof (chain)
picking this:
invar (Transforming (States direction.Left big small))
[PROOF STEP]
have [simp]: "size_new (Small.push x small) = Suc (size_new small)"
[PROOF STATE]
proof (prove)
using this:
invar (Transforming (States direction.Left big small))

goal (1 subgoal):
 1. size_new (Small.push x small) = Suc (size_new small)
[PROOF STEP]
using Small_Proof.size_new_push
[PROOF STATE]
proof (prove)
using this:
invar (Transforming (States direction.Left big small))
invar ?small \<Longrightarrow> size_new (Small.push ?x ?small) = Suc (size_new ?small)

goal (1 subgoal):
 1. size_new (Small.push x small) = Suc (size_new small)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
size_new (Small.push x small) = Suc (size_new small)

goal (1 subgoal):
 1. \<not> 4 < remaining_steps (States direction.Left big (Small.push x small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
[PROOF STEP]
have [simp]: "size small_idle = size_new (Small.push x small)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size small_idle = size_new (Small.push x small)
[PROOF STEP]
using invar invar_stepped step_n_size_new_small[of Left big "Small.push x small" 4]
[PROOF STATE]
proof (prove)
using this:
invar (States direction.Left big (Small.push x small))
invar ((step ^^ 4) (States direction.Left big (Small.push x small)))
\<lbrakk>invar (States direction.Left big (Small.push x small)); (step ^^ 4) (States direction.Left big (Small.push x small)) = States ?dir' ?big' ?small'\<rbrakk> \<Longrightarrow> size_new ?small' = size_new (Small.push x small)

goal (1 subgoal):
 1. size small_idle = size_new (Small.push x small)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
size small_idle = size_new (Small.push x small)

goal (1 subgoal):
 1. \<not> 4 < remaining_steps (States direction.Left big (Small.push x small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
size small_idle = size_new (Small.push x small)
[PROOF STEP]
have [simp]: "\<not>is_empty small_idle"
[PROOF STATE]
proof (prove)
using this:
size small_idle = size_new (Small.push x small)

goal (1 subgoal):
 1. \<not> is_empty small_idle
[PROOF STEP]
using Idle_Proof.size_not_empty[of small_idle]
[PROOF STATE]
proof (prove)
using this:
size small_idle = size_new (Small.push x small)
(0 < size small_idle) = (\<not> is_empty small_idle)

goal (1 subgoal):
 1. \<not> is_empty small_idle
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> is_empty small_idle

goal (1 subgoal):
 1. \<not> 4 < remaining_steps (States direction.Left big (Small.push x small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
[PROOF STEP]
have size_new_big [simp]: "0 < size_new big"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < size_new big
[PROOF STEP]
using 6
[PROOF STATE]
proof (prove)
using this:
invar (Transforming (States direction.Left big small))

goal (1 subgoal):
 1. 0 < size_new big
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < size_new big

goal (1 subgoal):
 1. \<not> 4 < remaining_steps (States direction.Left big (Small.push x small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < size_new big
[PROOF STEP]
have [simp]: "size big_idle = size_new big"
[PROOF STATE]
proof (prove)
using this:
0 < size_new big

goal (1 subgoal):
 1. size big_idle = size_new big
[PROOF STEP]
using invar invar_stepped step_n_size_new_big[of Left big "Small.push x small" 4]
[PROOF STATE]
proof (prove)
using this:
0 < size_new big
invar (States direction.Left big (Small.push x small))
invar ((step ^^ 4) (States direction.Left big (Small.push x small)))
\<lbrakk>invar (States direction.Left big (Small.push x small)); (step ^^ 4) (States direction.Left big (Small.push x small)) = States ?dir' ?big' ?small'\<rbrakk> \<Longrightarrow> size_new ?big' = size_new big

goal (1 subgoal):
 1. size big_idle = size_new big
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
size big_idle = size_new big

goal (1 subgoal):
 1. \<not> 4 < remaining_steps (States direction.Left big (Small.push x small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
size big_idle = size_new big
[PROOF STEP]
have [simp]: "\<not>is_empty big_idle"
[PROOF STATE]
proof (prove)
using this:
size big_idle = size_new big

goal (1 subgoal):
 1. \<not> is_empty big_idle
[PROOF STEP]
using Idle_Proof.size_not_empty size_new_big
[PROOF STATE]
proof (prove)
using this:
size big_idle = size_new big
(0 < size ?idle) = (\<not> is_empty ?idle)
0 < size_new big

goal (1 subgoal):
 1. \<not> is_empty big_idle
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<not> is_empty big_idle

goal (1 subgoal):
 1. \<not> 4 < remaining_steps (States direction.Left big (Small.push x small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
[PROOF STEP]
have size_ok_1: "size small_idle \<le> 3 * size big_idle"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size small_idle \<le> 3 * size big_idle
[PROOF STEP]
using 6
[PROOF STATE]
proof (prove)
using this:
invar (Transforming (States direction.Left big small))

goal (1 subgoal):
 1. size small_idle \<le> 3 * size big_idle
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
size small_idle \<le> 3 * size big_idle

goal (1 subgoal):
 1. \<not> 4 < remaining_steps (States direction.Left big (Small.push x small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
[PROOF STEP]
have size_ok_2: "size big_idle \<le> 3 * size small_idle"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size big_idle \<le> 3 * size small_idle
[PROOF STEP]
using 6
[PROOF STATE]
proof (prove)
using this:
invar (Transforming (States direction.Left big small))

goal (1 subgoal):
 1. size big_idle \<le> 3 * size small_idle
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
size big_idle \<le> 3 * size small_idle

goal (1 subgoal):
 1. \<not> 4 < remaining_steps (States direction.Left big (Small.push x small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Left big small)))
[PROOF STEP]
from False
[PROOF STATE]
proof (chain)
picking this:
\<not> 4 < remaining_steps (States direction.Left big (Small.push x small))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> 4 < remaining_steps (States direction.Left big (Small.push x small))

goal (1 subgoal):
 1. invar (enqL x (Transforming (States direction.Left big small)))
[PROOF STEP]
using invar_stepped size_ok_1 size_ok_2
[PROOF STATE]
proof (prove)
using this:
\<not> 4 < remaining_steps (States direction.Left big (Small.push x small))
invar ((step ^^ 4) (States direction.Left big (Small.push x small)))
size small_idle \<le> 3 * size big_idle
size big_idle \<le> 3 * size small_idle

goal (1 subgoal):
 1. invar (enqL x (Transforming (States direction.Left big small)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invar (enqL x (Transforming (States direction.Left big small)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
invar (enqL x (Transforming (States direction.Left big small)))

goal (5 subgoals):
 1. \<And>x. invar Empty \<Longrightarrow> invar (enqL x Empty)
 2. \<And>x y. invar (One y) \<Longrightarrow> invar (enqL x (One y))
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> invar (enqL x (Two y z))
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> invar (enqL x (Three a b c))
 5. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x. invar Empty \<Longrightarrow> invar (enqL x Empty)
 2. \<And>x y. invar (One y) \<Longrightarrow> invar (enqL x (One y))
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> invar (enqL x (Two y z))
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> invar (enqL x (Three a b c))
 5. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
case (7 x big small)
[PROOF STATE]
proof (state)
this:
invar (Transforming (States direction.Right big small))

goal (5 subgoals):
 1. \<And>x. invar Empty \<Longrightarrow> invar (enqL x Empty)
 2. \<And>x y. invar (One y) \<Longrightarrow> invar (enqL x (One y))
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> invar (enqL x (Two y z))
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> invar (enqL x (Three a b c))
 5. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
let ?big = "Big.push x big"
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x. invar Empty \<Longrightarrow> invar (enqL x Empty)
 2. \<And>x y. invar (One y) \<Longrightarrow> invar (enqL x (One y))
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> invar (enqL x (Two y z))
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> invar (enqL x (Three a b c))
 5. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
let ?states = "States Right ?big small"
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x. invar Empty \<Longrightarrow> invar (enqL x Empty)
 2. \<And>x y. invar (One y) \<Longrightarrow> invar (enqL x (One y))
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> invar (enqL x (Two y z))
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> invar (enqL x (Three a b c))
 5. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
let ?states_stepped = "(step^^4) ?states"
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x. invar Empty \<Longrightarrow> invar (enqL x Empty)
 2. \<And>x y. invar (One y) \<Longrightarrow> invar (enqL x (One y))
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> invar (enqL x (Two y z))
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> invar (enqL x (Three a b c))
 5. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
from 7
[PROOF STATE]
proof (chain)
picking this:
invar (Transforming (States direction.Right big small))
[PROOF STEP]
have invar: "invar ?states"
[PROOF STATE]
proof (prove)
using this:
invar (Transforming (States direction.Right big small))

goal (1 subgoal):
 1. invar (States direction.Right (Big.push x big) small)
[PROOF STEP]
using invar_push_big[of Right big small x]
[PROOF STATE]
proof (prove)
using this:
invar (Transforming (States direction.Right big small))
invar (States direction.Right big small) \<Longrightarrow> invar (States direction.Right (Big.push x big) small)

goal (1 subgoal):
 1. invar (States direction.Right (Big.push x big) small)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invar (States direction.Right (Big.push x big) small)

goal (5 subgoals):
 1. \<And>x. invar Empty \<Longrightarrow> invar (enqL x Empty)
 2. \<And>x y. invar (One y) \<Longrightarrow> invar (enqL x (One y))
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> invar (enqL x (Two y z))
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> invar (enqL x (Three a b c))
 5. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (States direction.Right (Big.push x big) small)
[PROOF STEP]
have invar_stepped: "invar ?states_stepped"
[PROOF STATE]
proof (prove)
using this:
invar (States direction.Right (Big.push x big) small)

goal (1 subgoal):
 1. invar ((step ^^ 4) (States direction.Right (Big.push x big) small))
[PROOF STEP]
using invar_step_n
[PROOF STATE]
proof (prove)
using this:
invar (States direction.Right (Big.push x big) small)
invar ?states \<Longrightarrow> invar ((step ^^ ?n) ?states)

goal (1 subgoal):
 1. invar ((step ^^ 4) (States direction.Right (Big.push x big) small))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
invar ((step ^^ 4) (States direction.Right (Big.push x big) small))

goal (5 subgoals):
 1. \<And>x. invar Empty \<Longrightarrow> invar (enqL x Empty)
 2. \<And>x y. invar (One y) \<Longrightarrow> invar (enqL x (One y))
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> invar (enqL x (Two y z))
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> invar (enqL x (Three a b c))
 5. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
proof(cases "4 < remaining_steps ?states")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 4 < remaining_steps (States direction.Right (Big.push x big) small) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
 2. \<not> 4 < remaining_steps (States direction.Right (Big.push x big) small) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
4 < remaining_steps (States direction.Right (Big.push x big) small)

goal (2 subgoals):
 1. 4 < remaining_steps (States direction.Right (Big.push x big) small) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
 2. \<not> 4 < remaining_steps (States direction.Right (Big.push x big) small) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
obtain big_stepped small_stepped where stepped [simp]:
       "?states_stepped = States Right big_stepped small_stepped"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>big_stepped small_stepped. (step ^^ 4) (States direction.Right (Big.push x big) small) = States direction.Right big_stepped small_stepped \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis remaining_steps_states.cases step_n_same)
[PROOF STATE]
proof (state)
this:
(step ^^ 4) (States direction.Right (Big.push x big) small) = States direction.Right big_stepped small_stepped

goal (2 subgoals):
 1. 4 < remaining_steps (States direction.Right (Big.push x big) small) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
 2. \<not> 4 < remaining_steps (States direction.Right (Big.push x big) small) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
from True
[PROOF STATE]
proof (chain)
picking this:
4 < remaining_steps (States direction.Right (Big.push x big) small)
[PROOF STEP]
have remaining_steps: "0 < remaining_steps ?states_stepped"
[PROOF STATE]
proof (prove)
using this:
4 < remaining_steps (States direction.Right (Big.push x big) small)

goal (1 subgoal):
 1. 0 < remaining_steps ((step ^^ 4) (States direction.Right (Big.push x big) small))
[PROOF STEP]
using invar remaining_steps_n_steps_sub[of ?states 4]
[PROOF STATE]
proof (prove)
using this:
4 < remaining_steps (States direction.Right (Big.push x big) small)
invar (States direction.Right (Big.push x big) small)
invar (States direction.Right (Big.push x big) small) \<Longrightarrow> remaining_steps ((step ^^ 4) (States direction.Right (Big.push x big) small)) = remaining_steps (States direction.Right (Big.push x big) small) - 4

goal (1 subgoal):
 1. 0 < remaining_steps ((step ^^ 4) (States direction.Right (Big.push x big) small))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < remaining_steps ((step ^^ 4) (States direction.Right (Big.push x big) small))

goal (2 subgoals):
 1. 4 < remaining_steps (States direction.Right (Big.push x big) small) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
 2. \<not> 4 < remaining_steps (States direction.Right (Big.push x big) small) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
from True 7(1)
[PROOF STATE]
proof (chain)
picking this:
4 < remaining_steps (States direction.Right (Big.push x big) small)
invar (Transforming (States direction.Right big small))
[PROOF STEP]
have size_ok: "size_ok ?states_stepped"
[PROOF STATE]
proof (prove)
using this:
4 < remaining_steps (States direction.Right (Big.push x big) small)
invar (Transforming (States direction.Right big small))

goal (1 subgoal):
 1. size_ok ((step ^^ 4) (States direction.Right (Big.push x big) small))
[PROOF STEP]
using
          step_4_push_big_size_ok[of Right big small x]
          remaining_steps_push_big[of Right big small x]
[PROOF STATE]
proof (prove)
using this:
4 < remaining_steps (States direction.Right (Big.push x big) small)
invar (Transforming (States direction.Right big small))
\<lbrakk>invar (States direction.Right big small); 4 \<le> remaining_steps (States direction.Right big small); size_ok (States direction.Right big small)\<rbrakk> \<Longrightarrow> size_ok ((step ^^ 4) (States direction.Right (Big.push x big) small))
invar (States direction.Right big small) \<Longrightarrow> remaining_steps (States direction.Right (Big.push x big) small) = remaining_steps (States direction.Right big small)

goal (1 subgoal):
 1. size_ok ((step ^^ 4) (States direction.Right (Big.push x big) small))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
size_ok ((step ^^ 4) (States direction.Right (Big.push x big) small))

goal (2 subgoals):
 1. 4 < remaining_steps (States direction.Right (Big.push x big) small) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
 2. \<not> 4 < remaining_steps (States direction.Right (Big.push x big) small) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
from remaining_steps size_ok invar_stepped
[PROOF STATE]
proof (chain)
picking this:
0 < remaining_steps ((step ^^ 4) (States direction.Right (Big.push x big) small))
size_ok ((step ^^ 4) (States direction.Right (Big.push x big) small))
invar ((step ^^ 4) (States direction.Right (Big.push x big) small))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < remaining_steps ((step ^^ 4) (States direction.Right (Big.push x big) small))
size_ok ((step ^^ 4) (States direction.Right (Big.push x big) small))
invar ((step ^^ 4) (States direction.Right (Big.push x big) small))

goal (1 subgoal):
 1. invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
by(cases big_stepped; cases small_stepped)
         (auto simp: Let_def split!: Common.state.split)
[PROOF STATE]
proof (state)
this:
invar (enqL x (Transforming (States direction.Right big small)))

goal (1 subgoal):
 1. \<not> 4 < remaining_steps (States direction.Right (Big.push x big) small) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 4 < remaining_steps (States direction.Right (Big.push x big) small) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 4 < remaining_steps (States direction.Right (Big.push x big) small)

goal (1 subgoal):
 1. \<not> 4 < remaining_steps (States direction.Right (Big.push x big) small) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> 4 < remaining_steps (States direction.Right (Big.push x big) small)
[PROOF STEP]
have remaining_steps_stepped: "remaining_steps ?states_stepped = 0"
[PROOF STATE]
proof (prove)
using this:
\<not> 4 < remaining_steps (States direction.Right (Big.push x big) small)

goal (1 subgoal):
 1. remaining_steps ((step ^^ 4) (States direction.Right (Big.push x big) small)) = 0
[PROOF STEP]
using invar
[PROOF STATE]
proof (prove)
using this:
\<not> 4 < remaining_steps (States direction.Right (Big.push x big) small)
invar (States direction.Right (Big.push x big) small)

goal (1 subgoal):
 1. remaining_steps ((step ^^ 4) (States direction.Right (Big.push x big) small)) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
remaining_steps ((step ^^ 4) (States direction.Right (Big.push x big) small)) = 0

goal (1 subgoal):
 1. \<not> 4 < remaining_steps (States direction.Right (Big.push x big) small) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
remaining_steps ((step ^^ 4) (States direction.Right (Big.push x big) small)) = 0
[PROOF STEP]
obtain small_current small_idle big_current big_idle where idle [simp]: "
      ?states_stepped =
      States Right
          (Big.state.Common (state.Idle big_current big_idle))
          (Small.state.Common (state.Idle small_current small_idle))
      "
[PROOF STATE]
proof (prove)
using this:
remaining_steps ((step ^^ 4) (States direction.Right (Big.push x big) small)) = 0

goal (1 subgoal):
 1. (\<And>big_current big_idle small_current small_idle. (step ^^ 4) (States direction.Right (Big.push x big) small) = States direction.Right (Big.state.Common (state.Idle big_current big_idle)) (Small.state.Common (state.Idle small_current small_idle)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using remaining_steps_idle' invar_stepped remaining_steps_stepped step_n_same
[PROOF STATE]
proof (prove)
using this:
remaining_steps ((step ^^ 4) (States direction.Right (Big.push x big) small)) = 0
\<lbrakk>invar (States ?dir ?big ?small); remaining_steps (States ?dir ?big ?small) = 0\<rbrakk> \<Longrightarrow> \<exists>big_current big_idle small_current small_idle. States ?dir ?big ?small = States ?dir (Big.state.Common (state.Idle big_current big_idle)) (Small.state.Common (state.Idle small_current small_idle))
invar ((step ^^ 4) (States direction.Right (Big.push x big) small))
remaining_steps ((step ^^ 4) (States direction.Right (Big.push x big) small)) = 0
(step ^^ ?n) (States ?dir ?big ?small) = States ?dir' ?big' ?small' \<Longrightarrow> ?dir = ?dir'

goal (1 subgoal):
 1. (\<And>big_current big_idle small_current small_idle. (step ^^ 4) (States direction.Right (Big.push x big) small) = States direction.Right (Big.state.Common (state.Idle big_current big_idle)) (Small.state.Common (state.Idle small_current small_idle)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (smt (verit) invar_states.elims(2))
[PROOF STATE]
proof (state)
this:
(step ^^ 4) (States direction.Right (Big.push x big) small) = States direction.Right (Big.state.Common (state.Idle big_current big_idle)) (Small.state.Common (state.Idle small_current small_idle))

goal (1 subgoal):
 1. \<not> 4 < remaining_steps (States direction.Right (Big.push x big) small) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
from 7
[PROOF STATE]
proof (chain)
picking this:
invar (Transforming (States direction.Right big small))
[PROOF STEP]
have [simp]: "size_new (Big.push x big) = Suc (size_new big)"
[PROOF STATE]
proof (prove)
using this:
invar (Transforming (States direction.Right big small))

goal (1 subgoal):
 1. size_new (Big.push x big) = Suc (size_new big)
[PROOF STEP]
using Big_Proof.size_new_push
[PROOF STATE]
proof (prove)
using this:
invar (Transforming (States direction.Right big small))
invar ?big \<Longrightarrow> size_new (Big.push ?x ?big) = Suc (size_new ?big)

goal (1 subgoal):
 1. size_new (Big.push x big) = Suc (size_new big)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
size_new (Big.push x big) = Suc (size_new big)

goal (1 subgoal):
 1. \<not> 4 < remaining_steps (States direction.Right (Big.push x big) small) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
have [simp]: "size big_idle = size_new (Big.push x big)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size big_idle = size_new (Big.push x big)
[PROOF STEP]
using invar invar_stepped step_n_size_new_big[of Right "Big.push x big" small 4]
[PROOF STATE]
proof (prove)
using this:
invar (States direction.Right (Big.push x big) small)
invar ((step ^^ 4) (States direction.Right (Big.push x big) small))
\<lbrakk>invar (States direction.Right (Big.push x big) small); (step ^^ 4) (States direction.Right (Big.push x big) small) = States ?dir' ?big' ?small'\<rbrakk> \<Longrightarrow> size_new ?big' = size_new (Big.push x big)

goal (1 subgoal):
 1. size big_idle = size_new (Big.push x big)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
size big_idle = size_new (Big.push x big)

goal (1 subgoal):
 1. \<not> 4 < remaining_steps (States direction.Right (Big.push x big) small) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
size big_idle = size_new (Big.push x big)
[PROOF STEP]
have [simp]: "\<not>is_empty big_idle"
[PROOF STATE]
proof (prove)
using this:
size big_idle = size_new (Big.push x big)

goal (1 subgoal):
 1. \<not> is_empty big_idle
[PROOF STEP]
using Idle_Proof.size_not_empty[of big_idle]
[PROOF STATE]
proof (prove)
using this:
size big_idle = size_new (Big.push x big)
(0 < size big_idle) = (\<not> is_empty big_idle)

goal (1 subgoal):
 1. \<not> is_empty big_idle
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> is_empty big_idle

goal (1 subgoal):
 1. \<not> 4 < remaining_steps (States direction.Right (Big.push x big) small) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
have size_new_small [simp]: "0 < size_new small"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < size_new small
[PROOF STEP]
using 7
[PROOF STATE]
proof (prove)
using this:
invar (Transforming (States direction.Right big small))

goal (1 subgoal):
 1. 0 < size_new small
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < size_new small

goal (1 subgoal):
 1. \<not> 4 < remaining_steps (States direction.Right (Big.push x big) small) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < size_new small
[PROOF STEP]
have [simp]: "size small_idle = size_new small"
[PROOF STATE]
proof (prove)
using this:
0 < size_new small

goal (1 subgoal):
 1. size small_idle = size_new small
[PROOF STEP]
using invar invar_stepped step_n_size_new_small[of Right "Big.push x big" small 4]
[PROOF STATE]
proof (prove)
using this:
0 < size_new small
invar (States direction.Right (Big.push x big) small)
invar ((step ^^ 4) (States direction.Right (Big.push x big) small))
\<lbrakk>invar (States direction.Right (Big.push x big) small); (step ^^ 4) (States direction.Right (Big.push x big) small) = States ?dir' ?big' ?small'\<rbrakk> \<Longrightarrow> size_new ?small' = size_new small

goal (1 subgoal):
 1. size small_idle = size_new small
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
size small_idle = size_new small

goal (1 subgoal):
 1. \<not> 4 < remaining_steps (States direction.Right (Big.push x big) small) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
size small_idle = size_new small
[PROOF STEP]
have [simp]: "\<not>is_empty small_idle"
[PROOF STATE]
proof (prove)
using this:
size small_idle = size_new small

goal (1 subgoal):
 1. \<not> is_empty small_idle
[PROOF STEP]
using Idle_Proof.size_not_empty size_new_small
[PROOF STATE]
proof (prove)
using this:
size small_idle = size_new small
(0 < size ?idle) = (\<not> is_empty ?idle)
0 < size_new small

goal (1 subgoal):
 1. \<not> is_empty small_idle
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<not> is_empty small_idle

goal (1 subgoal):
 1. \<not> 4 < remaining_steps (States direction.Right (Big.push x big) small) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
have size_ok_1: "size small_idle \<le> 3 * size big_idle"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size small_idle \<le> 3 * size big_idle
[PROOF STEP]
using 7
[PROOF STATE]
proof (prove)
using this:
invar (Transforming (States direction.Right big small))

goal (1 subgoal):
 1. size small_idle \<le> 3 * size big_idle
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
size small_idle \<le> 3 * size big_idle

goal (1 subgoal):
 1. \<not> 4 < remaining_steps (States direction.Right (Big.push x big) small) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
have size_ok_2: "size big_idle \<le> 3 * size small_idle"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size big_idle \<le> 3 * size small_idle
[PROOF STEP]
using 7
[PROOF STATE]
proof (prove)
using this:
invar (Transforming (States direction.Right big small))

goal (1 subgoal):
 1. size big_idle \<le> 3 * size small_idle
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
size big_idle \<le> 3 * size small_idle

goal (1 subgoal):
 1. \<not> 4 < remaining_steps (States direction.Right (Big.push x big) small) \<Longrightarrow> invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
from False
[PROOF STATE]
proof (chain)
picking this:
\<not> 4 < remaining_steps (States direction.Right (Big.push x big) small)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> 4 < remaining_steps (States direction.Right (Big.push x big) small)

goal (1 subgoal):
 1. invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
using invar_stepped size_ok_1 size_ok_2
[PROOF STATE]
proof (prove)
using this:
\<not> 4 < remaining_steps (States direction.Right (Big.push x big) small)
invar ((step ^^ 4) (States direction.Right (Big.push x big) small))
size small_idle \<le> 3 * size big_idle
size big_idle \<le> 3 * size small_idle

goal (1 subgoal):
 1. invar (enqL x (Transforming (States direction.Right big small)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invar (enqL x (Transforming (States direction.Right big small)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
invar (enqL x (Transforming (States direction.Right big small)))

goal (4 subgoals):
 1. \<And>x. invar Empty \<Longrightarrow> invar (enqL x Empty)
 2. \<And>x y. invar (One y) \<Longrightarrow> invar (enqL x (One y))
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> invar (enqL x (Two y z))
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> invar (enqL x (Three a b c))
[PROOF STEP]
qed auto


[STATEMENT]
lemma reach_PublicV_imples_FriendV[simp]:
assumes "reach s"
and "vis s pID \<noteq> PublicV"
shows "vis s pID = FriendV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vis s pID = FriendV
[PROOF STEP]
using assms reach_vis
[PROOF STATE]
proof (prove)
using this:
reach s
vis s pID \<noteq> PublicV
reach ?s \<Longrightarrow> vis ?s ?pID \<in> {FriendV, PublicV}

goal (1 subgoal):
 1. vis s pID = FriendV
[PROOF STEP]
by auto


[STATEMENT]
lemma reachNT_state:
assumes "reachNT s"
shows "\<not> (\<exists> uid \<in> UIDs.
   uid \<in>\<in> userIDs s \<and> PID \<in>\<in> postIDs s \<and>
   (uid = admin s \<or> uid = owner s PID \<or> uid \<in>\<in> friendIDs s (owner s PID) \<or>
    vis s PID = PublicV))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<exists>uid\<in>UIDs. uid \<in>\<in> userIDs s \<and> PID \<in>\<in> postIDs s \<and> (uid = admin s \<or> uid = owner s PID \<or> uid \<in>\<in> friendIDs s (owner s PID) \<or> vis s PID = PublicV))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
reachNT s

goal (1 subgoal):
 1. \<not> (\<exists>uid\<in>UIDs. uid \<in>\<in> userIDs s \<and> PID \<in>\<in> postIDs s \<and> (uid = admin s \<or> uid = owner s PID \<or> uid \<in>\<in> friendIDs s (owner s PID) \<or> vis s PID = PublicV))
[PROOF STEP]
proof induct
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> (\<exists>uid\<in>UIDs. uid \<in>\<in> userIDs istate \<and> PID \<in>\<in> postIDs istate \<and> (uid = admin istate \<or> uid = owner istate PID \<or> uid \<in>\<in> friendIDs istate (owner istate PID) \<or> vis istate PID = PublicV))
 2. \<And>trn. \<lbrakk>reachNT (srcOf trn); \<not> (\<exists>uid\<in>UIDs. uid \<in>\<in> userIDs (srcOf trn) \<and> PID \<in>\<in> postIDs (srcOf trn) \<and> (uid = admin (srcOf trn) \<or> uid = owner (srcOf trn) PID \<or> uid \<in>\<in> friendIDs (srcOf trn) (owner (srcOf trn) PID) \<or> vis (srcOf trn) PID = PublicV)); validTrans trn; \<not> T trn\<rbrakk> \<Longrightarrow> \<not> (\<exists>uid\<in>UIDs. uid \<in>\<in> userIDs (tgtOf trn) \<and> PID \<in>\<in> postIDs (tgtOf trn) \<and> (uid = admin (tgtOf trn) \<or> uid = owner (tgtOf trn) PID \<or> uid \<in>\<in> friendIDs (tgtOf trn) (owner (tgtOf trn) PID) \<or> vis (tgtOf trn) PID = PublicV))
[PROOF STEP]
case (Step trn)
[PROOF STATE]
proof (state)
this:
reachNT (srcOf trn)
\<not> (\<exists>uid\<in>UIDs. uid \<in>\<in> userIDs (srcOf trn) \<and> PID \<in>\<in> postIDs (srcOf trn) \<and> (uid = admin (srcOf trn) \<or> uid = owner (srcOf trn) PID \<or> uid \<in>\<in> friendIDs (srcOf trn) (owner (srcOf trn) PID) \<or> vis (srcOf trn) PID = PublicV))
validTrans trn
\<not> T trn

goal (2 subgoals):
 1. \<not> (\<exists>uid\<in>UIDs. uid \<in>\<in> userIDs istate \<and> PID \<in>\<in> postIDs istate \<and> (uid = admin istate \<or> uid = owner istate PID \<or> uid \<in>\<in> friendIDs istate (owner istate PID) \<or> vis istate PID = PublicV))
 2. \<And>trn. \<lbrakk>reachNT (srcOf trn); \<not> (\<exists>uid\<in>UIDs. uid \<in>\<in> userIDs (srcOf trn) \<and> PID \<in>\<in> postIDs (srcOf trn) \<and> (uid = admin (srcOf trn) \<or> uid = owner (srcOf trn) PID \<or> uid \<in>\<in> friendIDs (srcOf trn) (owner (srcOf trn) PID) \<or> vis (srcOf trn) PID = PublicV)); validTrans trn; \<not> T trn\<rbrakk> \<Longrightarrow> \<not> (\<exists>uid\<in>UIDs. uid \<in>\<in> userIDs (tgtOf trn) \<and> PID \<in>\<in> postIDs (tgtOf trn) \<and> (uid = admin (tgtOf trn) \<or> uid = owner (tgtOf trn) PID \<or> uid \<in>\<in> friendIDs (tgtOf trn) (owner (tgtOf trn) PID) \<or> vis (tgtOf trn) PID = PublicV))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
reachNT (srcOf trn)
\<not> (\<exists>uid\<in>UIDs. uid \<in>\<in> userIDs (srcOf trn) \<and> PID \<in>\<in> postIDs (srcOf trn) \<and> (uid = admin (srcOf trn) \<or> uid = owner (srcOf trn) PID \<or> uid \<in>\<in> friendIDs (srcOf trn) (owner (srcOf trn) PID) \<or> vis (srcOf trn) PID = PublicV))
validTrans trn
\<not> T trn

goal (1 subgoal):
 1. \<not> (\<exists>uid\<in>UIDs. uid \<in>\<in> userIDs (tgtOf trn) \<and> PID \<in>\<in> postIDs (tgtOf trn) \<and> (uid = admin (tgtOf trn) \<or> uid = owner (tgtOf trn) PID \<or> uid \<in>\<in> friendIDs (tgtOf trn) (owner (tgtOf trn) PID) \<or> vis (tgtOf trn) PID = PublicV))
[PROOF STEP]
by (cases trn) auto
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>uid\<in>UIDs. uid \<in>\<in> userIDs (tgtOf trn) \<and> PID \<in>\<in> postIDs (tgtOf trn) \<and> (uid = admin (tgtOf trn) \<or> uid = owner (tgtOf trn) PID \<or> uid \<in>\<in> friendIDs (tgtOf trn) (owner (tgtOf trn) PID) \<or> vis (tgtOf trn) PID = PublicV))

goal (1 subgoal):
 1. \<not> (\<exists>uid\<in>UIDs. uid \<in>\<in> userIDs istate \<and> PID \<in>\<in> postIDs istate \<and> (uid = admin istate \<or> uid = owner istate PID \<or> uid \<in>\<in> friendIDs istate (owner istate PID) \<or> vis istate PID = PublicV))
[PROOF STEP]
qed (simp add: istate_def)


[STATEMENT]
lemma T_\<phi>_\<gamma>:
assumes 1: "reachNT s" and 2: "step s a = (ou,s')"
and 3: "\<phi> (Trans s a ou s')" and
(* note that now we have some overlap between \<phi> and \<gamma>, even for reachNT: *)
4: "\<forall> ca. a \<noteq> COMact ca"
shows "\<not> \<gamma> (Trans s a ou s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> \<gamma> (Trans s a ou s')
[PROOF STEP]
using reachNT_state[OF 1] 2 3 4
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>uid\<in>UIDs. uid \<in>\<in> userIDs s \<and> PID \<in>\<in> postIDs s \<and> (uid = admin s \<or> uid = owner s PID \<or> uid \<in>\<in> friendIDs s (owner s PID) \<or> vis s PID = PublicV))
step s a = (ou, s')
\<phi> (Trans s a ou s')
\<forall>ca. a \<noteq> COMact ca

goal (1 subgoal):
 1. \<not> \<gamma> (Trans s a ou s')
[PROOF STEP]
using \<phi>_def2
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>uid\<in>UIDs. uid \<in>\<in> userIDs s \<and> PID \<in>\<in> postIDs s \<and> (uid = admin s \<or> uid = owner s PID \<or> uid \<in>\<in> friendIDs s (owner s PID) \<or> vis s PID = PublicV))
step s a = (ou, s')
\<phi> (Trans s a ou s')
\<forall>ca. a \<noteq> COMact ca
\<phi> (Trans ?s ?a ?ou ?s') = ((\<exists>uid p pst. ?a = Uact (uPost uid p PID pst) \<and> ?ou = outOK) \<or> (\<exists>uid p aid. ?a = COMact (comSendPost uid p aid PID) \<and> ?ou \<noteq> outErr))

goal (1 subgoal):
 1. \<not> \<gamma> (Trans s a ou s')
[PROOF STEP]
(* [OF 2] *)
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>uid\<in>UIDs. uid \<in>\<in> userIDs s \<and> PID \<in>\<in> postIDs s \<and> (uid = admin s \<or> uid = owner s PID \<or> uid \<in>\<in> friendIDs s (owner s PID) \<or> vis s PID = PublicV))
step s a = (ou, s')
\<phi> (Trans s a ou s')
\<forall>ca. a \<noteq> COMact ca
\<phi> (Trans ?s ?a ?ou ?s') = ((\<exists>uid p pst. ?a = Uact (uPost uid p PID pst) \<and> ?ou = outOK) \<or> (\<exists>uid p aid. ?a = COMact (comSendPost uid p aid PID) \<and> ?ou \<noteq> outErr))

goal (1 subgoal):
 1. \<not> \<gamma> (Trans s a ou s')
[PROOF STEP]
by (auto simp add: u_defs com_defs)