tail recursion
--------------
size(H . L) = 1 + size(L); size([]) = 0


algebraic data types
--------------------
Tree = Leaf | Node Tree Tree // node, left subtree, right subtree


example of a simple alegbra
---------------------------
sorts S = { Bool, Nat }

A = < [D_Bool, D_Nat], [F]_T > where:
	D_Bool = { tt, ff }
	D_Nat = { 0, 1, ...}
	F_Bool = { true, false } // constants
	F_Nat = { 0 } // constants
	F_{Bool -> Bool} = { not }
	F_{Bool Bool -> Bool} = { and, or }
	F_{Nat -> Nat} = { succ }
	F_{Nat Nat -> Nat} = { plus, minus, times, div }


equations
---------
plus(5,1) = succ(5)
times(4,2) = plus(4,4)

variables n : Nat
plus(n,1) = succ(n)
times(n,2) = plus(n,n)
forall m : Nat . plus(n,m) = plus(m,n)


initial correct model X wrong model
-----------------------------------
specification Ex
	sorts Bool
	operations
		true, false : -> Bool
		not : Bool -> Bool
	equations (sentences)
		not(true) = false
		not(false) = true

the correct model (initial) is just this one
	D = {0,1} // carrier set
	true = 1
	false = 0
	not(0) = 1
	not(1) = 0

wrong incorrect model is for example this one
	D = {1}
	true = 1
	false = 1
	not(1) = 1


specification for List
----------------------
sorts: List, Int

empty_list()
add(L, o)
add(L, i, o)
get(L, i)
remove(L, i)
size(L)
contains(L, o)

contains(empty_list(), o) = false // terminating condition
contains(add(L, o1), o) = if o1 == o then true else contains(L, o)