(use-modules (vikalpa)
             (vikalpa the-little-prover))

(define-system the-little-prover-0 (the-little-prover)
  (define-theorem simple-list-induction (x)
    (equal? (if (natural? (size x))
                (if (atom? x) '#t (< (size (cdr x)) (size x)))
                '#t)
            #t))

  (define-proof simple-list-induction
    ()
    (((1 2 3) size/cdr)
     ((1 2) if-same)
     ((1) if-same)
     (() equal-same)))

  (define-function list-length (xs)
    (if (atom? xs)
        '0
        (+ '1 (list-length (cdr xs)))))

  (define-proof list-length
    (natural? (size xs))
    ((() simple-list-induction)))

  (define-theorem natural?/1 ()
    (equal? (natural? 1) #t))

  (define-proof natural?/1
    ()
    ((() if-same (set x (natural? '0)))
     ((2 1) natural?/succ)
     ((2) equal-same)
     ((1) natural?/0)
     (() if-true)))

  (define-theorem natural?/list-length (xs)
    (natural? (list-length xs)))

  (define-proof natural?/list-length
    (list-induction xs)
    (((2 1) list-length)
     ((2 1) if-nest-A)
     ((2) natural?/0)
     ((3 2 1) list-length)
     ((3 2 1) if-nest-E)
     ((3) if-same (set x (natural? (succ '0))))
     ((3 2 2) natural?/+)
     ((3 2) if-same)
     ((3 1) natural?/1)
     ((3) if-true)
     (() if-same))))