[STATEMENT]
lemma list_enqL: "invar deque \<Longrightarrow> listL (enqL x deque) = x # listL deque"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar deque \<Longrightarrow> RealTimeDeque.listL (enqL x deque) = x # RealTimeDeque.listL deque
[PROOF STEP]
proof(induction x deque rule: enqL.induct)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x. invar Empty \<Longrightarrow> RealTimeDeque.listL (enqL x Empty) = x # RealTimeDeque.listL Empty
 2. \<And>x y. invar (One y) \<Longrightarrow> RealTimeDeque.listL (enqL x (One y)) = x # RealTimeDeque.listL (One y)
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> RealTimeDeque.listL (enqL x (Two y z)) = x # RealTimeDeque.listL (Two y z)
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> RealTimeDeque.listL (enqL x (Three a b c)) = x # RealTimeDeque.listL (Three a b c)
 5. \<And>x left right length_right. invar (deque.Idle left (idle.Idle right length_right)) \<Longrightarrow> RealTimeDeque.listL (enqL x (deque.Idle left (idle.Idle right length_right))) = x # RealTimeDeque.listL (deque.Idle left (idle.Idle right length_right))
 6. \<And>x big small. invar (Transforming (States direction.Left big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Left big small))) = x # RealTimeDeque.listL (Transforming (States direction.Left big small))
 7. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Right big small))) = x # RealTimeDeque.listL (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> RealTimeDeque.listL (enqL x Empty) = x # RealTimeDeque.listL Empty
 2. \<And>x y. invar (One y) \<Longrightarrow> RealTimeDeque.listL (enqL x (One y)) = x # RealTimeDeque.listL (One y)
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> RealTimeDeque.listL (enqL x (Two y z)) = x # RealTimeDeque.listL (Two y z)
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> RealTimeDeque.listL (enqL x (Three a b c)) = x # RealTimeDeque.listL (Three a b c)
 5. \<And>x left right length_right. invar (deque.Idle left (idle.Idle right length_right)) \<Longrightarrow> RealTimeDeque.listL (enqL x (deque.Idle left (idle.Idle right length_right))) = x # RealTimeDeque.listL (deque.Idle left (idle.Idle right length_right))
 6. \<And>x big small. invar (Transforming (States direction.Left big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Left big small))) = x # RealTimeDeque.listL (Transforming (States direction.Left big small))
 7. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Right big small))) = x # RealTimeDeque.listL (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> RealTimeDeque.listL (enqL x Empty) = x # RealTimeDeque.listL Empty
 2. \<And>x y. invar (One y) \<Longrightarrow> RealTimeDeque.listL (enqL x (One y)) = x # RealTimeDeque.listL (One y)
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> RealTimeDeque.listL (enqL x (Two y z)) = x # RealTimeDeque.listL (Two y z)
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> RealTimeDeque.listL (enqL x (Three a b c)) = x # RealTimeDeque.listL (Three a b c)
 5. \<And>x left right length_right. invar (deque.Idle left (idle.Idle right length_right)) \<Longrightarrow> RealTimeDeque.listL (enqL x (deque.Idle left (idle.Idle right length_right))) = x # RealTimeDeque.listL (deque.Idle left (idle.Idle right length_right))
 6. \<And>x big small. invar (Transforming (States direction.Left big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Left big small))) = x # RealTimeDeque.listL (Transforming (States direction.Left big small))
 7. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Right big small))) = x # RealTimeDeque.listL (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> RealTimeDeque.listL (enqL x Empty) = x # RealTimeDeque.listL Empty
 2. \<And>x y. invar (One y) \<Longrightarrow> RealTimeDeque.listL (enqL x (One y)) = x # RealTimeDeque.listL (One y)
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> RealTimeDeque.listL (enqL x (Two y z)) = x # RealTimeDeque.listL (Two y z)
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> RealTimeDeque.listL (enqL x (Three a b c)) = x # RealTimeDeque.listL (Three a b c)
 5. \<And>x left right length_right. invar (deque.Idle left (idle.Idle right length_right)) \<Longrightarrow> RealTimeDeque.listL (enqL x (deque.Idle left (idle.Idle right length_right))) = x # RealTimeDeque.listL (deque.Idle left (idle.Idle right length_right))
 6. \<And>x big small. invar (Transforming (States direction.Left big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Left big small))) = x # RealTimeDeque.listL (Transforming (States direction.Left big small))
 7. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Right big small))) = x # RealTimeDeque.listL (Transforming (States direction.Right big small))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RealTimeDeque.listL (enqL x (deque.Idle left (idle.Idle right length_right))) = x # RealTimeDeque.listL (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> RealTimeDeque.listL (enqL x (deque.Idle left (idle.Idle right length_right))) = x # RealTimeDeque.listL (deque.Idle left (idle.Idle right length_right))
 2. \<not> length_left' \<le> 3 * length_right \<Longrightarrow> RealTimeDeque.listL (enqL x (deque.Idle left (idle.Idle right length_right))) = x # RealTimeDeque.listL (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> RealTimeDeque.listL (enqL x (deque.Idle left (idle.Idle right length_right))) = x # RealTimeDeque.listL (deque.Idle left (idle.Idle right length_right))
 2. \<not> length_left' \<le> 3 * length_right \<Longrightarrow> RealTimeDeque.listL (enqL x (deque.Idle left (idle.Idle right length_right))) = x # RealTimeDeque.listL (deque.Idle left (idle.Idle right length_right))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length_left' \<le> 3 * length_right
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length_left' \<le> 3 * length_right

goal (1 subgoal):
 1. RealTimeDeque.listL (enqL x (deque.Idle left (idle.Idle right length_right))) = x # RealTimeDeque.listL (deque.Idle left (idle.Idle right length_right))
[PROOF STEP]
using Idle_Proof.push_list[of x left]
[PROOF STATE]
proof (prove)
using this:
length_left' \<le> 3 * length_right
Idle.list (Idle.push x left) = x # Idle.list left

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

goal (1 subgoal):
 1. \<not> length_left' \<le> 3 * length_right \<Longrightarrow> RealTimeDeque.listL (enqL x (deque.Idle left (idle.Idle right length_right))) = x # RealTimeDeque.listL (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> RealTimeDeque.listL (enqL x (deque.Idle left (idle.Idle right length_right))) = x # RealTimeDeque.listL (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> RealTimeDeque.listL (enqL x (deque.Idle left (idle.Idle right length_right))) = x # RealTimeDeque.listL (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> RealTimeDeque.listL (enqL x (deque.Idle left (idle.Idle right length_right))) = x # RealTimeDeque.listL (deque.Idle left (idle.Idle right length_right))
[PROOF STEP]
let ?length_right = "2 * length_right + 1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> length_left' \<le> 3 * length_right \<Longrightarrow> RealTimeDeque.listL (enqL x (deque.Idle left (idle.Idle right length_right))) = x # RealTimeDeque.listL (deque.Idle left (idle.Idle right length_right))
[PROOF STEP]
let ?big = "Reverse  (Current [] 0 left' ?length_left) left' [] ?length_left"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> length_left' \<le> 3 * length_right \<Longrightarrow> RealTimeDeque.listL (enqL x (deque.Idle left (idle.Idle right length_right))) = x # RealTimeDeque.listL (deque.Idle left (idle.Idle right length_right))
[PROOF STEP]
let ?small = "Reverse1 (Current [] 0 right ?length_right) right []"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> length_left' \<le> 3 * length_right \<Longrightarrow> RealTimeDeque.listL (enqL x (deque.Idle left (idle.Idle right length_right))) = x # RealTimeDeque.listL (deque.Idle left (idle.Idle right length_right))
[PROOF STEP]
let ?states = "States Right ?big ?small"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> length_left' \<le> 3 * length_right \<Longrightarrow> RealTimeDeque.listL (enqL x (deque.Idle left (idle.Idle right length_right))) = x # RealTimeDeque.listL (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> RealTimeDeque.listL (enqL x (deque.Idle left (idle.Idle right length_right))) = x # RealTimeDeque.listL (deque.Idle left (idle.Idle right length_right))
[PROOF STEP]
from False 5 invar_left'
[PROOF STATE]
proof (chain)
picking this:
\<not> length_left' \<le> 3 * length_right
invar (deque.Idle left (idle.Idle right length_right))
invar (idle.Idle left' length_left')
[PROOF STEP]
have invar: "invar ?states"
[PROOF STATE]
proof (prove)
using this:
\<not> length_left' \<le> 3 * length_right
invar (deque.Idle left (idle.Idle right length_right))
invar (idle.Idle left' length_left')

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 (2 * length_right + 1)) 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 (2 * length_right + 1)) right []))

goal (1 subgoal):
 1. \<not> length_left' \<le> 3 * length_right \<Longrightarrow> RealTimeDeque.listL (enqL x (deque.Idle left (idle.Idle right length_right))) = x # RealTimeDeque.listL (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 (2 * length_right + 1)) right []))
[PROOF STEP]
have "States.listL ?states = x # Idle.list left @ rev (Stack.list right)"
[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 (2 * length_right + 1)) right []))

goal (1 subgoal):
 1. States.listL (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (2 * length_right + 1)) right [])) = x # Idle.list left @ rev (Stack.list right)
[PROOF STEP]
using Idle_Proof.push_list[of x left]
[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 (2 * length_right + 1)) right []))
Idle.list (Idle.push x left) = x # Idle.list left

goal (1 subgoal):
 1. States.listL (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (2 * length_right + 1)) right [])) = x # Idle.list left @ rev (Stack.list right)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
States.listL (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (2 * length_right + 1)) right [])) = x # Idle.list left @ rev (Stack.list right)

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

goal (1 subgoal):
 1. States.listL ((step ^^ 6) (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (2 * length_right + 1)) right []))) = x # Idle.list left @ rev (Stack.list right)
[PROOF STEP]
by (metis invar step_n_listL)
[PROOF STATE]
proof (state)
this:
States.listL ((step ^^ 6) (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (2 * length_right + 1)) right []))) = x # Idle.list left @ rev (Stack.list right)

goal (1 subgoal):
 1. \<not> length_left' \<le> 3 * length_right \<Longrightarrow> RealTimeDeque.listL (enqL x (deque.Idle left (idle.Idle right length_right))) = x # RealTimeDeque.listL (deque.Idle left (idle.Idle right length_right))
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
\<not> length_left' \<le> 3 * length_right
States.listL ((step ^^ 6) (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (2 * length_right + 1)) right []))) = x # Idle.list left @ rev (Stack.list right)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> length_left' \<le> 3 * length_right
States.listL ((step ^^ 6) (States direction.Right (Reverse (Current [] 0 left' (length_left' - length_right - 1)) left' [] (length_left' - length_right - 1)) (Reverse1 (Current [] 0 right (2 * length_right + 1)) right []))) = x # Idle.list left @ rev (Stack.list right)

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

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

goal (6 subgoals):
 1. \<And>x. invar Empty \<Longrightarrow> RealTimeDeque.listL (enqL x Empty) = x # RealTimeDeque.listL Empty
 2. \<And>x y. invar (One y) \<Longrightarrow> RealTimeDeque.listL (enqL x (One y)) = x # RealTimeDeque.listL (One y)
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> RealTimeDeque.listL (enqL x (Two y z)) = x # RealTimeDeque.listL (Two y z)
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> RealTimeDeque.listL (enqL x (Three a b c)) = x # RealTimeDeque.listL (Three a b c)
 5. \<And>x big small. invar (Transforming (States direction.Left big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Left big small))) = x # RealTimeDeque.listL (Transforming (States direction.Left big small))
 6. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Right big small))) = x # RealTimeDeque.listL (Transforming (States direction.Right big small))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x. invar Empty \<Longrightarrow> RealTimeDeque.listL (enqL x Empty) = x # RealTimeDeque.listL Empty
 2. \<And>x y. invar (One y) \<Longrightarrow> RealTimeDeque.listL (enqL x (One y)) = x # RealTimeDeque.listL (One y)
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> RealTimeDeque.listL (enqL x (Two y z)) = x # RealTimeDeque.listL (Two y z)
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> RealTimeDeque.listL (enqL x (Three a b c)) = x # RealTimeDeque.listL (Three a b c)
 5. \<And>x big small. invar (Transforming (States direction.Left big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Left big small))) = x # RealTimeDeque.listL (Transforming (States direction.Left big small))
 6. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Right big small))) = x # RealTimeDeque.listL (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> RealTimeDeque.listL (enqL x Empty) = x # RealTimeDeque.listL Empty
 2. \<And>x y. invar (One y) \<Longrightarrow> RealTimeDeque.listL (enqL x (One y)) = x # RealTimeDeque.listL (One y)
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> RealTimeDeque.listL (enqL x (Two y z)) = x # RealTimeDeque.listL (Two y z)
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> RealTimeDeque.listL (enqL x (Three a b c)) = x # RealTimeDeque.listL (Three a b c)
 5. \<And>x big small. invar (Transforming (States direction.Left big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Left big small))) = x # RealTimeDeque.listL (Transforming (States direction.Left big small))
 6. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Right big small))) = x # RealTimeDeque.listL (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> RealTimeDeque.listL (enqL x Empty) = x # RealTimeDeque.listL Empty
 2. \<And>x y. invar (One y) \<Longrightarrow> RealTimeDeque.listL (enqL x (One y)) = x # RealTimeDeque.listL (One y)
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> RealTimeDeque.listL (enqL x (Two y z)) = x # RealTimeDeque.listL (Two y z)
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> RealTimeDeque.listL (enqL x (Three a b c)) = x # RealTimeDeque.listL (Three a b c)
 5. \<And>x big small. invar (Transforming (States direction.Left big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Left big small))) = x # RealTimeDeque.listL (Transforming (States direction.Left big small))
 6. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Right big small))) = x # RealTimeDeque.listL (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> RealTimeDeque.listL (enqL x Empty) = x # RealTimeDeque.listL Empty
 2. \<And>x y. invar (One y) \<Longrightarrow> RealTimeDeque.listL (enqL x (One y)) = x # RealTimeDeque.listL (One y)
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> RealTimeDeque.listL (enqL x (Two y z)) = x # RealTimeDeque.listL (Two y z)
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> RealTimeDeque.listL (enqL x (Three a b c)) = x # RealTimeDeque.listL (Three a b c)
 5. \<And>x big small. invar (Transforming (States direction.Left big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Left big small))) = x # RealTimeDeque.listL (Transforming (States direction.Left big small))
 6. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Right big small))) = x # RealTimeDeque.listL (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> RealTimeDeque.listL (enqL x Empty) = x # RealTimeDeque.listL Empty
 2. \<And>x y. invar (One y) \<Longrightarrow> RealTimeDeque.listL (enqL x (One y)) = x # RealTimeDeque.listL (One y)
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> RealTimeDeque.listL (enqL x (Two y z)) = x # RealTimeDeque.listL (Two y z)
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> RealTimeDeque.listL (enqL x (Three a b c)) = x # RealTimeDeque.listL (Three a b c)
 5. \<And>x big small. invar (Transforming (States direction.Left big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Left big small))) = x # RealTimeDeque.listL (Transforming (States direction.Left big small))
 6. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Right big small))) = x # RealTimeDeque.listL (Transforming (States direction.Right big small))
[PROOF STEP]
obtain big_stepped small_stepped where stepped:
      "?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 (6 subgoals):
 1. \<And>x. invar Empty \<Longrightarrow> RealTimeDeque.listL (enqL x Empty) = x # RealTimeDeque.listL Empty
 2. \<And>x y. invar (One y) \<Longrightarrow> RealTimeDeque.listL (enqL x (One y)) = x # RealTimeDeque.listL (One y)
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> RealTimeDeque.listL (enqL x (Two y z)) = x # RealTimeDeque.listL (Two y z)
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> RealTimeDeque.listL (enqL x (Three a b c)) = x # RealTimeDeque.listL (Three a b c)
 5. \<And>x big small. invar (Transforming (States direction.Left big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Left big small))) = x # RealTimeDeque.listL (Transforming (States direction.Left big small))
 6. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Right big small))) = x # RealTimeDeque.listL (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 ?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> RealTimeDeque.listL (enqL x Empty) = x # RealTimeDeque.listL Empty
 2. \<And>x y. invar (One y) \<Longrightarrow> RealTimeDeque.listL (enqL x (One y)) = x # RealTimeDeque.listL (One y)
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> RealTimeDeque.listL (enqL x (Two y z)) = x # RealTimeDeque.listL (Two y z)
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> RealTimeDeque.listL (enqL x (Three a b c)) = x # RealTimeDeque.listL (Three a b c)
 5. \<And>x big small. invar (Transforming (States direction.Left big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Left big small))) = x # RealTimeDeque.listL (Transforming (States direction.Left big small))
 6. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Right big small))) = x # RealTimeDeque.listL (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
      "States.listL ?states_stepped = x # Small.list_current small @ rev (Big.list_current big)"
[PROOF STATE]
proof (prove)
using this:
invar (States direction.Left big (Small.push x small))

goal (1 subgoal):
 1. States.listL ((step ^^ 4) (States direction.Left big (Small.push x small))) = x # Small.list_current small @ rev (Big.list_current big)
[PROOF STEP]
using step_n_listL
[PROOF STATE]
proof (prove)
using this:
invar (States direction.Left big (Small.push x small))
invar ?states \<Longrightarrow> States.listL ((step ^^ ?n) ?states) = States.listL ?states

goal (1 subgoal):
 1. States.listL ((step ^^ 4) (States direction.Left big (Small.push x small))) = x # Small.list_current small @ rev (Big.list_current big)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
States.listL ((step ^^ 4) (States direction.Left big (Small.push x small))) = x # Small.list_current small @ rev (Big.list_current big)

goal (6 subgoals):
 1. \<And>x. invar Empty \<Longrightarrow> RealTimeDeque.listL (enqL x Empty) = x # RealTimeDeque.listL Empty
 2. \<And>x y. invar (One y) \<Longrightarrow> RealTimeDeque.listL (enqL x (One y)) = x # RealTimeDeque.listL (One y)
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> RealTimeDeque.listL (enqL x (Two y z)) = x # RealTimeDeque.listL (Two y z)
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> RealTimeDeque.listL (enqL x (Three a b c)) = x # RealTimeDeque.listL (Three a b c)
 5. \<And>x big small. invar (Transforming (States direction.Left big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Left big small))) = x # RealTimeDeque.listL (Transforming (States direction.Left big small))
 6. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Right big small))) = x # RealTimeDeque.listL (Transforming (States direction.Right big small))
[PROOF STEP]
with 6
[PROOF STATE]
proof (chain)
picking this:
invar (Transforming (States direction.Left big small))
States.listL ((step ^^ 4) (States direction.Left big (Small.push x small))) = x # Small.list_current small @ rev (Big.list_current big)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (Transforming (States direction.Left big small))
States.listL ((step ^^ 4) (States direction.Left big (Small.push x small))) = x # Small.list_current small @ rev (Big.list_current big)

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

goal (5 subgoals):
 1. \<And>x. invar Empty \<Longrightarrow> RealTimeDeque.listL (enqL x Empty) = x # RealTimeDeque.listL Empty
 2. \<And>x y. invar (One y) \<Longrightarrow> RealTimeDeque.listL (enqL x (One y)) = x # RealTimeDeque.listL (One y)
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> RealTimeDeque.listL (enqL x (Two y z)) = x # RealTimeDeque.listL (Two y z)
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> RealTimeDeque.listL (enqL x (Three a b c)) = x # RealTimeDeque.listL (Three a b c)
 5. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Right big small))) = x # RealTimeDeque.listL (Transforming (States direction.Right big small))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x. invar Empty \<Longrightarrow> RealTimeDeque.listL (enqL x Empty) = x # RealTimeDeque.listL Empty
 2. \<And>x y. invar (One y) \<Longrightarrow> RealTimeDeque.listL (enqL x (One y)) = x # RealTimeDeque.listL (One y)
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> RealTimeDeque.listL (enqL x (Two y z)) = x # RealTimeDeque.listL (Two y z)
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> RealTimeDeque.listL (enqL x (Three a b c)) = x # RealTimeDeque.listL (Three a b c)
 5. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Right big small))) = x # RealTimeDeque.listL (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> RealTimeDeque.listL (enqL x Empty) = x # RealTimeDeque.listL Empty
 2. \<And>x y. invar (One y) \<Longrightarrow> RealTimeDeque.listL (enqL x (One y)) = x # RealTimeDeque.listL (One y)
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> RealTimeDeque.listL (enqL x (Two y z)) = x # RealTimeDeque.listL (Two y z)
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> RealTimeDeque.listL (enqL x (Three a b c)) = x # RealTimeDeque.listL (Three a b c)
 5. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Right big small))) = x # RealTimeDeque.listL (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> RealTimeDeque.listL (enqL x Empty) = x # RealTimeDeque.listL Empty
 2. \<And>x y. invar (One y) \<Longrightarrow> RealTimeDeque.listL (enqL x (One y)) = x # RealTimeDeque.listL (One y)
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> RealTimeDeque.listL (enqL x (Two y z)) = x # RealTimeDeque.listL (Two y z)
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> RealTimeDeque.listL (enqL x (Three a b c)) = x # RealTimeDeque.listL (Three a b c)
 5. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Right big small))) = x # RealTimeDeque.listL (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> RealTimeDeque.listL (enqL x Empty) = x # RealTimeDeque.listL Empty
 2. \<And>x y. invar (One y) \<Longrightarrow> RealTimeDeque.listL (enqL x (One y)) = x # RealTimeDeque.listL (One y)
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> RealTimeDeque.listL (enqL x (Two y z)) = x # RealTimeDeque.listL (Two y z)
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> RealTimeDeque.listL (enqL x (Three a b c)) = x # RealTimeDeque.listL (Three a b c)
 5. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Right big small))) = x # RealTimeDeque.listL (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> RealTimeDeque.listL (enqL x Empty) = x # RealTimeDeque.listL Empty
 2. \<And>x y. invar (One y) \<Longrightarrow> RealTimeDeque.listL (enqL x (One y)) = x # RealTimeDeque.listL (One y)
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> RealTimeDeque.listL (enqL x (Two y z)) = x # RealTimeDeque.listL (Two y z)
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> RealTimeDeque.listL (enqL x (Three a b c)) = x # RealTimeDeque.listL (Three a b c)
 5. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Right big small))) = x # RealTimeDeque.listL (Transforming (States direction.Right big small))
[PROOF STEP]
obtain big_stepped small_stepped where stepped:
      "?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 (5 subgoals):
 1. \<And>x. invar Empty \<Longrightarrow> RealTimeDeque.listL (enqL x Empty) = x # RealTimeDeque.listL Empty
 2. \<And>x y. invar (One y) \<Longrightarrow> RealTimeDeque.listL (enqL x (One y)) = x # RealTimeDeque.listL (One y)
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> RealTimeDeque.listL (enqL x (Two y z)) = x # RealTimeDeque.listL (Two y z)
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> RealTimeDeque.listL (enqL x (Three a b c)) = x # RealTimeDeque.listL (Three a b c)
 5. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Right big small))) = x # RealTimeDeque.listL (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 list_invar:
    "list_current_small_first (States Right big small) = list_small_first (States Right big small)"
[PROOF STATE]
proof (prove)
using this:
invar (Transforming (States direction.Right big small))

goal (1 subgoal):
 1. list_current_small_first (States direction.Right big small) = list_small_first (States direction.Right big small)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
list_current_small_first (States direction.Right big small) = list_small_first (States direction.Right big small)

goal (5 subgoals):
 1. \<And>x. invar Empty \<Longrightarrow> RealTimeDeque.listL (enqL x Empty) = x # RealTimeDeque.listL Empty
 2. \<And>x y. invar (One y) \<Longrightarrow> RealTimeDeque.listL (enqL x (One y)) = x # RealTimeDeque.listL (One y)
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> RealTimeDeque.listL (enqL x (Two y z)) = x # RealTimeDeque.listL (Two y z)
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> RealTimeDeque.listL (enqL x (Three a b c)) = x # RealTimeDeque.listL (Three a b c)
 5. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Right big small))) = x # RealTimeDeque.listL (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> RealTimeDeque.listL (enqL x Empty) = x # RealTimeDeque.listL Empty
 2. \<And>x y. invar (One y) \<Longrightarrow> RealTimeDeque.listL (enqL x (One y)) = x # RealTimeDeque.listL (One y)
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> RealTimeDeque.listL (enqL x (Two y z)) = x # RealTimeDeque.listL (Two y z)
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> RealTimeDeque.listL (enqL x (Three a b c)) = x # RealTimeDeque.listL (Three a b c)
 5. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Right big small))) = x # RealTimeDeque.listL (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
      "States.listL ?states = x # Big.list_current big @ rev (Small.list_current small)"
[PROOF STATE]
proof (prove)
using this:
invar (States direction.Right (Big.push x big) small)

goal (1 subgoal):
 1. States.listL (States direction.Right (Big.push x big) small) = x # Big.list_current big @ rev (Small.list_current small)
[PROOF STEP]
using app_rev[of _ _ _ "x # Big.list_current big"]
[PROOF STATE]
proof (prove)
using this:
invar (States direction.Right (Big.push x big) small)
?as @ rev ?bs = ?cs @ rev (x # Big.list_current big) \<Longrightarrow> ?bs @ rev ?as = (x # Big.list_current big) @ rev ?cs

goal (1 subgoal):
 1. States.listL (States direction.Right (Big.push x big) small) = x # Big.list_current big @ rev (Small.list_current small)
[PROOF STEP]
by(auto split: prod.split)
[PROOF STATE]
proof (state)
this:
States.listL (States direction.Right (Big.push x big) small) = x # Big.list_current big @ rev (Small.list_current small)

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

goal (1 subgoal):
 1. States.listL ((step ^^ 4) (States direction.Right (Big.push x big) small)) = x # Big.list_current big @ rev (Small.list_current small)
[PROOF STEP]
by (metis invar step_n_listL)
[PROOF STATE]
proof (state)
this:
States.listL ((step ^^ 4) (States direction.Right (Big.push x big) small)) = x # Big.list_current big @ rev (Small.list_current small)

goal (5 subgoals):
 1. \<And>x. invar Empty \<Longrightarrow> RealTimeDeque.listL (enqL x Empty) = x # RealTimeDeque.listL Empty
 2. \<And>x y. invar (One y) \<Longrightarrow> RealTimeDeque.listL (enqL x (One y)) = x # RealTimeDeque.listL (One y)
 3. \<And>x y z. invar (Two y z) \<Longrightarrow> RealTimeDeque.listL (enqL x (Two y z)) = x # RealTimeDeque.listL (Two y z)
 4. \<And>x a b c. invar (Three a b c) \<Longrightarrow> RealTimeDeque.listL (enqL x (Three a b c)) = x # RealTimeDeque.listL (Three a b c)
 5. \<And>x big small. invar (Transforming (States direction.Right big small)) \<Longrightarrow> RealTimeDeque.listL (enqL x (Transforming (States direction.Right big small))) = x # RealTimeDeque.listL (Transforming (States direction.Right big small))
[PROOF STEP]
with list_invar
[PROOF STATE]
proof (chain)
picking this:
list_current_small_first (States direction.Right big small) = list_small_first (States direction.Right big small)
States.listL ((step ^^ 4) (States direction.Right (Big.push x big) small)) = x # Big.list_current big @ rev (Small.list_current small)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
list_current_small_first (States direction.Right big small) = list_small_first (States direction.Right big small)
States.listL ((step ^^ 4) (States direction.Right (Big.push x big) small)) = x # Big.list_current big @ rev (Small.list_current small)

goal (1 subgoal):
 1. RealTimeDeque.listL (enqL x (Transforming (States direction.Right big small))) = x # RealTimeDeque.listL (Transforming (States direction.Right big small))
[PROOF STEP]
using app_rev[of "Small.list_current small" "Big.list_current big"]
[PROOF STATE]
proof (prove)
using this:
list_current_small_first (States direction.Right big small) = list_small_first (States direction.Right big small)
States.listL ((step ^^ 4) (States direction.Right (Big.push x big) small)) = x # Big.list_current big @ rev (Small.list_current small)
Small.list_current small @ rev (Big.list_current big) = ?cs @ rev ?ds \<Longrightarrow> Big.list_current big @ rev (Small.list_current small) = ?ds @ rev ?cs

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

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