; $Id: quotrem-ex.scm,v 1.4 2008/01/25 13:30:26 logik Exp $

(set! COMMENT-FLAG #f)
(libload "nat.scm")
(set! COMMENT-FLAG #t)
(set! DOT-NOTATION #f)

(add-var-name "l" (py "nat"))

; "QR"
(set-goal (pf "all m,n ex k,l(n=(m+1)*k+l & l<m+1)"))
(assume "m")
(ind)
(ex-intro (pt "0"))
(ex-intro (pt "0"))
(ng)
(prop)
(assume "n" 1)
(ex-elim 1)
(assume "k" 2)
(ex-elim 2)
(assume "l" 3)
(cases (pt "l<m"))

; Case l<m
(assume 4)
(ex-intro (pt "k"))
(ex-intro (pt "l+1"))
(ng)
(prop)

; Case l<m -> F
(assume 4)
(ex-intro (pt "k+1"))
(ex-intro (pt "0"))
(ng)
(split)
(add-global-assumption
 "Lemma" (pf "all n,m,k,l(n=m*k+k+l & l<m+1 &(l<m -> F) -> n=m*k+k+m)"))
(use "Lemma" (pt "l"))
(prop)
(prop)
; Proof finished.
(save "QR")

(define eterm (proof-to-extracted-term (theorem-name-to-proof "QR")))
(add-var-name "p" (py "nat@@nat"))
(define neterm (nt eterm))

(pp neterm)

; [n0,n1]
;  (Rec nat=>nat@@nat)n1(0@0)
;  ([n2,p3][if (right p3<n0) (left p3@Succ right p3) (Succ left p3@0)])

(pp (nt (mk-term-in-app-form neterm (pt "2") (pt "7"))))
(pp (nt (mk-term-in-app-form neterm (pt "5") (pt "7"))))
(pp (nt (mk-term-in-app-form neterm (pt "6") (pt "54"))))
(pp (nt (mk-term-in-app-form neterm (pt "6") (pt "754"))))