ϵ">]> Clausal Language (ver. 5.81.20, by P.J. Voda, J. Komara, J. Kluka)
...
Clausal Language (ver. 5.81.20, by P.J. Voda, J. Komara, J. Kluka)
Module  Ex12a in logic: Peano arithmetic
Included module  Standard
Included module  Mtex
Included module  Mauxa
Remark 

Literature.

  • [1] J. Komara. Declarative Programming. Downloadable lecture notes available through the web page of the course.

  • [2] J. Kľuka. Lecture Notes from Introduction to Declarative Programming.

  • [3] J. Komara and P. J. Voda. Metamathematics of Computer Programming. 2001.

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 , x ) =?
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
Theorem  Insert_ord
Ord (x) →OrdInsert (a,x)
Remark 

Insertion sort.

Function  Isort
Isort ( x ) =?
Remark 

Exercise. 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: 251376 free: 133964764
Time used: 0:0:1:12