--
--      операция сравнения '=' и ключевое слово 'is' 
--      имеют различный смысл, но в этом примере смысл практически совпадает.
--      если в схеме появляются "глобальные переменные" - множество
--      всех глобальных переменных наз. состояние - то операция = и 
--      is будут иметь различный смысл. is означает равно для всех состояний
-- 

scheme PEANO =
    class
        type                        -- завели тип N
            N
        value
            zero : N,               -- завели величину zero
                                    -- (это не переменная, нельзя присваивать)
            succ: N -> N            -- величина - функция из N в N
        axiom
          [first_is_zero]         --
                                    -- квантор всеобщности
            all n : N :-            -- n - это обозначение

                ~(succ(n) is zero)  -- для каждого n результат succ(n)
            ,                       -- не есть zero
          [linear_order]
            all  n1, n2 : N :-
                (succ(n1) is succ(n2)) => (n1 is n2)
            ,
          [induction]
            all p : N -> Bool :-    -- для любого предиката
                                    --
                    (p(zero) /\ (all n : N :- p(n) => p(succ(n))))
                         =>
                             (all n : N :- p(n))
    end

--
-- ~     отрицание
-- :-    выполняется
-- =>    влечет
-- /\    логическое и
-- \/    логическое или
-- exist квантор существования   
--
--

PEANO                           --  подключение схемы PEANO

scheme NAT =
    extend PEANO with
    class
        value
          plus : N >< N -> N    -- вводим функции (операции)  сложить
          ,
          mult : N >< N -> N    -- и умножить
        axiom
          [plus_zero]
            all n : N :-
            plus(n, zero) is n
            ,
          [plus_succ]
            all n1, n2 : N :-
            plus(n1, succ(n2)) is succ(plus(n1, n2))
            ,
          [mult_zero]
            all n : N :-
            mult(n, zero) is zero
            ,
          [mult_succ]
            all n1, n2 : N :-
            mult(n1, succ(n2)) is plus(mult(n1, n2), n1)

    end