...
Clausal Language (ver. 5.81.21, by P.J. Voda, J. Komara, J. Kluka)
Module  Ex09c in logic: Peano arithmetic
Included module  Standard
Included module  Mtex
Included module  Mtexln
Included module  Mauxc
Remark 

Literature.

  • [1] Ján Komara. Specification and Verification of Programs. Online.

  • [2] Ján Kľuka. Úvod do deklaratívneho programovania. Online.

  • [3] Ján Komara. Recursive Functions. Online.

Remark 

Chapter. Programs Operating on Lists.

Remark 

Section. Sorting of Lists.

Remark 

[CL] Remark. See the auxiliary module Maux*.

Remark 

Subsection. Insertion Sort.

Remark 

Insertion function.

Function  Insert  / 2
Insert ( a ,0) =a,0 Insert ( a , v , w ) =a,v,w← a≦v Insert ( a , v , w ) =v,Insert (a,w) ← a>v
Remark 

Exercise. Prove

Insert (a,x) ∼a,x Ord (x) →OrdInsert (a,x)
Lemma  Lemma_insert_perm
i∼a,w→v,i∼a,v,w 
##
Theorem  Insert_perm
Insert (a,x) ∼a,x 
##
Lemma  Insert_le
b≦a∧b≼x→b≼Insert (a,x) 
##
Theorem  Insert_ord
Ord (x) →OrdInsert (a,x)
Remark 

Insertion sort.

Function  Isort
Isort (0) =0 Isort ( v , w ) =Insert (v,Isort (w) )
Remark 

Exercise. (bonus 2 points) Prove

Isort (x) ∼x OrdIsort (x)
Lemma  Lemma_isort_perm
iw∼w∧ivw∼v,iw→ivw∼v,w 
##
Theorem  Isort_perm
Isort (x) ∼x 
##
Theorem  Isort_ord
OrdIsort (x)
Query:

Results:
Heap used: 260500 free: 133955200
Time used: 0:0:0:61