[STATEMENT]
lemma chop_transfer [transfer_rule]: 
  "((=) ===> list_all2 R ===> list_all2 (list_all2 R)) chop chop"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> list_all2 R ===> list_all2 (list_all2 R)) chop chop
[PROOF STEP]
proof (intro rel_funI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>x = y; list_all2 R xa ya\<rbrakk> \<Longrightarrow> list_all2 (list_all2 R) (chop x xa) (chop y ya)
[PROOF STEP]
fix m n ::nat and xs :: "'a list" and ys :: "'b list"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>x = y; list_all2 R xa ya\<rbrakk> \<Longrightarrow> list_all2 (list_all2 R) (chop x xa) (chop y ya)
[PROOF STEP]
assume "m = n" "list_all2 R xs ys"
[PROOF STATE]
proof (state)
this:
m = n
list_all2 R xs ys

goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>x = y; list_all2 R xa ya\<rbrakk> \<Longrightarrow> list_all2 (list_all2 R) (chop x xa) (chop y ya)
[PROOF STEP]
from this(2)
[PROOF STATE]
proof (chain)
picking this:
list_all2 R xs ys
[PROOF STEP]
have "list_all2 (list_all2 R) (chop n xs) (chop n ys)"
[PROOF STATE]
proof (prove)
using this:
list_all2 R xs ys

goal (1 subgoal):
 1. list_all2 (list_all2 R) (chop n xs) (chop n ys)
[PROOF STEP]
proof (induction n xs arbitrary: ys rule: chop.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>n ys. list_all2 R [] ys \<Longrightarrow> list_all2 (list_all2 R) (chop n []) (chop n ys)
 2. \<And>xs ys. list_all2 R xs ys \<Longrightarrow> list_all2 (list_all2 R) (chop 0 xs) (chop 0 ys)
 3. \<And>n xs ys. \<lbrakk>0 < n; xs \<noteq> []; \<And>ys. list_all2 R (drop n xs) ys \<Longrightarrow> list_all2 (list_all2 R) (chop n (drop n xs)) (chop n ys); list_all2 R xs ys\<rbrakk> \<Longrightarrow> list_all2 (list_all2 R) (chop n xs) (chop n ys)
[PROOF STEP]
case (3 n xs ys)
[PROOF STATE]
proof (state)
this:
0 < n
xs \<noteq> []
list_all2 R (drop n xs) ?ys \<Longrightarrow> list_all2 (list_all2 R) (chop n (drop n xs)) (chop n ?ys)
list_all2 R xs ys

goal (3 subgoals):
 1. \<And>n ys. list_all2 R [] ys \<Longrightarrow> list_all2 (list_all2 R) (chop n []) (chop n ys)
 2. \<And>xs ys. list_all2 R xs ys \<Longrightarrow> list_all2 (list_all2 R) (chop 0 xs) (chop 0 ys)
 3. \<And>n xs ys. \<lbrakk>0 < n; xs \<noteq> []; \<And>ys. list_all2 R (drop n xs) ys \<Longrightarrow> list_all2 (list_all2 R) (chop n (drop n xs)) (chop n ys); list_all2 R xs ys\<rbrakk> \<Longrightarrow> list_all2 (list_all2 R) (chop n xs) (chop n ys)
[PROOF STEP]
hence "ys \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
0 < n
xs \<noteq> []
list_all2 R (drop n xs) ?ys \<Longrightarrow> list_all2 (list_all2 R) (chop n (drop n xs)) (chop n ?ys)
list_all2 R xs ys

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

goal (3 subgoals):
 1. \<And>n ys. list_all2 R [] ys \<Longrightarrow> list_all2 (list_all2 R) (chop n []) (chop n ys)
 2. \<And>xs ys. list_all2 R xs ys \<Longrightarrow> list_all2 (list_all2 R) (chop 0 xs) (chop 0 ys)
 3. \<And>n xs ys. \<lbrakk>0 < n; xs \<noteq> []; \<And>ys. list_all2 R (drop n xs) ys \<Longrightarrow> list_all2 (list_all2 R) (chop n (drop n xs)) (chop n ys); list_all2 R xs ys\<rbrakk> \<Longrightarrow> list_all2 (list_all2 R) (chop n xs) (chop n ys)
[PROOF STEP]
with 3
[PROOF STATE]
proof (chain)
picking this:
0 < n
xs \<noteq> []
list_all2 R (drop n xs) ?ys \<Longrightarrow> list_all2 (list_all2 R) (chop n (drop n xs)) (chop n ?ys)
list_all2 R xs ys
ys \<noteq> []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
0 < n
xs \<noteq> []
list_all2 R (drop n xs) ?ys \<Longrightarrow> list_all2 (list_all2 R) (chop n (drop n xs)) (chop n ?ys)
list_all2 R xs ys
ys \<noteq> []

goal (1 subgoal):
 1. list_all2 (list_all2 R) (chop n xs) (chop n ys)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
list_all2 (list_all2 R) (chop n xs) (chop n ys)

goal (2 subgoals):
 1. \<And>n ys. list_all2 R [] ys \<Longrightarrow> list_all2 (list_all2 R) (chop n []) (chop n ys)
 2. \<And>xs ys. list_all2 R xs ys \<Longrightarrow> list_all2 (list_all2 R) (chop 0 xs) (chop 0 ys)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
list_all2 (list_all2 R) (chop n xs) (chop n ys)

goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>x = y; list_all2 R xa ya\<rbrakk> \<Longrightarrow> list_all2 (list_all2 R) (chop x xa) (chop y ya)
[PROOF STEP]
with \<open>m = n\<close>
[PROOF STATE]
proof (chain)
picking this:
m = n
list_all2 (list_all2 R) (chop n xs) (chop n ys)
[PROOF STEP]
show "list_all2 (list_all2 R) (chop m xs) (chop n ys)"
[PROOF STATE]
proof (prove)
using this:
m = n
list_all2 (list_all2 R) (chop n xs) (chop n ys)

goal (1 subgoal):
 1. list_all2 (list_all2 R) (chop m xs) (chop n ys)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
list_all2 (list_all2 R) (chop m xs) (chop n ys)

goal:
No subgoals!
[PROOF STEP]
qed