# Re: [isabelle] proof solution [ newbie question ]

```Gregory,

I don't think it is provable for xs and ys empty.

```
lemma assumes xs0: "xs ~= []" and ys0: "ys ~= []" and hd: "hd xs = hd ys" and tl: "tl xs @ zs = tl ys"
```  shows "xs @ zs = ys"
proof-
from xs0 ys0 obtain xsh xst ysh yst
where xs: "xs = xsh#xst" and ys: "ys = ysh#yst" apply (cases xs, auto)
apply (cases ys, auto) done
with hd have xsh: "xsh = ysh" by simp
have "ys = xsh#(tl ys)" by  (simp add: ys xsh)
also have "... = xsh # xst @ zs" by (simp add: tl[symmetric] xs)
finally show ?thesis by (simp add: xs)
qed

Amin.

Gregory Kulczycki wrote:
```
I've been experimenting with the Isabelle prover and have reached a point in
```a proof where I have the following subgoal:

/\ xs ys zs. [| hd xs = hd ys; tl xs @ zs = tl ys |] ==> xs @ zs = ys

This looks obvious to me (since xs @ zs = ys is equivalent to hd xs # tl xs
@ zs = hd ys # tl ys for non-empty xs) , but I don't know how to proceed.

Any suggestions?

Thanks,
Greg
```
```

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.