[STATEMENT]
lemma lfinite_lappend [simp]:
  "lfinite (lappend xs ys) \<longleftrightarrow> lfinite xs \<and> lfinite ys"
  (is "?lhs \<longleftrightarrow> ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lfinite (lappend xs ys) = (lfinite xs \<and> lfinite ys)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lfinite (lappend xs ys) \<Longrightarrow> lfinite xs \<and> lfinite ys
 2. lfinite xs \<and> lfinite ys \<Longrightarrow> lfinite (lappend xs ys)
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
lfinite (lappend xs ys)

goal (2 subgoals):
 1. lfinite (lappend xs ys) \<Longrightarrow> lfinite xs \<and> lfinite ys
 2. lfinite xs \<and> lfinite ys \<Longrightarrow> lfinite (lappend xs ys)
[PROOF STEP]
thus ?rhs
[PROOF STATE]
proof (prove)
using this:
lfinite (lappend xs ys)

goal (1 subgoal):
 1. lfinite xs \<and> lfinite ys
[PROOF STEP]
proof(induct zs\<equiv>"lappend xs ys" arbitrary: xs ys)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xs ys. LNil = lappend xs ys \<Longrightarrow> lfinite xs \<and> lfinite ys
 2. \<And>xs x xsa ys. \<lbrakk>lfinite xs; \<And>xsa ys. xs = lappend xsa ys \<Longrightarrow> lfinite xsa \<and> lfinite ys; LCons x xs = lappend xsa ys\<rbrakk> \<Longrightarrow> lfinite xsa \<and> lfinite ys
[PROOF STEP]
case lfinite_LNil
[PROOF STATE]
proof (state)
this:
LNil = lappend xs ys

goal (2 subgoals):
 1. \<And>xs ys. LNil = lappend xs ys \<Longrightarrow> lfinite xs \<and> lfinite ys
 2. \<And>xs x xsa ys. \<lbrakk>lfinite xs; \<And>xsa ys. xs = lappend xsa ys \<Longrightarrow> lfinite xsa \<and> lfinite ys; LCons x xs = lappend xsa ys\<rbrakk> \<Longrightarrow> lfinite xsa \<and> lfinite ys
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
LNil = lappend xs ys

goal (1 subgoal):
 1. lfinite xs \<and> lfinite ys
[PROOF STEP]
by(simp add: LNil_eq_lappend_iff)
[PROOF STATE]
proof (state)
this:
lfinite xs \<and> lfinite ys

goal (1 subgoal):
 1. \<And>xs x xsa ys. \<lbrakk>lfinite xs; \<And>xsa ys. xs = lappend xsa ys \<Longrightarrow> lfinite xsa \<and> lfinite ys; LCons x xs = lappend xsa ys\<rbrakk> \<Longrightarrow> lfinite xsa \<and> lfinite ys
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs x xsa ys. \<lbrakk>lfinite xs; \<And>xsa ys. xs = lappend xsa ys \<Longrightarrow> lfinite xsa \<and> lfinite ys; LCons x xs = lappend xsa ys\<rbrakk> \<Longrightarrow> lfinite xsa \<and> lfinite ys
[PROOF STEP]
case (lfinite_LConsI zs z)
[PROOF STATE]
proof (state)
this:
lfinite zs
zs = lappend ?xs ?ys \<Longrightarrow> lfinite ?xs \<and> lfinite ?ys
LCons z zs = lappend xs ys

goal (1 subgoal):
 1. \<And>xs x xsa ys. \<lbrakk>lfinite xs; \<And>xsa ys. xs = lappend xsa ys \<Longrightarrow> lfinite xsa \<and> lfinite ys; LCons x xs = lappend xsa ys\<rbrakk> \<Longrightarrow> lfinite xsa \<and> lfinite ys
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
lfinite zs
zs = lappend ?xs ?ys \<Longrightarrow> lfinite ?xs \<and> lfinite ?ys
LCons z zs = lappend xs ys

goal (1 subgoal):
 1. lfinite xs \<and> lfinite ys
[PROOF STEP]
by(cases xs)(cases ys, simp_all)
[PROOF STATE]
proof (state)
this:
lfinite xs \<and> lfinite ys

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lfinite xs \<and> lfinite ys

goal (1 subgoal):
 1. lfinite xs \<and> lfinite ys \<Longrightarrow> lfinite (lappend xs ys)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lfinite xs \<and> lfinite ys \<Longrightarrow> lfinite (lappend xs ys)
[PROOF STEP]
assume ?rhs (is "?xs \<and> ?ys")
[PROOF STATE]
proof (state)
this:
lfinite xs \<and> lfinite ys

goal (1 subgoal):
 1. lfinite xs \<and> lfinite ys \<Longrightarrow> lfinite (lappend xs ys)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lfinite xs \<and> lfinite ys
[PROOF STEP]
obtain ?xs ?ys
[PROOF STATE]
proof (prove)
using this:
lfinite xs \<and> lfinite ys

goal (1 subgoal):
 1. (\<lbrakk>lfinite xs; lfinite ys\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
lfinite xs
lfinite ys

goal (1 subgoal):
 1. lfinite xs \<and> lfinite ys \<Longrightarrow> lfinite (lappend xs ys)
[PROOF STEP]
thus ?lhs
[PROOF STATE]
proof (prove)
using this:
lfinite xs
lfinite ys

goal (1 subgoal):
 1. lfinite (lappend xs ys)
[PROOF STEP]
by induct simp_all
[PROOF STATE]
proof (state)
this:
lfinite (lappend xs ys)

goal:
No subgoals!
[PROOF STEP]
qed