<= y) xs`
Thank you very much! I will try my proofs again.
Regards,
Liu
-Original Messages-
From:michael.norr...@data61.csiro.au
Sent Time:2017-12-04 13:35:21 (Monday)
To: 2015200...@mail.buct.edu.cn
Cc: hol-info@lists.sourceforge.net
Subject: Re: [Hol-info] Proof about sortin
.
Michael
From: Liu Gengyang <2015200...@mail.buct.edu.cn>
Date: Monday, 4 December 2017 at 14:38
To: "Norrish, Michael (Data61, Acton)"
Cc: hol4_QA
Subject: Re: Re: [Hol-info] Proof about sorting
Hi Michael,
I have been seen these documents before, but there is no theorem same to
(Monday)
To: 2015200...@mail.buct.edu.cn, hol-info@lists.sourceforge.net
Cc:
Subject: Re: [Hol-info] Proof about sorting
There are proofs that quick-sort and merge-sort are correct in the distribution
already. Perhaps looking at these examples in src/sort will give you some
clues.
Michael
From: Liu Geng
You might like to try the following
(1) a predicate sorted, to mean each list member is <= the next one
(2) a lemma that inserting an element into a sorted list gives a sorted list
Jeremy
On 04/12/17 12:58, Liu Gengyang wrote:
Hi,
Recently I am meeting a problem, it has been confusing me a f
There are proofs that quick-sort and merge-sort are correct in the distribution
already. Perhaps looking at these examples in src/sort will give you some
clues.
Michael
From: Liu Gengyang <2015200...@mail.buct.edu.cn>
Date: Monday, 4 December 2017 at 13:02
To: hol4_QA
Subject: [Hol-info] Proo
