#lang pie
;Authoren: Jan Huber & Alexander Rzehak
; Kommentare mit Semikolon
(claim Pear U)
(define Pear (Pair Nat Nat))

(claim Birne U)
(define Birne Pear)

(claim sub1 (-> Nat Nat))
(define sub1 (lambda (a) (rec-Nat a 0 (lambda (n-1 akk) n-1))))


(claim + (-> Nat Nat Nat))
(define + (lambda (x y)(iter-Nat x y (lambda (a) (add1 a)))))

(claim - (-> Nat Nat Nat))
(define - (lambda (x y) (iter-Nat y x (lambda (a) (sub1 a)))))

(claim * (-> Nat Nat Nat))
(define * (lambda (x y) (iter-Nat x 0 (lambda (a) (+ a y)))))


(claim gauss (-> Nat Nat))
(define gauss (lambda (n) (rec-Nat n 0 (lambda (n-1 akk) (+ (add1 n-1) akk)))))

(claim factorial (-> Nat Nat))
(define factorial (lambda (n) (rec-Nat n 1 (lambda (n-1 akk) (* (add1 n-1) akk)))))

(claim five (-> Nat Nat))
(define five (lambda (x) 5))

(claim pow (-> Nat Nat Nat))
(define pow (lambda (x y) (rec-Nat y 1 (lambda (n-1)(lambda (akk) (* akk x))))))

(claim True Nat)
(define True 0)
(claim False Nat)
(define False 1)
(claim Bool U)
(define Bool Nat)

(claim == (-> Nat Nat Nat))
(define == (lambda (a b)(which-Nat (+ (which-Nat (- a b) 0 (lambda (y) 1)) (which-Nat (- b a) 0 (lambda (z) 1))) 0 (lambda (x) 1))))

(claim modulo-step (-> Nat Nat Nat))
(define modulo-step (lambda (a b) (which-Nat (== a b) 0 (lambda (y)(which-Nat (- a b) a (lambda (x)(- a b)))))))

(claim modulo (-> Nat Nat Nat))
(define modulo (lambda (a b)(rec-Nat a a (lambda (n-1 akk) (modulo-step akk b)))))

(claim durch2teilbar (-> Nat Bool))
(define durch2teilbar (lambda (x) (which-Nat (modulo x 2) 0 (lambda (y)1))))

(claim durchXteilbar (-> Nat Nat Bool))
(define durchXteilbar (lambda (a x) (which-Nat (modulo a x) 0 (lambda (y)1))))

(claim halbierer (-> Nat Nat))
(define halbierer (lambda (x)(rec-Nat x 0 (lambda (n-1 akk) (which-Nat (durch2teilbar n-1) akk (lambda(y)(add1 akk)))))))

;funktioniert noch nicht
(claim / (-> Nat Nat Nat))
(define / (lambda (x divisor)(rec-Nat x 0 (lambda (n-1 akk) (which-Nat (durchXteilbar n-1 divisor) akk (lambda(y)(add1 akk)))))))