[Agda] Kruskal's theorem

[Sergei Meshveliani]

Great! Thank you.

And my formulation below looked a bit stronger:
I wrote 
        "w(j) = u w(i) v  for some words  u, v".

But all right, I agree to change this to
"w(i) is obtained by deleting some letters (may be none) from w(j)".

------
Sergei


On Mon, 2014-06-30 at 10:16 +0200, Frédéric Blanqui wrote:
> This is Higman's Lemma, a special case of Kruskal's theorem indeed. See 
> http://en.wikipedia.org/wiki/Higman%27s_lemma . There are proofs of this 
> lemma in various proof assistants including Coq. Check on the web. I 
> don't know for Agda. Regards, Frédéric.
> 
> Le 30/06/2014 10:00, Sergei Meshveliani a écrit :
> > People,
> >
> > consider the following theorem.
> >
> > Th-0
> > ----
> > Let   w(1), w(2) ...
> > be an infinite sequence of words in the alphabet  {a, b}.
> > Then there exist  i < j  such that  w(i) is a subword in w(j)
> > (that is   w(j) = u w(i) v   for some words  u, v).
> >
> > 1) Is this true?
> > (I am sorry if I confuse things).
> >
> > 2) Is this a special case of Kruskal's theorem about finite trees?
> > 3) Has anybody tried to prove in Agda a theorem like Th-0 ?
> > 4) In Coq ?
> >
> > Thanks,
> >
> > ------
> > Sergei
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>