;; 2026-04-12.  natpluscomm.scm

;; (load "~/git/minlog/init.scm")

(set! COMMENT-FLAG #f)
(load "natplus.scm") ;ggf. den passenden Pfad zu natplus.scm angeben
(set! COMMENT-FLAG #t)

(display-pconst "NatPlus")

(set-goal "all n 0+n=n")
(ind)
(use "Truth")
(assume "n" "IH")
...

(add-rewrite-rule "0+n" "n")

(display-pconst "NatPlus")

(set-goal "all n,m Succ n+m=Succ(n+m)")
(assume "n")
(ind)
...

(add-rewrite-rule "Succ n+m" "Succ(n+m)")

(display-pconst "NatPlus")

(set-goal "all n,m,l n+(m+l)=n+m+l")
(assume "n" "m")
(ind)
...

(add-rewrite-rule "n+(m+l)" "n+m+l")

(display-pconst "NatPlus")

(save "NatPlusAssoc")

(pp "NatPlusAssoc")

;; NatPlusComm
(set-goal "all n,m n+m=m+n")
...

(save "NatPlusComm")

(pp "NatPlusComm")