[Agda] Kruskal's theorem

[Frédéric Blanqui]

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