;; 2022-10-03.  ivt2.scm.  Based on ivt1.scm.  NatToPos replaced by
;; cNatPos (in pos.scm) to block unwanted unfoldings.

;; 2022-09-28.  ivt1.scm

;; Change: IVTAux proved with 4 rather than 3 subintervals, to work
;; work with dyadic rationals only.

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

(set! COMMENT-FLAG #f)
(libload "nat.scm")
(libload "list.scm")
(libload "pos.scm")
(libload "int.scm")
(libload "rat.scm")
(libload "rea.scm")
(libload "cont.scm")
;; (set! COMMENT-FLAG #t)

(display "loading ivt.scm ...") (newline)

;; Intermediate value theorem, with 1/2^l a lower bound on the slope:

;; Approximate splitting principle.

;; (pp "ApproxSplit")
;; all x,y,z,p(Real x -> Real y -> Real z -> RealLt x y p -> z<<=y oru x<<=z)

;; We use a formulation of ApproxSplit without disjunction.

;; ApproxSplitBoole
(set-goal "all x1,x2,x3,p(Real x1 -> Real x2 -> Real x3 ->
                    RealLt x1 x2 p -> exl boole(
                    (boole -> x3<<=x2) andi ((boole -> F) -> x1<<=x3)))")
(assume "x1" "x2" "x3" "p" "Rx1" "Rx2" "Rx3" "x1<x2")
(assert "x3<<=x2 oru x1<<=x3")
 (use "ApproxSplit" (pt "p"))
 (use "Rx1")
 (use "Rx2")
 (use "Rx3")
 (use "x1<x2")
(assume "Disj")
(elim "Disj")
(drop "Disj")
(assume "x3<=x2")
(intro 0 (pt "True"))
(split)
(assume "Useless")
(use "x3<=x2")
(assume "Absurd")
(use "EfRealLe")
(use "Absurd")
(use "Truth")
;; 11
(assume "x1<=x3")
(intro 0 (pt "False"))
(split)
(assume "Absurd")
(use "EfRealLe")
(use "Absurd")
(assume "Useless")
(use "x1<=x3")
;; Proof finished.
;; (cdp)
(save "ApproxSplitBoole")

(add-sound "ApproxSplitBoole")

;; ok, ApproxSplitBooleSound has been added as a new theorem:

;; allnc x,x0,x1,p(
;;  Real x -> 
;;  Real x0 -> 
;;  Real x1 -> 
;;  RealLt x x0 p -> 
;;  (ExLTMR (cterm (boole) (boole -> x1<<=x0) andnc ((boole -> F) -> x<<=x1)))
;;  (cApproxSplitBoole x x0 x1 p))

;; with computation rule

;; cApproxSplitBoole eqd cApproxSplitPos

;; We do not deanimate ApproxSplitBoole since the extracted term is short.

;; We first prove an auxiliary lemma IVTAux, for the construction step.

;; First we define a (formally inductive) correctness predicate:

(add-ids
 (list (list "Corr" (make-arity (py "cont") (py "rat") (py "rat") (py "pos"))))
 '("all f,c,d,p(
     f doml<=c -> d<=f domr -> c+(1#2**p)<=d ->
     f c<<=0 -> 0<<=f d ->
     Corr f c d p)" "CorrIntro"))

;; Now the properties of Corr.

(set-goal "all f,c,d,p(Corr f c d p -> f doml<=c)")
(assume "f" "c" "d" "p")
(elim)
(search)
(save "CorrElim1")

(set-goal "all f,c,d,p(Corr f c d p -> d<=f domr)")
(assume "f" "c" "d" "p")
(elim)
(search)
(save "CorrElim2")

(set-goal "all f,c,d,p(Corr f c d p -> c+(1#2**p)<=d)")
(assume "f" "c" "d" "p")
(elim)
(search)
(save "CorrElim3")

(set-goal "all f,c,d,p(Corr f c d p -> f c<<=0)")
(assume "f" "c" "d" "p")
(elim)
(search)
(save "CorrElim4")

(set-goal "all f,c,d,p(Corr f c d p -> 0<<=f d)")
(assume "f" "c" "d" "p")
(elim)
(search)
(save "CorrElim5")

;; We also will use a corollary to CorrElim3
;; CorrElim3Cor
(set-goal "all f,c,d,p(Corr f c d p -> c<=d)")
(assume "f" "c" "d" "p" "CorrHyp")
(use "RatLeTrans" (pt "c+(1#2**p)"))
(use "RatLeTrans" (pt "c+0"))
(use "Truth")
(use "RatLeMonPlus")
(use "Truth")
(use "Truth")
(use "CorrElim3" (pt "f"))
(use "CorrHyp")
;; Proof finished.
(save "CorrElim3Cor")

;; RatTwoTimes
(set-goal "all a 2*a==a+a")
(simp (pf "(2#1)=RatPlus 1 1"))
(assume "a")
(simprat "RatTimesPlusDistrLeft")
(ng)
(use "Truth")
(use "Truth")
;; Proof fnished.
(save "RatTwoTimes")

;; RatThreeTimes
(set-goal "all a 3*a==a+a+a")
(simp (pf "(3#1)=RatPlus(RatPlus 1 1)1"))
(assume "a")
(simprat "RatTimesPlusDistrLeft")
(simprat "RatTimesPlusDistrLeft")
(use "Truth")
(use "Truth")
;; Proof fnished.
(save "RatThreeTimes")

;; RatFourTimes
(set-goal "all a 4*a==a+a+a+a")
(simp (pf "(4#1)=RatPlus(RatPlus(RatPlus 1 1)1)1"))
(assume "a")
(simprat "RatTimesPlusDistrLeft")
(simprat "RatTimesPlusDistrLeft")
(simprat "RatTimesPlusDistrLeft")
(use "Truth")
(use "Truth")
;; Proof fnished.
(save "RatFourTimes")

;; RatThreeTwoTimes
(set-goal "all a 3*a==2*a+a")
(assume "a")
(simprat "RatTwoTimes")
(use "RatThreeTimes")
;; Proof finished.
;; (cp)
(save "RatThreeTwoTimes")

;; RatFourThreeTimesL
(set-goal "all a 4*a==3*a+a")
(assume "a")
(simprat "RatThreeTimes")
(use "RatFourTimes")
;; Proof finished.
;; (cp)
(save "RatFourThreeTimesL")

;; RatFourThreeTimesR
(set-goal "all a 4*a==a+3*a")
(assume "a")
(simprat "RatThreeTimes")
(use "RatFourTimes")
;; Proof finished.
;; (cp)
(save "RatFourThreeTimesR")

(pp "PosExpTwoPosPlus")
;; all p,q 2**p*2**q=2**(p+q)

;; RatOneOverExpTwoPosS
(set-goal "all p (1#2**PosS p)=(1#2)*(1#2**p)")
(assume "p")
(ng)
(simp "<-" "PosPlus0RewRule")
(simp "<-" "PosExpTwoPosPlus")
(use "Truth")
;; Proof finished.
;; (cp)
(save "RatOneOverExpTwoPosS")

;; RatEqvMinusMinus
(set-goal "all a,b,c,d(b+c==a+d -> b+ ~a==d+ ~c)")
(assume "a" "b" "c" "d" "PlusEq")
(use "RatEqvPlusCancelR" (pt "a"))
(simprat "RatEqvPlusMinus")
(simp (pf "d+ ~c+a=a+(d+ ~c)"))
(simp "RatPlusAssoc")
(use "RatEqvPlusCancelR" (pt "c"))
(simprat "RatEqvPlusMinus")
(use "PlusEq")
(use "RatPlusComm")
;; Proof finished.
;; (cp)
(save "RatEqvMinusMinus")

;; ArgIncrLL
(set-goal "all c,d,p(c+(1#2**p)<=d -> c+(1#2**PosS(PosS p))<=(1#4)*(3*c+d))")
(assume "c" "d" "p" "LeHyp")
(simprat (pf "(1#2**PosS(PosS p))==(1#4)*(1#2**p)"))
(use "RatLeTimesCancelL" (pt "(4#1)"))
(use "Truth")
(simprat "RatTimesPlusDistr")
(simp "RatTimesAssoc")
(ng #t)
(simprat "RatFourThreeTimesL")
(simp "<-" "RatPlusAssoc")
(use "RatLeMonPlus")
(use "Truth")
(use "LeHyp")
;; ?^4:(1#2**PosS(PosS p))==(1#4)*(1#2**p)
(simp "RatOneOverExpTwoPosS")
(simp "RatOneOverExpTwoPosS")
(use "Truth")
;; Proof finished.
;; (cp)
(save "ArgIncrLL")

;; ArgIncrLLWeak
(set-goal "all c,d(c<=d -> c<=(1#4)*(3*c+d))")
(assume "c" "d" "c<=d")
(use "RatLeTrans" (pt "(1#4)*(4*c)"))
(use "Truth")
(use "RatLeTimesCancelL" (pt "4#1"))
(use "Truth")
(ng #t)
(simprat "RatFourThreeTimesL")
(use "RatLeMonPlus")
(use "RatLeMonTimesR")
(use "Truth")
(use "Truth")
(use "c<=d")
;; Proof finished.
;; (cp)
(save "ArgIncrLLWeak")

;; ArgIncrL
(set-goal "all c,d,p(
 c+(1#2**p)<=d -> (1#4)*(3*c+d)+(1#2**PosS(PosS p))<=(1#2)*(c+d))")
(assume "c" "d" "p" "LeHyp")
(simprat (pf "(1#2**PosS(PosS p))==(1#4)*(1#2**p)"))
(simprat "<-" "RatTimesPlusDistr")
(use "RatLeTimesCancelL" (pt "4#1"))
(use "Truth")
(ng #t)
(simprat "RatTimesPlusDistr")
(simprat "RatThreeTwoTimes")
(simp "<-" "RatPlusAssoc")
(simp "<-" "RatPlusAssoc")
(use "RatLeMonPlus")
(use "Truth")
(simp (pf "d+(1#2**p)=(1#2**p)+d"))
(simprat "RatTwoTimes")
(simp "RatPlusAssoc")
(use "RatLeMonPlus")
(use "LeHyp")
(use "Truth")
(use "RatPlusComm")
;; ?^4:(1#2**PosS(PosS p))==(1#4)*(1#2**p)
(simp "RatOneOverExpTwoPosS")
(simp "RatOneOverExpTwoPosS")
(use "Truth")
;; Proof finished.
;; (cp)
(save "ArgIncrL")

;; ArgIncrR
(set-goal "all c,d,p(
 c+(1#2**p)<=d -> (1#2)*(c+d)+(1#2**PosS(PosS p))<=(1#4)*(c+3*d))")
(assume "c" "d" "p" "LeHyp")
(simprat (pf "(1#2**PosS(PosS p))==(1#4)*(1#2**p)"))
(simprat (pf "(1#2)==(1#4)*2"))
(simp "<-" "RatTimesAssoc")
(simprat "<-" "RatTimesPlusDistr")
(use "RatLeMonTimesR")
(use "Truth")
(simprat "RatTimesPlusDistr")
(simprat "RatThreeTwoTimes")
(simp "<-" "RatPlusAssoc")
(simprat (pf "2*c==c+c"))
(simp "<-" "RatPlusAssoc")
(use  "RatLeMonPlus")
(use "Truth")
(simp "RatPlusAssoc")
(simp (pf "c+2*d=2*d+c"))
(simp "<-" "RatPlusAssoc")
(use  "RatLeMonPlus")
(use "Truth")
(use "LeHyp")
(use "RatPlusComm")
(use "RatTwoTimes")
(use "Truth")
;; ?^4:(1#2**PosS(PosS p))==(1#4)*(1#2**p)
(simp "RatOneOverExpTwoPosS")
(simp "RatOneOverExpTwoPosS")
(use "Truth")
;; Proof finished.
;; (cp)
(save "ArgIncrR")

;; ArgIncrRR
(set-goal "all c,d,p(c+(1#2**p)<=d -> (1#4)*(c+3*d)+(1#2**PosS(PosS p))<=d)")
(assume "c" "d" "p" "LeHyp")
(simprat (pf "(1#2**PosS(PosS p))==(1#4)*(1#2**p)"))
(use "RatLeTimesCancelL" (pt "(4#1)"))
(use "Truth")
(simprat "RatTimesPlusDistr")
(simp "RatTimesAssoc")
(simp "RatTimesAssoc")
(ng #t)
(simprat "RatFourThreeTimesL")
(simp (pf "c+3*d=3*d+c"))
(simp "<-" "RatPlusAssoc")
(use "RatLeMonPlus")
(use "Truth")
(use "LeHyp")
(use "RatPlusComm")
;; ?^4:(1#2**PosS(PosS p))==(1#4)*(1#2**p)
(simp "RatOneOverExpTwoPosS")
(simp "RatOneOverExpTwoPosS")
(use "Truth")
;; Proof finished.
;; (cp)
(save "ArgIncrRR")

;; ArgIncrRRWeak
(set-goal "all c,d(c<=d -> (1#4)*(c+3*d)<=d)")
(assume "c" "d" "c<=d")
(use "RatLeTrans" (pt "(1#4)*(4*d)"))
(use "RatLeTimesCancelL" (pt "4#1"))
(use "Truth")
(ng #t)
(simp "RatPlusComm")
(simprat "RatFourThreeTimesL")
(use "RatLeMonPlus")
(use "Truth")
(use "c<=d")
(use "Truth")
;; Proof finished.
;; (cp)
(save "ArgIncrRRWeak")

;; IVTAux1
(set-goal "all f,c,d,p(Cont f -> Corr f c d p -> 0<<=f((1#2)*(c+d)) ->
                       Corr f c((1#2)*(c+d))(PosS p))")
(assume "f" "c" "d" "p" "Cont f" "Corr f c d p" "0<<=f d1")
(cut "f doml<=c")
(assume "a<=c")
(cut "d<=f domr")
(assume "d<=b")
(cut "c+(1#2**p)<=d")
(assume "c<_p d")
(cut "f c<<=0")
(assume "f c<<=0")
(cut "0<<=f d")
(assume "0<<=f d")
;; ?^17:Corr f c((1#2)*(c+d))(PosS p)
(use "CorrIntro")
(auto)
;; ?^19:(1#2)*(c+d)<=f domr
(use "RatLeTrans" (pt "(1#2)*(d+d)"))
(use "RatLeMonTimesR")
(use "Truth")
(use "RatLeMonPlus")
(use "RatLeTrans" (pt "c+(1#2**p)"))
(use "Truth")
(use "CorrElim3" (pt "f"))
(use "Corr f c d p")
(use "Truth")
;; ?^24:(1#2)*(d+d)<=f domr
(simprat "<-" "RatTwoTimes")
(ng #t)
(use "d<=b")
;; ?^20:c+(1#2**PosS p)<=(1#2)*(c+d)
(simp "RatOneOverExpTwoPosS")
(use "RatLeTimesCancelL" (pt "2#1"))
(use "Truth")
(simprat "RatTimesPlusDistr")
(simp "RatTimesAssoc")
(simp "RatTimesAssoc")
(ng #t)
(simprat "RatTwoTimes")
(simp "<-" "RatPlusAssoc")
(use "RatLeMonPlus")
(use "Truth")
(use "c<_p d")
;; ?^21:f c<<=0
(use "f c<<=0")
;; ?^22:0<<=f((1#3)*(c+d+d))
(use "0<<=f d1")
;; ?^16:0<<=f d
(use-with "CorrElim5" (pt "f") (pt "c") (pt "d") (pt "p") "Corr f c d p")
;; ?^13:f c<<=0
(use-with "CorrElim4" (pt "f") (pt "c") (pt "d") (pt "p") "Corr f c d p")
(use-with "CorrElim3" (pt "f") (pt "c") (pt "d") (pt "p") "Corr f c d p")
(use-with "CorrElim2" (pt "f") (pt "c") (pt "d") (pt "p") "Corr f c d p")
(use-with "CorrElim1" (pt "f") (pt "c") (pt "d") (pt "p") "Corr f c d p")
;; Proof finished.
;; (cp)
(save "IVTAux1")

;; IVTAux2
(set-goal "all f,c,d,p(
 Cont f -> 
 Corr f c d p ->
 f((1#4)*(3*c+d))<<=0 ->
 0<<=f((1#4)*(c+3*d)) ->
 Corr f((1#4)*(3*c+d))((1#4)*(c+3*d))(PosS p))")
(assume "f" "c" "d" "p" "Cont f" "Corr f c d p" "fb1<=0" "0<=fb2")
(cut "f doml<=c")
(assume "a<=c")
(cut "d<=f domr")
(assume "d<=b")
(cut "c+(1#2**p)<=d")
(assume "c<_p d")
(cut "f c<<=0")
(assume "f c<<=0")
(cut "0<<=f d")
(assume "0<<=f d")
;; ?^17:Corr f((1#4)*(3*c+d))((1#4)*(c+3*d))(PosS p)
(use "CorrIntro")
;; ?^18:f doml<=(1#4)*(3*c+d)
(use "RatLeTrans" (pt "c"))
(use "a<=c")
(use "RatLeTrans" (pt "(1#4)*(3*c+c)"))
(simprat "<-" "RatFourThreeTimesL")
(use "Truth")
(use "RatLeMonTimesR")
(use "Truth")
(use "RatLeMonPlus")
(use "Truth")
(use "RatLeTrans" (pt "c+(1#2**p)"))
(use "Truth")
(use "c<_p d")
;; ?^19:(1#4)*(c+3*d)<=f domr
(use "RatLeTrans" (pt "d"))
(use "RatLeTrans" (pt "(1#4)*(d+3*d)"))
(use "RatLeMonTimesR")
(use "Truth")
(use "RatLeMonPlus")
(use "RatLeTrans" (pt "c+(1#2**p)"))
(use "Truth")
(use "c<_p d")
(use "Truth")
(simprat "RatThreeTimes")
(ng #t)
(simprat "<-" "RatFourTimes")
(use "Truth")
(use "d<=b")
;; ?^20:(1#4)*(3*c+d)+(1#2**PosS p)<=(1#4)*(c+3*d)
(simprat (pf "(1#2**PosS p)==(1#2**PosS(PosS p))+(1#2**PosS(PosS p))"))
(simp "RatPlusAssoc")
(use "RatLeTrans" (pt "(1#2)*(c+d)+(1#2**PosS(PosS p))"))
(use "RatLeTrans" (pt "(1#2)*(c+d)+(1#2**PosS(PosS p))"))
(use "RatLeMonPlus")
(use "ArgIncrL")
(use "c<_p d")
(use "Truth")
(use "Truth")
;; (use "RatLeMonPlus")
;; (use "Truth")
;; (use "Truth")
(use "ArgIncrR")
(use "c<_p d")
;; ?^48:(1#2**PosS p)==(1#2**PosS(PosS p))+(1#2**PosS(PosS p))
(assert "(1#2**PosS(PosS p))==(1#4)*(1#2**p)") ;make it a lemma?
(simp "RatOneOverExpTwoPosS")
(simp "RatOneOverExpTwoPosS")
(use "Truth")
;; Assertion proved.
(assume "Assertion")
(simprat "Assertion")
(simprat "<-" "RatTimesPlusDistr")
(simp "RatOneOverExpTwoPosS")
(ng #t)
(use "SZeroPosPlus")
;; ?^21:f((1#4)*(3*c+d))<<=0
(use "fb1<=0")
;; ?^22:0<<=f((1#4)*(c+3*d))
(use "0<=fb2")
;; ?^16:0<<=f d
(use-with "CorrElim5" (pt "f") (pt "c") (pt "d") (pt "p") "Corr f c d p")
;; ?^13:f c<<=0
(use-with "CorrElim4" (pt "f") (pt "c") (pt "d") (pt "p") "Corr f c d p")
(use-with "CorrElim3" (pt "f") (pt "c") (pt "d") (pt "p") "Corr f c d p")
(use-with "CorrElim2" (pt "f") (pt "c") (pt "d") (pt "p") "Corr f c d p")
(use-with "CorrElim1" (pt "f") (pt "c") (pt "d") (pt "p") "Corr f c d p")
;; Proof finished.
;; (cp)
(save "IVTAux2")

;; IVTAux3
(set-goal "all f,c,d,p(
 Cont f -> 
 Corr f c d p -> f((1#2)*(c+d))<<=0 -> Corr f((1#2)*(c+d))d(PosS p))")
;; Proof should be similar to IVTAux1
(assume "f" "c" "d" "p" "Cont f" "Corr f c d p" "0<<=f d1")
(cut "f doml<=c")
(assume "a<=c")
(cut "d<=f domr")
(assume "d<=b")
(cut "c+(1#2**p)<=d")
(assume "c<_p d")
(cut "f c<<=0")
(assume "f c<<=0")
(cut "0<<=f d")
(assume "0<<=f d")
;; ?^17:Corr f((1#2)*(c+d))d(PosS p)
(use "CorrIntro")
;; ?^18:f doml<=(1#2)*(c+d)
(use "RatLeTrans" (pt "(1#2)*(c+c)"))
(use "RatLeTrans" (pt "c"))
(use "a<=c")
(simprat "<-" "RatTwoTimes")
(use "Truth")
;; ?^24:(1#2)*(c+c)<=(1#2)*(c+d)
(use "RatLeMonTimesR")
(use "Truth")
(use "RatLeMonPlus")
(use "Truth")
(use "RatLeTrans" (pt "c+(1#2**p)"))
(use "Truth")
(use "c<_p d")
;; ?^19:d<=f domr
(use-with "CorrElim2" (pt "f") (pt "c") (pt "d") (pt "p") "Corr f c d p")
;; ?^20:(1#2)*(c+d)+(1#2**PosS p)<=d
(simp "RatOneOverExpTwoPosS")
(simprat "<-" "RatTimesPlusDistr")
(simp (pf "c+d=d+c"))
(use "RatLeTrans" (pt "(1#2)*(2*d)"))
(simprat "RatTwoTimes")
(use "RatLeTimesCancelL" (pt "2#1"))
(use "Truth")
(simp "RatTimesAssoc")
(simp "RatTimesAssoc")
(ng #t)
(simp "<-" "RatPlusAssoc")
(use "RatLeMonPlus")
(use "Truth")
(use "c<_p d")
(use "Truth")
(use "RatPlusComm")
;; ?^21:f((1#2)*(c+d))<<=0
(auto)
;; ?^16:0<<=f d
(use-with "CorrElim5" (pt "f") (pt "c") (pt "d") (pt "p") "Corr f c d p")
;; ?^13:f c<<=0
(use-with "CorrElim4" (pt "f") (pt "c") (pt "d") (pt "p") "Corr f c d p")
(use-with "CorrElim3" (pt "f") (pt "c") (pt "d") (pt "p") "Corr f c d p")
(use-with "CorrElim2" (pt "f") (pt "c") (pt "d") (pt "p") "Corr f c d p")
(use-with "CorrElim1" (pt "f") (pt "c") (pt "d") (pt "p") "Corr f c d p")
;; Proof finished.
;; (cp)
(save "IVTAux3")

;; (pp "IVTAux1")
;; (pp "IVTAux2")
;; (pp "IVTAux3")

;; IVTAux
(set-goal "all f,q(
     Cont f -> 
     f f doml<<=0 -> 
     0<<=f f domr -> 
     all c,d,p(
      f doml<=c -> d<=f domr -> c+(1#2**p)<=d -> RealLt(f c)(f d)(p+q)) -> 
     all p,c,d(
      Corr f c d p -> 
      exd c1 
       exl d1(
        Corr f c1 d1(PosS p) andnc 
        c<=c1 andnc d1<=d andnc d1+ ~c1==(1#2)*(d+ ~c))))")
(assume "f" "q" "Cont f" "f a<<=0" "0<<=f b" "HS" "p" "c" "d" "Corrfcdp")

(cut "exl b1 b1 eqd (1#4)*(3*c+d)")
(use "Id")
(assume "b1Ex")
(by-assume "b1Ex" "b1" "b1Def")

(cut "exl z1 z1 eqd f b1")
(use "Id")
(assume "z1Ex")
(by-assume "z1Ex" "z1" "z1Def")

(cut "exl b2 b2 eqd (1#2)*(c+d)")
(use "Id")
(assume "b2Ex")
(by-assume "b2Ex" "b2" "b2Def")

(cut "exl z2 z2 eqd f b2")
(use "Id")
(assume "z2Ex")
(by-assume "z2Ex" "z2" "z2Def")

(assert "f doml<=c")
(use "CorrElim1" (pt "d") (pt "p"))
(use "Corrfcdp")
(assume "a<=c")

(assert "d<=f domr")
(use "CorrElim2" (pt "c") (pt "p"))
(use "Corrfcdp")
(assume "d<=b")

(assert "c+(1#2**p)<=d")
(use "CorrElim3" (pt "f"))
(use "Corrfcdp")
(assume "c<_pd")

(assert "f c<<=0")
(use "CorrElim4" (pt "d") (pt "p"))
(use "Corrfcdp")
(assume "fc<=0")

(assert "0<<=f d")
(use "CorrElim5" (pt "c") (pt "p"))
(use "Corrfcdp")
(assume "0<=fd")

(drop "Corrfcdp")

(assert "c<=d")
(use "RatLeTrans" (pt "c+(1#2**p)"))
(use "Truth")
(use "c<_pd")
(assume "c<=d")

(assert "RealLt z1 z2(PosS(PosS p)+q)")
(simp "z1Def")
(simp "z2Def")
(use "HS")

;; ?^56:f doml<=b1
(use "RatLeTrans" (pt "c"))
(auto)
(simp "b1Def")
(use "ArgIncrLLWeak")
(auto)
(use "RatLeTrans" (pt "d"))
(simp "b2Def")
(use "RatLeTrans" (pt "(1#2)*(2*d)"))
(use "RatLeMonTimesR")
(use "Truth")
(simprat "RatTwoTimes")
(use "RatLeMonPlus")
(auto)

;; b1+(1#2**PosS(PosS p))<=b2
(simp "b1Def")
(simp "b2Def")
(use "ArgIncrL")
(use "c<_pd")
;; Assertion proved.
(assume "z1<z2")

(cut "exl boole((boole -> 0<<=z2) andnc ((boole -> F) -> z1<<=0))")
(assume "ExBooleHypL")
(by-assume "ExBooleHypL" "boole" "ExKernelL")
(cases (pt "boole"))

;; Case L
(assume "LeftL")
(assert "0<<=z2")
(use "ExKernelL")
(use "LeftL")
(assume "0<<=z2")
(intro 0 (pt "c"))
(intro 0 (pt "b2"))
;; ?^96:Corr f c b2(PosS p) andnc c<=c andnc b2<=d andnc b2+ ~c==(1#2)*(d+ ~c)
(split)
(intro 0)
(auto)
;; b2<=f domr
(use "RatLeTrans" (pt "d"))
(simp "b2Def")
;; (1#2)*(c+d)<=d
(use "RatLeTrans" (pt "(1#2)*(2*d)"))
(use "RatLeMonTimesR")
(use "Truth")
(simprat "RatTwoTimes")
(use "RatLeMonPlus")
(auto)
;; c+(1#2**PosS p)<=b2
(simprat (pf "(1#2**PosS p)==2*(1#2**PosS(PosS p))"))
(simprat "RatTwoTimes")
(simp "RatPlusAssoc")
(use "RatLeTrans" (pt "(1#4)*(3*c+d)+(1#2**PosS(PosS p))"))
(use "RatLeMonPlus")
(use "ArgIncrLL")
(use "c<_pd")
(use "Truth")
(simp "b2Def")
(use "ArgIncrL")
(use "c<_pd")
;; ?^115:(1#2**PosS p)==2*(1#2**PosS(PosS p))
(simprat (pf "(1#2**PosS(PosS p))==(1#2)*(1#2**PosS p)"))
(simp "RatTimesAssoc")
(use "Truth")
(simp "RatOneOverExpTwoPosS")
(auto)
(simp "<-" "z2Def")
(auto)
;; ?^98:c<=c andnc b2<=d andnc b2+ ~c==(1#2)*(d+ ~c)
(split)
(use "Truth")
(split)
(simp "b2Def")
;; ?^135:(1#2)*(c+d)<=d ;was proven already earlier
(use "RatLeTrans" (pt "(1#2)*(2*d)"))
(use "RatLeMonTimesR")
(use "Truth")
(simprat "RatTwoTimes")
(use "RatLeMonPlus")
(use "RatLeTrans" (pt "c+(1#2**p)"))
(auto)
;; ?^133:b2+ ~c==(1#2)*(d+ ~c)
(simp "b2Def")
(use "RatEqvTimesCancelL" (pt "(2#1)"))
(use "Truth")
(ng #t)
(simprat "RatTimesPlusDistr")
(ng #t)
(simprat "RatTwoTimes")
(ng #t)
(simp "<-" "RatPlusAssoc")
(simp "RatPlusComm")
(use "RatEqvPlusMinus")
;; ?_89:(boole -> F) -> 
;;      exd c0 
;;       exl d0(
;;        Corr f c0 d0(PosS p) andnc 
;;        c<=c0 andnc d0<=d andnc d0+ ~c0==(1#2)*(d+ ~c))
(assume "RightL")
(assert "z1<<=0")
(use "ExKernelL")
(use "RightL")
(drop "ExKernelL" "RightL")
(assume "z1<<=0")

(def "b3" "(1#4)*(c+3*d)")
(def "z3" "f b3")

(assert "RealLt z2 z3(PosS(PosS p)+q)")
(simp "z2Def")
(simp "z3Def")
(use "HS")

;; ?^178:f doml<=b2
(use "RatLeTrans" (pt "c"))
(auto)
(simp "b2Def")
(use "RatLeTrans" (pt "(1#2)*(2*c)"))
(use "Truth")
(simprat "RatTwoTimes")
(use "RatLeMonTimesR")
(auto)

;; ?^179:b3<=f domr
(use "RatLeTrans" (pt "d"))
(simp "b3Def")
(use "ArgIncrRRWeak")
(auto)

;; ?^180:b2+(1#2**PosS(PosS p))<=b3
(simp "b2Def")
(simp "b3Def")
(use "ArgIncrR")
(use "c<_pd")
;; Assertion proved.
(assume "z2<z3")

(cut "exl boole((boole -> 0<<=z3) andnc ((boole -> F) -> z2<<=0))")
(assume "ExBooleHypR")
(by-assume "ExBooleHypR" "boole2" "ExKernelR")
(cases (pt "boole2"))

;; Case M
(assume "Middle")
(assert "0<<=z3")
(use "ExKernelR")
(use "Middle")
(drop "ExKernelR" "Middle")
(assume "0<<=z3")
(intro 0 (pt "b1"))
(intro 0 (pt "b3"))
(split)
(intro 0)

;; f doml<=b1
(use "RatLeTrans" (pt "c"))
(auto)
(simp "b1Def")
(use "RatLeTrans" (pt "(1#4)*(4*c)"))
(use "Truth")
(use "RatLeMonTimesR")
(use "Truth")
(simprat "RatFourThreeTimesL")
(use "RatLeMonPlus")
(use "Truth")
(use "c<=d")

;; b3<=f domr
(use "RatLeTrans" (pt "d"))
(simp "b3Def")
(use "RatLeTrans" (pt "(1#4)*(4*d)"))
(use "RatLeMonTimesR")
(use "Truth")
(simprat "RatFourThreeTimesR")
(use "RatLeMonPlus")
(use "c<=d")
(auto)
;; b1+(1#2**PosS p)<=b3
(simprat (pf "(1#2**PosS p)==2*(1#2**PosS(PosS p))"))
(simprat "RatTwoTimes")
(simp "RatPlusAssoc")
(use "RatLeTrans" (pt "(1#2)*(c+d)+(1#2**PosS(PosS p))"))
(use "RatLeMonPlus")
(simp "b1Def")
(use "ArgIncrL")
(use "c<_pd")
(use "Truth")
(simp "b3Def")
(use "ArgIncrR")
(use "c<_pd")

;; (1#2**PosS p)==2*(1#2**PosS(PosS p))
(simprat (pf "(1#2**PosS(PosS p))==(1#2)*(1#2**PosS p)"))
(simp "RatTimesAssoc")
(use "Truth")
(simp "RatOneOverExpTwoPosS")
(use "Truth")

;; f b1<<=0
(simp "<-" "z1Def")
(auto)
(simp "<-" "z3Def")
(auto)

;; ?^214:c<=b1 andnc b3<=d andnc b3+ ~b1==(1#2)*(d+ ~c)
(split)
(simp "b1Def")
(use "ArgIncrLLWeak")
(use "c<=d")

;; ?^259:b3<=d andnc b3+ ~b1==(1#2)*(d+ ~c)
(split)
(simp "b3Def")
(use "ArgIncrRRWeak")
(use "c<=d")

;; ?^263:b3+ ~b1==(1#2)*(d+ ~c)
(simprat (pf "(1#2)*(d+ ~c)==(1#4)*(d+d)+ ~((1#4)*(c+c))"))
(simp "b3Def")
(simp "b1Def")
(use "RatEqvMinusMinus")
(simprat "<-" "RatTimesPlusDistr")
(simprat "<-" "RatTimesPlusDistr")
(use "RatTimesCompat")
(use "Truth")
(simp "RatPlusComm")
(ng #t)
(simprat "RatThreeTimes")
(simprat "RatThreeTimes")
(use "Truth")
;; (1#2)*(d+ ~c)==(1#4)*(d+d)+ ~((1#4)*(c+c))
(simprat "<-" "RatTwoTimes")
(simprat "<-" "RatTwoTimes")
(ng #t)
(simp "<-" "RatTimes3RewRule")
(use "RatTimesPlusDistr")

;; ?_204:(boole2 -> F) -> 
;;       exd c0 
;;        exl d0(
;;         Corr f c0 d0(PosS p) andnc 
;;         c<=c0 andnc d0<=d andnc d0+ ~c0==(1#2)*(d+ ~c))

;; Case R
(assume "RightR")
(assert "z2<<=0")
(use "ExKernelR")
(use "RightR")
(drop "ExKernelR" "RightR")
(assume "z2<<=0")
(intro 0 (pt "b2"))
(intro 0 (pt "d"))
;; ?^290:Corr f b2 d(PosS p) andnc c<=b2 andnc d<=d andnc d+ ~b2==(1#2)*(d+ ~c)
(split)
(intro 0)

;; f doml<=b2
(use "RatLeTrans" (pt "c"))
(auto)
;; c<=b2
(simp "b2Def")
;; c<=(1#2)*(c+d)
(use "RatLeTrans" (pt "(1#2)*(2*c)"))
(use "Truth")
(use "RatLeMonTimesR")
(use "Truth")
(simprat "RatTwoTimes")
(use "RatLeMonPlus")
(use "Truth")
(use "c<=d")

;; d<=f domr
(auto)

;; ?^295:b2+(1#2**PosS p)<=d
(simprat (pf "(1#2**PosS p)==2*(1#2**PosS(PosS p))"))
(simprat "RatTwoTimes")
(simp "RatPlusAssoc")
(use "RatLeTrans" (pt "(1#4)*(c+3*d)+(1#2**PosS(PosS p))"))
(use "RatLeMonPlus")
(simp "b2Def")
(use "ArgIncrR")
(use "c<_pd")
(use "Truth")
;; (1#4)*(c+3*d)+(1#2**PosS(PosS p))<=d
(use "ArgIncrRR")
(use "c<_pd")
;; (1#2**PosS p)==2*(1#2**PosS(PosS p)) same as goal 116
(simprat (pf "(1#2**PosS(PosS p))==(1#2)*(1#2**PosS p)"))
(simp "RatTimesAssoc")
(use "Truth")
(simp "RatOneOverExpTwoPosS")
(use "Truth")
;; f b2<<=0
(simp "<-" "z2Def")
(use "z2<<=0")
;; 0<<=f d
(auto)
;; ?^292:c<=b2 andnc d<=d andnc d-b2==(1#2)*(d-c)
(split)
(simp "b2Def")
(use "RatLeTrans" (pt "(1#2)*(2*c)"))
(use "Truth")
(use "RatLeMonTimesR")
(use "Truth")
(simprat "RatTwoTimes")
(use "RatLeMonPlus")
(use "Truth")
(use "c<=d")
(split)
(use "Truth")

;; ?^135:d+ ~b2==(1#2)*(d+ ~c)
(simprat (pf "(1#2)*(d+ ~c)==(1#2)*d+ ~(1#2)*c"))
(simp "b2Def")
(use "RatEqvMinusMinus")
(simp "RatPlusComm")
(simprat "RatTimesPlusDistr")
(simp "<-" "RatPlusAssoc")
(use "RatPlusCompat")
(use "Truth")
(simprat "<-" "RatTimesPlusDistr")
(simprat "<-" "RatTwoTimes")
(use "Truth")

;; (1#2)*(d+ ~c)==(1#2)*d+ ~(1#2)*c
(ng #t)
(simp "<-" "RatTimes3RewRule")
(simprat "<-" "RatTimesPlusDistr")
(use "Truth")
;; ?_198:exl boole((boole -> 0<<=z3) andnc ((boole -> F) -> z2<<=0))

(use "ApproxSplitBoole" (pt "PosS(PosS p)+q"))
(simp "z2Def")
(use "ContReal")
(auto)
(use "RatLeTrans" (pt "c"))
(auto)
(use "RatLeTrans" (pt "d"))
(auto)
(use "RealRat")
(simp "z3Def")
(use "ContReal")
(auto)
(use "RatLeTrans" (pt "c"))
(auto)
(use "RatLeTrans" (pt "d"))
(auto)
(use "RealRat")
(autoreal)
(use "z2<z3")

;; ?_83:exl boole((boole -> 0<<=z2) andnc ((boole -> F) -> z1<<=0))

(use "ApproxSplitBoole" (pt "PosS(PosS p)+q"))
(simp "z1Def")
(use "ContReal")
(auto)
(use "RatLeTrans" (pt "c"))
(auto)
(use "RatLeTrans" (pt "d"))
(auto)
(use "RealRat")
(simp "z2Def")
(use "ContReal")
(auto)
(use "RatLeTrans" (pt "c"))
(auto)
(use "RatLeTrans" (pt "d"))
(auto)
(use "RealRat")
(autoreal)
(use "z1<z2")

;; ?_25:exl z z eqd f b2
(intro 0 (pt "f b2"))
(intro 0)

;; ?_18:exl b b eqd(1#2)*(c+d)
(intro 0 (pt "(1#2)*(c+d)"))
(intro 0)

;; ?_11:exl z z eqd f b1
(intro 0 (pt "f b1"))
(intro 0)

;; ?_4:exl b b eqd(1#4)*(3*c+d)
(intro 0 (pt "(1#4)*(3*c+d)"))
(intro 0)
;; Proof finished.
;; (cp)
(save "IVTAux")

(define eterm (proof-to-extracted-term))
(define neterm (rename-variables (nt eterm)))
;; (pp neterm)

;; [f,p,p0,a,a0]
;;  [let a1
;;    ((1#4)*(3*a+a0))
;;    [let x
;;     (RealConstr(f approx(a1 max f doml min f domr))([p1]f uMod(PosS p1)))
;;     [let a2
;;      ((1#2)*(a+a0))
;;      [let x0
;;       (RealConstr(f approx(a2 max f doml min f domr))([p1]f uMod(PosS p1)))
;;       [if (cApproxSplitPos x x0 0(PosS(PosS(p0+p))))
;;        (a pair a2)
;;        [if (cApproxSplitPos x0
;;             (RealConstr(f approx((1#4)*(a+3*a0)max f doml min f domr))
;;              ([p1]f uMod(PosS p1)))
;;             0
;;             (PosS(PosS(p0+p))))
;;         (a1 pair(1#4)*(a+3*a0))
;;         (a2 pair a0)]]]]]]

(add-sound "IVTAux")

;; ok, IVTAuxSound has been added as a new theorem:

;; allnc f,q(
;;  Cont f -> 
;;  f f doml<<=0 -> 
;;  0<<=f f domr -> 
;;  all c,d,p(f doml<=c -> d<=f domr -> c+(1#2**p)<=d -> RealLt(f c)(f d)(p+q)) -> 
;;  allnc p,c,d(
;;   Corr f c d p -> 
;;   (ExDTMR (cterm (c0,a^) 
;;             (ExLTMR (cterm (d0) 
;;                       Corr f c0 d0(PosS p) andnc 
;;                       c<=c0 andnc d0<=d andnc d0+ ~c0==(1#2)*(d+ ~c)))
;;             a^))
;;   (cIVTAux f q p c d)))

;; with computation rule

;; cIVTAux eqd
;; ([f,p,p0,a,a0]
;;   [let a1
;;     ((1#4)*(3*a+a0))
;;     [let x
;;      (RealConstr(f approx(a1 max f doml min f domr))([p1]f uMod(PosS p1)))
;;      [let a2
;;       ((1#2)*(a+a0))
;;       [let x0
;;        (RealConstr(f approx(a2 max f doml min f domr))([p1]f uMod(PosS p1)))
;;        [if (cApproxSplitPos x x0 0(PosS(PosS(p0+p))))
;;         (a pair a2)
;;         [if (cApproxSplitPos x0
;;              (RealConstr(f approx((1#4)*(a+3*a0)max f doml min f domr))
;;               ([p1]f uMod(PosS p1)))
;;              0
;;              (PosS(PosS(p0+p))))
;;          (a1 pair(1#4)*(a+3*a0))
;;          (a2 pair a0)]]]]]])

(deanimate "IVTAux")

(add-var-name "cd" (py "rat yprod rat"))

;; IVTAuxPairs
(set-goal "all f,q(
     Cont f -> 
     f f doml<<=0 -> 
     0<<=f f domr -> 
     all c,d,p(
      f doml<=c -> d<=f domr -> c+(1#2**p)<=d -> RealLt(f c)(f d)(p+q)) -> 
     all p,cd(
      Corr f(lft cd)(rht cd)p -> 
      exl cd0(
       Corr f(lft cd0)(rht cd0)(PosS p) andnc 
       lft cd<=lft cd0 andnc 
       rht cd0<=rht cd andnc rht cd0+ ~lft cd0==(1#2)*(rht cd+ ~lft cd))))")
(assume "f" "q" "Cont f" "f a<<=0" "0<<=f b" "HS" "p" "cd" "Corrfcdp")
(assert "exd c1 
       exl d1(
        Corr f c1 d1(PosS p) andnc 
        lft cd<=c1 andnc d1<=rht cd andnc d1+ ~c1==(1#2)*(rht cd+ ~lft cd))")
(use "IVTAux" (pt "q"))
(auto)
(assume "ExHyp")
(by-assume "ExHyp" "c" "cProp")
(by-assume "cProp" "d" "cdProp")
(intro 0 (pt "c pair d"))
(ng #t)
(use "cdProp")
;; Proof finished.
;; (cp)
(save "IVTAuxPairs")

(define eterm (proof-to-extracted-term))
(define neterm (rename-variables (nt eterm)))
;; (pp neterm)

;; [f,p,p0,cd]cIVTAux f p p0 lft cd rht cd

(display-animation)

(add-sound "IVTAuxPairs")

;; ok, IVTAuxPairsSound has been added as a new theorem:

;; allnc f,q(
;;  Cont f -> 
;;  f f doml<<=0 -> 
;;  0<<=f f domr -> 
;;  all c,d,p(f doml<=c -> d<=f domr -> c+(1#2**p)<=d -> RealLt(f c)(f d)(p+q)) -> 
;;  allnc p,cd(
;;   Corr f(lft cd)(rht cd)p -> 
;;   (ExLTMR (cterm (cd0) 
;;             Corr f(lft cd0)(rht cd0)(PosS p) andnc 
;;             lft cd<=lft cd0 andnc 
;;             rht cd0<=rht cd andnc rht cd0+ ~lft cd0==(1#2)*(rht cd+ ~lft cd)))
;;   (cIVTAuxPairs f q p cd)))

;; with computation rule

;; cIVTAuxPairs eqd([f,p,p0,cd]cIVTAux f p p0 lft cd rht cd)

;; We leave IVTAuxPairs animated because it is short

;; IVTAuxSoundCor
(set-goal "allnc f,q(
 Cont f -> 
 f f doml<<=0 -> 
 0<<=f f domr -> 
 allnc c,d,p(
  f doml<=c -> d<=f domr -> c+(1#2**p)<=d -> RealLt(f c)(f d)(p+q)) -> 
 allnc p,cd(
  Corr f(lft cd)(rht cd)p -> 
  exnc cd0(cd0 eqd cIVTAuxPairs f q p cd andnc
   Corr f(lft cd0)(rht cd0)(PosS p) andnc 
   lft cd<=lft cd0 andnc 
   rht cd0<=rht cd andnc rht cd0+ ~lft cd0==(1#2)*(rht cd+ ~lft cd))))")
(assume "f" "q" "Cf" "fa<=0" "0<=fb" "HypSlope" "p" "cd" "CorrHyp")
(intro 0 (pt "cIVTAuxPairs f q p cd"))
(split)
(use "InitEqD")
(use-with
 "ExLTMRElim" (py "rat yprod rat")
 (make-cterm (pv "cd0")
	     (pf "Corr f(lft cd0)(rht cd0)(PosS p) andnc 
            lft cd<=lft cd0 andnc 
            rht cd0<=rht cd andnc rht cd0+ ~lft cd0==(1#2)*(rht cd+ ~lft cd)"))
 (pt "cIVTAuxPairs f q p cd")
 "?")
(use "IVTAuxPairsSound")
(auto)
;; Proof finished.
;; (cp)
(save "IVTAuxPairsSoundCor")

(add-var-name "xx" "yy" (py "alpha"))
(add-var-name "xxs" (py "nat=>alpha"))
(add-pvar-name "RR" (make-arity (py "nat") (py "alpha")))
(add-pvar-name "SS" (make-arity (py "nat") (py "alpha") (py "alpha")))
(add-var-name "g" (py "nat=>alpha=>alpha"))

;; DC
(set-goal "all xx0,g(
 RR^ Zero xx0 -> 
 all n,xx(RR^ n xx -> (RR^(Succ n)(g n xx) andnc SS^ n xx (g n xx))) -> 
 exl xxs(
  xxs Zero eqd xx0 andnc
  all n RR^ n(xxs n) andnc all n SS^ n(xxs n)(xxs(Succ n))))")
(assume "xx0" "g" "Init" "Step")
(intro 0 (pt "[n]((Rec nat=>alpha)n xx0 g)"))
(ng)
(split)
(use "InitEqD")
(assert "all xxs(all n xxs n eqd (Rec nat=>alpha)n xx0 g ->
 all n(RR^ n(xxs n) andnc RR^(n+1)(xxs(n+1)) andnc SS^ n(xxs n)(xxs(n+1))))")
(assume "xxs" "xxsDef")
(ind)
(split)
(simp "xxsDef")
(ng)
(use "Init")
;; 13
(split)
;; 16,17
(simp "xxsDef")
(ng)
(use "Step")
(use "Init")
;; 17
(simp "xxsDef")
(ng)
(simp "xxsDef")
(ng)
(use "Step")
(use "Init")
;; 11
(assume "n" "IH")
(split)
;; 27,28
(use "IH")
;; 28
(split)
(simp "xxsDef")
(ng)
(use "Step")
(simp "<-" "xxsDef")
(use "Step")
(use "IH")
;; 30
(simp "xxsDef")
(simp "xxsDef")
(ng)
(use "Step")
(simp "<-" "xxsDef")
(use "Step")
(use "IH")
;; Assertion proved.
(assume "Assertion")
(split)
(assume "n")
(use-with "Assertion" (pt "[n](Rec nat=>alpha)n xx0 g") "?" (pt "n") 'left)
(assume "n1")
(use "InitEqD")
;; 44
(assume "n")
(use-with "Assertion"
	  (pt "[n](Rec nat=>alpha)n xx0 g") "?" (pt "n") 'right 'right)
(assume "n1")
(use "InitEqD")
;; Proof finished.
;; (cp)
(save "DC")

(define eterm (proof-to-extracted-term))
(define DC-neterm (rename-variables (nt eterm)))
(pp DC-neterm)
;; [xx,g,n](Rec nat=>alpha)n xx g

(add-sound "DC")

;; ok, DCSound has been added as a new theorem:

;; allnc xx,g(
;;  RR^ Zero xx -> 
;;  all n,xx0(RR^ n xx0 -> RR^(Succ n)(g n xx0) andnc SS^ n xx0(g n xx0)) -> 
;;  (ExLTMR (cterm (xxs) 
;;            xxs Zero eqd xx andnc 
;;            all n RR^ n(xxs n) andnc all n SS^ n(xxs n)(xxs(Succ n))))
;;  ((cDC alpha)xx g))

;; with computation rule

;; (cDC alpha)eqd([xx,g,n](Rec nat=>alpha)n xx g)

;; We do not deanimate DC since the extracted term is short.

(add-var-name "cds" (py "nat=>rat yprod rat"))

;; NatPosNatPlusSucc
(set-goal "all p,n cNatPos(p+Succ n)=PosS(cNatPos(p+n))")
(assume "p" "n")
(simp "NatPosExFree")
(simp "NatPosExFree")
(use "NatToPosNatPlusSucc")
;; Proof finished.
;; (cp)
(save "NatPosNatPlusSucc")

;; IVTcds
(set-goal "all f,q,p0(
     Cont f -> 
     f f doml<<=0 -> 
     0<<=f f domr -> 
     f doml+(1#2**p0)<=f domr -> 
     all c,d,p(
      f doml<=c -> d<=f domr -> c+(1#2**p)<=d -> RealLt(f c)(f d)(p+q)) -> 
     exl cds(
      cds Zero eqd(f doml pair f domr) andnc 
      all n Corr f(lft(cds n))(rht(cds n))(cNatPos(p0+n)) andnc 
      all n(
       lft(cds n)<=lft(cds(Succ n)) andnc 
       rht(cds(Succ n))<=rht(cds n) andnc 
       rht(cds(Succ n))+ ~lft(cds(Succ n))==(1#2)*(rht(cds n)+ ~lft(cds n)))))")
(assume "f" "q" "p0" "Cont f" "f a<<=0" "0<<=f b" "a <_p0 b" "HypSlope")
(use-with
 "DC"
 (py "rat yprod rat")
 (make-cterm (pv "n") (pv "cd") (pf "Corr f(lft cd)(rht cd)(cNatPos(p0+n))"))
 (make-cterm (pv "n") (pv "cd") (pv "cd1")
	     (pf "lft cd<=lft cd1 andnc rht cd1<=rht cd andnc
                  rht cd1+ ~lft cd1==(1#2)*(rht cd+ ~lft cd)"))
 (pt "f doml pair f domr")
 (pt "[n,cd]cIVTAuxPairs f q(cNatPos(p0+n))cd")
 ;; (pt "[n,cd]cIVTAux f q p0 cd")
 "?" "?")
;; Corr f(lft(f doml pair f domr))(rht(f doml pair f domr))(cNatPos(p0+Zero))
(use "CorrIntro")
(use "Truth")
(use "Truth")
(simp "NatPlus0CompRule")
(simp "NatPosExFree")
(simp "NatToPosToNatId")
(use "a <_p0 b")
(use "f a<<=0")
(use "0<<=f b")

;; Now the step hypothesis, to be proved by means of IVTAuxPairs
(assume "n" "cd" "Corr-Hyp")
(simp "NatPosNatPlusSucc")
;; (split)
(inst-with-to
 "IVTAuxPairsSoundCor"
 (pt "f") (pt "q") "Cont f" "f a<<=0" "0<<=f b" "HypSlope"
 (pt "cNatPos(p0+n)") (pt "cd")
 "Corr-Hyp"
 "Inst")
(by-assume "Inst" "cd0" "cd0Prop")
(assert "cd0 eqd cIVTAuxPairs f q(cNatPos(p0+n))cd")
 (use "cd0Prop")
(assume "cd0Def")
(simp (pf "([n0,cd0]cIVTAuxPairs f q(cNatPos(p0+n0))cd0)n cd eqd
           cIVTAuxPairs f q(cNatPos(p0+n))cd"))
(simp "<-" "cd0Def")
(use "cd0Prop")
(use "InitEqD")
;; Proof finished.
;; (cp)
(save "IVTcds")

(define eterm (proof-to-extracted-term)) 
(define IVTcds-neterm (rename-variables (nt eterm)))
;; (pp IVTcds-neterm)

;; (pp "IVTcds")

(add-sound "IVTcds")

;; ok, IVTcdsSound has been added as a new theorem:

;; allnc f,q,p(
;;  Cont f -> 
;;  f f doml<<=0 -> 
;;  0<<=f f domr -> 
;;  f doml+(1#2**p)<=f domr -> 
;;  all c,d,p0(
;;   f doml<=c -> d<=f domr -> c+(1#2**p0)<=d -> RealLt(f c)(f d)(p0+q)) -> 
;;  (ExLTMR (cterm (cds) 
;;            cds Zero eqd(f doml pair f domr) andnc 
;;            all n Corr f(lft(cds n))(rht(cds n))(cNatPos(p+n)) andnc 
;;            all n(
;;             lft(cds n)<=lft(cds(Succ n)) andnc 
;;             rht(cds(Succ n))<=rht(cds n) andnc 
;;             rht(cds(Succ n))+ ~lft(cds(Succ n))==
;;             (1#2)*(rht(cds n)+ ~lft(cds n)))))
;;  (cIVTcds f q p))

;; with computation rule

;; cIVTcds eqd
;; ([f,p,p0,n]
;;   (Rec nat=>rat yprod rat)n(f doml pair f domr)
;;   ([n0,cd]cIVTAux f p(cNatPos(p0+n0))lft cd rht cd))

(deanimate "IVTcds")

;; We now prove that [p]lft(cds n+p) increases.

;; IVTLeftIncr
(set-goal "all f,q,p0(
     Cont f -> 
     f f doml<<=0 -> 
     0<<=f f domr -> 
     f doml+(1#2**p0)<=f domr -> 
     all c,d,p(
      f doml<=c -> d<=f domr -> c+(1#2**p)<=d -> RealLt(f c)(f d)(p+q)) -> 
     all cds(
      cds Zero eqd(f doml pair f domr) andnc 
      all n Corr f(lft(cds n))(rht(cds n))(cNatPos(p0+n)) andnc 
      all n(
       lft(cds n)<=lft(cds(Succ n)) andnc 
       rht(cds(Succ n))<=rht(cds n) andnc 
       rht(cds(Succ n))+ ~lft(cds(Succ n))==(1#2)*(rht(cds n)+ ~lft(cds n))) -> 
      all n,m lft(cds n)<=lft(cds(n+m))))")
(assume "f" "q" "p0" "Cont f" "f a<<=0" "0<<=f b" "a <_p0 b" "HypSlope"
	"cds" "Hcds" "n")
(ind)
(use "Truth")
(assume "m" "IH")
(use "RatLeTrans" (pt "lft(cds(n+m))"))
(use "IH")
(use "Hcds")
;; Proof finished.
;; (cp)
(save "IVTLeftIncr")

;; The corresponding proof of d(n+p)<=dn:

;; IVTRightDecr
(set-goal "all cds(
 all n rht(cds(Succ n))<=rht(cds n) -> 
 all n,m rht(cds(n+m))<=rht(cds n))")
(assume "cds" "Step" "n")
(ind)
(use "Truth")
(assume "m" "IH")
(use "RatLeTrans" (pt "rht(cds(n+m))"))
(auto)
;; Proof finished.
;; (cp)
(save "IVTRightDecr")

;; IVTDiff
(set-goal "all f,cds(
 cds Zero eqd(f doml pair f domr) -> 
 all n rht(cds(Succ n))+ ~lft(cds(Succ n))==
       (1#2)*(rht(cds n)+ ~lft(cds n)) -> 
 all n rht(cds n)+ ~lft(cds n)==(1#2**n)*(f domr+ ~f doml))")
(assume "f" "cds" "EqZero" "Step")
(ind)
  (simp "EqZero")
  (use "Truth")
(assume "n" "IH")
(simprat "Step")
(simprat "IH")
(use "Truth")
;; Proof finished.
;; (cp)
(save "IVTDiff")

;; We will need a general criterion for Cauchyness, in order to avoid
;; doing a symmetric argument twice, in a concrete case.  To be called
;; CauchyCrit.

;; CauchyCrit
(set-goal "all as,M(all p,n,m(M p<=n -> n<=m -> abs(as n+ ~(as m))<=(1#2**p)) ->
                    Cauchy as M)")
(assume "as" "M" "Hyp")
(use "CauchyIntro")
;; ?^3:allnc p,n,m(M p<=n -> M p<=m -> abs(as n+ ~(as m))<=(1#2**p))
(assume "p" "n" "m" "M p<=n" "M p<=m")
(use "NatLeLin" (pt "n") (pt "m"))
(assume "n<=m")
(auto)
;; m<=n -> abs(as n+ ~(as m))<=(1#2**p)
(assume "m<=n")
(simp "<-" "RatAbs0RewRule")
(ng #t)
(simp "RatPlusComm")
(use "Hyp")
(use "M p<=m")
(use "m<=n")
;; Proof finished.
;; (cdp)
(save "CauchyCrit")

;; Attempt l |-> p

;; IVTRealLeft
(set-goal 
 "all a,b,p0(0<=b+ ~a ->
 b+ ~a<=2**p0 -> 
 all cds(
  all n,m(n<=m -> lft(cds n)<=lft(cds m)) -> 
  all n,m(n<=m -> rht(cds m)<=rht(cds n)) -> 
  all n lft(cds n)<=rht(cds n) -> 
  all n rht(cds n)+ ~lft(cds n)==(1#2**n)*(b+ ~a) -> 
  Real(RealConstr([n]lft(cds n))([p]p+p0))))")
(assume "a" "b" "p0" "0<=b-a" "b-a<=2**p" "cds"
	"csIncr" "dsDecr" "cs<=ds" "cdDiff")
(use "RealIntro")
;; 3,4
;; Cauchyness
(use "CauchyCrit")
(ng #t)
;; ?^6:all p,n,m(p+l<=n -> n<=m -> abs(lft(cds n)+ ~lft(cds m))<=(1#2**p))
(assume "p" "n" "m" "MBd" "n<=m")
;; ?^7:abs(lft(cds n)+ ~lft(cds m))<=(1#2**p)
(simprat (pf "abs(lft(cds n)+ ~lft(cds m))==lft(cds m)+ ~lft(cds n)"))
;; ?^8:lft(cds m)+ ~lft(cds n)<=(1#2**p)
(use "RatLeTrans" (pt "rht(cds n)+ ~lft(cds n)"))
(ng #t)
(use "RatLeTrans" (pt "rht(cds m)"))
(use "cs<=ds")
(use "dsDecr")
(use "n<=m")
(simprat "cdDiff")
(simprat (pf "(1#2**p)==(1#2**(p+p0))*2**p0"))
(use "RatLeMonTimesTwo")
(use "Truth")
(use "0<=b-a")
;; ?^21:(1#2**n)<=(1#2**(p+p0))
(ng #t)
(use "NatLeMonTwoExp")
(use "MBd")
(use "b-a<=2**p")
;; ?^18:(1#2**p)==(1#2**(p+l))*2**p0
(simp "<-" "PosExpTwoPosPlus")
(use "PosTimesComm")
;; ?^9:abs(lft(cds n)+ ~lft(cds m))==lft(cds m)+ ~lft(cds n)
(simp (pf "abs(lft(cds n)+ ~lft(cds m))=abs(~(lft(cds n)+ ~lft(cds m)))"))
(ng #t)
(simp "RatPlusComm")
(simp "RatAbsId")
(use "Truth")
(use "RatLePlusCancelR" (pt "lft(cds n)"))
(simprat "RatEqvPlusMinus")
(use "csIncr")
(use "n<=m")
(simp "RatAbs0RewRule")
(use "Truth")
;; ?^4:Mon((RealConstr([n]lft(cds n))([p]p+l))mod)
(use "MonIntro")
(ng #t)
(assume "p" "q" "p<=q")
(simp "PosToNatLe")
(use "p<=q")
;; Proof finished.
;; (cp)
(save "IVTRealLeft")

;; The final goal, split into parts:
;; IVTFinalRealLeft
(set-goal "all f,q,p0(
     Cont f -> 
     f f doml<<=0 -> 
     0<<=f f domr -> 
     f doml+(1#2**p0)<=f domr -> 
     f domr-f doml<=2**p0  ->
     all c,d,p(
      f doml<=c -> d<=f domr -> c+(1#2**p)<=d -> RealLt(f c)(f d)(p+q)) -> 
     all cds(
      cds Zero eqd(f doml pair f domr) ->
      all n Corr f(lft(cds n))(rht(cds n))(cNatPos(p0+n)) ->
      all n(lft(cds n)<=lft(cds(Succ n))) ->
      all n(rht(cds(Succ n))<=rht(cds n)) ->
      all n(
       rht(cds(Succ n))+ ~lft(cds(Succ n))==(1#2)*(rht(cds n)+ ~lft(cds n))) ->
      Real(RealConstr([n]lft(cds n))([p]PosToNat(p+p0)))))")
(assume "f" "q" "p0" "Cont f" "f a<<=0" "0<<=f b" "a <_p0 b" "b-a<=2**p0" 
	"HypSlope" "cds"
	"cdsProp1" "cdsProp2" "cdsProp3" "cdsProp4" "cdsProp5")
(use "IVTRealLeft" (pt "f doml") (pt "f domr"))

;; ?^3:0<=f domr+ ~f doml
(use "RatLePlusCancelR" (pt "f doml"))
(simprat "RatEqvPlusMinus")
(use "RatLeTrans" (pt "f doml+(1#2**p0)"))
(use "Truth")
(use "a <_p0 b")
(use "b-a<=2**p0")
;; ?^5:all n,m(n<=m -> lft(cds n)<=lft(cds m))
(assume "n" "m" "n<=m")
(simp (pf "m=n+(m--n)"))
(use "IVTLeftIncr" (pt "f") (pt "q") (pt "p0"))
(auto)
(split)
(auto)
(split)
(auto)
(assume "n1")
(split)
(auto)
(split)
(auto)
(simp "NatPlusMinus")
(simp "<-" "NatMinusPlus")
(use "Truth")
(use "Truth")
(use "n<=m")
;; 6
(assume "n" "m" "n<=m")
(simp (pf "m=n+(m--n)"))
(use "IVTRightDecr")
(assume "n1")
(use "cdsProp4")
(simp "NatPlusComm")
(simp "NatMinusPlusEq")
(use "Truth")
(use "n<=m")
(assume "n")
(use "CorrElim3Cor" (pt "f") (pt "cNatPos(p0+n)"))
(use "cdsProp2")
;; ?^8:all n rht(cds n)-lft(cds n)=(2#3)**n*(f domr-f doml)
(use "IVTDiff")
;; 45
(use "cdsProp1")
(use "cdsProp5")
;; Proof finished.
;; (cdp)
(save "IVTFinalRealLeft")

;; IVTRealAppLeft
(set-goal 
 "all f,q,p(
 Cont f -> 
 f f doml<<=0 -> 
 0<<=f f domr -> 
 f doml+(1#2**p)<=f domr -> 
 f domr+ ~f doml<=2**p -> 
 all c,d,p(f doml<=c -> d<=f domr -> c+(1#2**p)<=d -> RealLt(f c)(f d)(p+q)) -> 
 all cds(
  cds Zero eqd(f doml pair f domr) -> 
  all n Corr f(lft(cds n))(rht(cds n))(cNatPos(p+n)) -> 
  all n lft(cds n)<=lft(cds(Succ n)) -> 
  all n rht(cds(Succ n))<=rht(cds n) -> 
  all n rht(cds(Succ n))-lft(cds(Succ n))==(1#2)*(rht(cds n)+ ~lft(cds n)) -> 
  Real(f(RealConstr([n]lft(cds n))([p0]PosToNat(p0+p))))))")
(assume "f" "q" "p" "Cont f" "f a<<=0" "0<<=f b"
	"a <_p b" "b-a<=2**p" "HypSlope" 
        "cds" "cdsProp1" "cdsProp2" "cdsProp3" "cdsProp4" "cdsProp5")
(use "ContReal")
(use "Cont f")
;; ?^4:f doml<=f domr
(use "RatLeTrans" (pt "f doml+(1#2**p)"))
(use "RatLeTrans" (pt "f doml+0"))
(use "Truth")
(use "RatLeMonPlus")
(use "Truth")
(use "Truth")
(use "a <_p b")
;; ?^5:Real(RealConstr([n]lft(cds n))([p0]PosToNat(p0+p)))
(use "IVTFinalRealLeft" (pt "f") (pt "q"))
(auto)
;; Proof finished.
;; (cdp)
(save "IVTRealAppLeft")

;; LeContAppZero
(set-goal "all f,x(Cont f -> Real x -> all m f(x seq m)<<=0 ->
 all n f doml<=x seq n ->
 all n x seq n<=f domr ->
 f x<<=0)")
(assume "f" "x" "Cf" "Rx" "LeZeroHyp" "LBd" "UBd")
(use "RealLeChar2RealConstrFree")
(use "ContReal")
(use "Cf")
(use "RatLeTrans" (pt "x seq Zero"))
(use "LBd")
(use "UBd")
(use "Rx")
(use "RealRat")
;; ?^5:all p exnc n all n0(n<=n0 -> (f x)seq n0<=0 seq n0+(1#2**p))
(assume "p")
(assert "exi m m=x mod(PosPred(f uModCont(PosS p)))")
 (intro 0 (pt "x mod(PosPred(f uModCont(PosS p)))"))
 (use "Truth")
(assume "mEx")
(by-assume "mEx" "m" "mDef")
(inst-with-to "LeZeroHyp" (pt "m") "LeZeroHypInst")
(inst-with-to "RealLeChar1RealConstrFree"
	      (pt "f(x seq m)")
	      (pt "RealConstr([n](0#1))([p]Zero)")
	      "Inst")
(inst-with-to "Inst" "LeZeroHypInst" "AllExProp")
(inst-with-to "AllExProp" (pt "PosS p") "ExHyp")
(drop "LeZeroHyp" "Inst" "LeZeroHypInst" "AllExProp")
(by-assume "ExHyp" "n1" "n1Prop")
(assert "exi n n=n1 max m max f uMod(PosS p)")
 (intro 0 (pt "n1 max m max f uMod(PosS p)"))
 (use "Truth")
(assume "nEx")
(by-assume "nEx" "n" "nDef")
(intro 0 (pt "n"))
(assume "n0" "n<=n0")
;;   f  x  Cf:Cont f
;;   Rx:Real x
;;   LBd:all n f doml<=x seq n
;;   UBd:all n x seq n<=f domr
;;   p  m  mDef:m=x mod(PosPred(f uModCont(PosS p)))
;;   n1  n1Prop:all n(n1<=n -> (f(x seq m))seq n<=0 seq n+(1#2**PosS p))
;;   n  nDef:n=n1 max m max f uMod(PosS p)
;;   n0  n<=n0:n<=n0
;; -----------------------------------------------------------------------------
;; ?^39:(f x)seq n0<=0 seq n0+(1#2**p)

(ng #t)
(simp "RatMaxMinEq")
;;   f  x  Cf:Cont f
;;   Rx:Real x
;;   LBd:all n f doml<=x seq n
;;   UBd:all n x seq n<=f domr
;;   p  m  mDef:m=x mod(PosPred(f uModCont(PosS p)))
;;   n1  n1Prop:all n(n1<=n -> (f(x seq m))seq n<=0 seq n+(1#2**PosS p))
;;   n  nDef:n=n1 max m max f uMod(PosS p)
;;   n0  n<=n0:n<=n0
;; -----------------------------------------------------------------------------
;; ?^41:f approx(x seq n0)n0<=(1#2**p)
(simprat (pf "f approx(x seq n0)n0==
 f approx(x seq n0)n0+ ~(f approx(x seq m)n0)+(f approx(x seq m)n0)"))
(get 45)
(simprat "RatEqvPlusMinus")
(use "Truth")
;; 44
(use "RatLeTrans" (pt "(1#2**PosS p)+(1#2**PosS p)"))
(use "RatLeMonPlus")
(use "RatLeTrans" (pt "abs(f approx(x seq n0)n0+ ~(f approx(x seq m)n0))"))
(use "Truth")
;; ?^52:abs(f approx(x seq n0)n0+ ~(f approx(x seq m)n0))<=(1#2**PosS p)
(use "ContElim2")
(use "Cf")
(use "LBd")
(use "UBd")
(use "LBd")
(use "UBd")
(use "NatLeTrans" (pt "n"))
(simp "nDef")
(use "NatMaxUB2")
(use "n<=n0")
;; ?^59:abs(x seq n0-x seq m)<=(1#2**PosPred(f uModCont(PosS p)))
(use "CauchyElim" (pt "x mod"))
(use "RealToCauchy")
(use "Rx")
(simp "<-" "mDef")
(use "NatLeTrans" (pt "n"))
(simp "nDef")
(use "NatLeTrans" (pt "n1 max m"))
(use "NatMaxUB2")
(use "NatMaxUB1")
(use "n<=n0")
(simp "<-" "mDef")
(use "Truth")
;; ?^50:f approx(x seq m)n0<=(1#2**PosS p)
(ng "n1Prop")
(assert "n1<=n0")
 (use "NatLeTrans" (pt "n"))
 (simp "nDef")
 (use "NatLeTrans" (pt "n1 max m"))
 (use "NatMaxUB1")
 (use "NatMaxUB1")
 (use "n<=n0")
;; Assertion proved.
(assume "n1<=n0")
(assert "f approx(x seq m max f doml min f domr)n0<=(1#2**PosS p)")
(use "n1Prop")
(use "n1<=n0")
(simp "RatMaxMinEq")
(assume "Hyp")
(use "Hyp")
(use "UBd")
(use "LBd")
;; ?^48:(1#2**PosS p)+(1#2**PosS p)<=(1#2**p)
(simprat "RatPlusHalfExpPosS")
(use "Truth")
(use "UBd")
(use "LBd")
;; Proof finished.
;; (cdp)
(save "LeContAppZero")

;; We will also need

;; LeZeroContApp
(set-goal "all f,x(Cont f -> Real x -> all m 0<<=f(x seq m) ->
 all n f doml<=x seq n ->
 all n x seq n<=f domr ->
 0<<=f x)")
(assume "f" "x" "Cf" "Rx" "ZeroLeHyp" "LBd" "UBd")
(use "RealLeChar2RealConstrFree")
(use "RealRat")
(use "ContReal")
(use "Cf")
(use "RatLeTrans" (pt "x seq Zero"))
(use "LBd")
(use "UBd")
(use "Rx")
;; ?^5:all p exnc n all n0(n<=n0 -> 0 seq n0<=(f x)seq n0+(1#2**p))
(assume "p")
(assert "exi m m=x mod(PosPred(f uModCont(PosS p)))")
 (intro 0 (pt "x mod(PosPred(f uModCont(PosS p)))"))
 (use "Truth")
(assume "mEx")
(by-assume "mEx" "m" "mDef")
(inst-with-to "ZeroLeHyp" (pt "m") "ZeroLeHypInst")
(inst-with-to "RealLeChar1RealConstrFree"
	      (pt "RealConstr([n](0#1))([p]Zero)")
	      (pt "f(x seq m)")
	      "Inst")
(inst-with-to "Inst" "ZeroLeHypInst" "AllExProp")
(inst-with-to "AllExProp" (pt "PosS p") "ExHyp")
(drop "ZeroLeHyp" "Inst" "ZeroLeHypInst" "AllExProp")
(by-assume "ExHyp" "n1" "n1Prop")
(assert "exi n n=n1 max m max f uMod(PosS p)")
 (intro 0 (pt "n1 max m max f uMod(PosS p)"))
 (use "Truth")
(assume "nEx")
(by-assume "nEx" "n" "nDef")
(intro 0 (pt "n"))
(assume "n0" "n<=n0")
;; ?^39:0 seq n0<=(f x)seq n0+(1#2**p)
(ng #t)
;; ?^40:0<=f approx(x seq n0 max f doml min f domr)n0+(1#2**p)
(simp "RatMaxMinEq")
;; ?^41:0<=f approx(x seq n0)n0+(1#2**p)
(simprat (pf "f approx(x seq n0)n0==
 f approx(x seq n0)n0+ ~(f approx(x seq m)n0)+(f approx(x seq m)n0)"))
(get 45)
(simprat "RatEqvPlusMinus")
(use "Truth")
;; ?^44:0<=f approx(x seq n0)n0+ ~(f approx(x seq m)n0)+f approx(x seq m)n0+
;;         (1#2**p)
(simprat (pf "0== ~((1#2**PosS p)+(1#2**PosS p))+(1#2**p)"))
(simp "RatLe3RewRule")
(simp "RatUMinus2RewRule")
(use "RatLeMonPlus")
;; 51,52
;; ?^51:~(1#2**PosS p)<=f approx(x seq n0)n0+ ~(f approx(x seq m)n0)
(assert "all a,b(abs a<=b -> ~b<=a)")
 (assume "a" "b" "abs a<=b")
 (simp (pf "a= ~ ~ a"))
 (simp "RatLe7RewRule")
 (use "RatLeTrans" (pt "abs ~a"))
 (simp "RatLe8RewRule")
 (use "Truth")
 (use "abs a<=b")
 (use "Truth")
;; Assertion proved.
(assume "Assertion")
(use "Assertion")
;; ?^63:abs(f approx(x seq n0)n0+ ~(f approx(x seq m)n0))<=(1#2**PosS p)
;; this was goal 52 above
(use "ContElim2")
(use "Cf")
(use "LBd")
(use "UBd")
(use "LBd")
(use "UBd")
(use "NatLeTrans" (pt "n"))
(simp "nDef")
(use "NatMaxUB2")
(use "n<=n0")
;; ?^70:abs(x seq n0-x seq m)<=(1#2**PosPred(f uModCont(PosS p)))
;; This was goal 59 above
(use "CauchyElim" (pt "x mod"))
(use "RealToCauchy")
(use "Rx")
(simp "<-" "mDef")
(use "NatLeTrans" (pt "n"))
(simp "nDef")
(use "NatLeTrans" (pt "n1 max m"))
(use "NatMaxUB2")
(use "NatMaxUB1")
(use "n<=n0")
(simp "<-" "mDef")
(use "Truth")
;; ?^52:~(1#2**PosS p)<=f approx(x seq m)n0
;; this si similar to goal 50 above
(ng "n1Prop")
(assert "n1<=n0")
 (use "NatLeTrans" (pt "n"))
 (simp "nDef")
 (use "NatLeTrans" (pt "n1 max m"))
 (use "NatMaxUB1")
 (use "NatMaxUB1")
 (use "n<=n0")
;; Assertion proved.
(assume "n1<=n0")
(assert "0<=f approx(x seq m max f doml min f domr)n0+(1#2**PosS p)")
(use "n1Prop")
(use "n1<=n0")
(simp "RatMaxMinEq")
(assume "Hyp")
(assert "all a,b(0<=a+b -> ~b<=a)")
 (assume "a" "b" "0<=a+b")
 (use "RatLeTrans" (pt "0+ ~b"))
 (use "Truth")
 (use "RatLeTrans" (pt "a+b+ ~b"))
 (use "RatLeMonPlus")
 (use "0<=a+b")
 (use "Truth")
 (simprat "RatEqvPlusMinusRev")
 (use "Truth")
;; Assertion proved.
(assume "Assertion")
(use "Assertion")
(use "Hyp")
(use "UBd")
(use "LBd")
;; ?^48:0== ~((1#2**PosS p)+(1#2**PosS p))+(1#2**p)
(simprat "RatPlusHalfExpPosS")
(use "Truth")
(use "UBd")
(use "LBd")
;; Proof finished.
;; (cdp)
(save "LeZeroContApp")

;; Similary for rht:

;; IVTRealRight
(set-goal 
 "all a,b,p1(0<=b+ ~a ->
 b+ ~a<=2**p1 -> 
 all cds(
  all n,m(n<=m -> lft(cds n)<=lft(cds m)) -> 
  all n,m(n<=m -> rht(cds m)<=rht(cds n)) -> 
  all n lft(cds n)<=rht(cds n) -> 
  all n rht(cds n)-lft(cds n)==(1#2**n)*(b+ ~a) -> 
  Real(RealConstr([n]rht(cds n))([p]PosToNat(p+p1)))))")
(assume
 "a" "b" "p1" "0<=b-a" "b-a<=2**p1" "cds" "cIncr" "dDecr" "cs<=ds" "cdDiff")
(use "RealIntro")
;; 3,4
;; Cauchyness
(use "CauchyCrit")
(ng #t)
;; ?^6:all p,n,m(
;;      TwoThirdExpBd(p+p1)<=n -> 
;;      n<=m -> abs(rht(cds n)+ ~rht(cds m))<=(1#2**p))
(assume "p" "n" "m" "MBd" "n<=m")

;; ?^7:abs(rht(cds n)+ ~rht(cds m))<=(1#2**p)
(simprat (pf "abs(rht(cds n)+ ~rht(cds m))==rht(cds n)+ ~rht(cds m)"))

;; ?^8:rht(cds n)+ ~rht(cds m)<=(1#2**p)
(use "RatLeTrans" (pt "rht(cds n)+ ~lft(cds n)"))
(ng #t)
(use "RatLeTrans" (pt "lft(cds m)"))
(use "cIncr")
(use "n<=m")
(use "cs<=ds")
(simprat "cdDiff")
(simprat (pf "(1#2**p)==(1#2**(p+p1))*2**p1"))
(use "RatLeMonTimesTwo")
(use "Truth")
(use "0<=b-a")
;; ?^21:(1#2)**n<=(1#2**(p+p1))
(ng  #t)
(use "NatLeMonTwoExp")
(use "MBd")
(use "b-a<=2**p1")
;; ?^18:(1#2**p)==(1#2**(p+p1))*2**p1
(simp "PosPlusComm")
(ng #t)
(simp "PosExpTwoPosPlus")
(use "Truth")
;; ?^9:abs(rht(cds n)-rht(cds m))==rht(cds n)-rht(cds m)
(ng #t)
(simp "RatAbsId")
(use "Truth")
(simprat (pf "0==rht(cds m)+ ~rht(cds m)"))
(ng #t)
(use "dDecr")
(use "n<=m")
(use "RatEqvSym")
(use "Truth")
;; ?^4:Mon((RealConstr([n]rht(cds n))([p]TwoThirdExpBd(p+p1)))mod)
(use "MonIntro")
(ng #t)
;; ?^37:allnc p,q(p<=q -> NatLe(PosToNat(p+p1))(PosToNat(q+p1)))
(assume "p" "q" "p<=q")
(assert "p+p1<=q+p1")
(use "PosLeMonPlus")
(use "p<=q")
(use "Truth")
(assume "LeHyp")
(simp "PosToNatLe")
(use "LeHyp")
;; Proof finished.
;; (cdp)
(save "IVTRealRight")

;; IVTFinalRealRight
(set-goal "all f,q,p(
     Cont f -> 
     f f doml<<=0 -> 
     0<<=f f domr -> 
     f doml+(1#2**p)<=f domr -> 
     f domr+ ~f doml<=2**p ->
     all c,d,p(
      f doml<=c -> d<=f domr -> c+(1#2**p)<=d -> RealLt(f c)(f d)(p+q)) -> 
     all cds(
      cds Zero eqd(f doml pair f domr) ->
      all n Corr f(lft(cds n))(rht(cds n))(cNatPos(p+n)) ->
      all n(lft(cds n)<=lft(cds(Succ n))) ->
      all n(rht(cds(Succ n))<=rht(cds n)) ->
      all n(
       rht(cds(Succ n))+ ~lft(cds(Succ n))==(1#2)*(rht(cds n)+ ~lft(cds n))) ->
      Real(RealConstr([n]rht(cds n))([p0]PosToNat(p0+p)))))")
(assume "f" "q" "p" "Cont f" "f a<<=0" "0<<=f b" "a <_p b" "b-a<=2**p" 
	"HypSlope" "cds"
	"cdsProp1" "cdsProp2" "cdsProp3" "cdsProp4" "cdsProp5")
(use "IVTRealRight" (pt "f doml") (pt "f domr"))

;; ?^3:0<=f domr-f doml
(use "RatLeTrans" (pt "f doml+(1#2**p)+ ~f doml"))
(simp "<-" "RatPlusAssoc")
(simp "RatPlusComm")
(simprat "RatEqvPlusMinus")
(use "Truth")
(ng #t)
(use "a <_p b")

;; ?^4:f domr-f doml<=2**p
(use "b-a<=2**p")
;; ?^5:all n,m(n<=m -> lft(cds n)<=lft(cds m))
(assume "n" "m" "n<=m")
(simp (pf "m=n+(m--n)"))
(use "IVTLeftIncr" (pt "f") (pt "q") (pt "p"))
(auto)
(split)
(auto)
(split)
(auto)
(assume "n1")
(split)
(auto)
(split)
(auto)
(simp "NatPlusMinus")
(simp "<-" "NatMinusPlus")
(use "Truth")
(use "Truth")
(use "n<=m")
;; ?^6:all n,m(n<=m -> rht(cds m)<=rht(cds n))
(assume "n" "m" "n<=m")
(simp (pf "m=n+(m--n)"))
(use "IVTRightDecr")
(use "cdsProp4")
(simp "NatPlusMinus")
(simp "<-" "NatMinusPlus")
(use "Truth")
(use "Truth")
(use "n<=m")
;; ?^7:all n lft(cds n)<=rht(cds n)
(assume "n")
(use "CorrElim3Cor" (pt "f") (pt "(cNatPos(p+n))"))
(use "cdsProp2")
;; ?^8:all n rht(cds n)-lft(cds n)==(1#2**n)*(f domr+ ~f doml)
(use "IVTDiff")
(use "cdsProp1")
(use "cdsProp5")
;; Proof finished.
;; (cdp)
(save "IVTFinalRealRight")

;; IVTRealAppRight
(set-goal 
 "all f,q,p(
 Cont f -> 
 f f doml<<=0 -> 
 0<<=f f domr -> 
 f doml+(1#2**p)<=f domr -> 
 f domr+ ~f doml<=2**p -> 
 all c,d,p(f doml<=c -> d<=f domr -> c+(1#2**p)<=d -> RealLt(f c)(f d)(p+q)) -> 
 all cds(
  cds Zero eqd(f doml pair f domr) -> 
  all n Corr f(lft(cds n))(rht(cds n))(cNatPos(p+n)) -> 
  all n lft(cds n)<=lft(cds(Succ n)) -> 
  all n rht(cds(Succ n))<=rht(cds n) -> 
  all n rht(cds(Succ n))+ ~lft(cds(Succ n))==(1#2)*(rht(cds n)+ ~lft(cds n)) -> 
  Real(f(RealConstr([n]rht(cds n))([p0]PosToNat(p0+p))))))")
(assume "f" "q" "p" "Cont f" "f a<<=0" "0<<=f b"
	"a <_p b" "b-a<=2**p" "HypSlope" 
        "cds" "cdsProp1" "cdsProp2" "cdsProp3" "cdsProp4" "cdsProp5")
(use "ContReal")
(use "Cont f")
;; ?^4:f doml<=f domr
(use "RatLeTrans" (pt "f doml+(1#2**p)"))
(use "RatLeTrans" (pt "f doml+0"))
(use "Truth")
(use "RatLeMonPlus")
(use "Truth")
(use "Truth")
(use "a <_p b")
;; ?^5:Real(RealConstr([n]rht(cds n))([p0]PosToNat(p0+p)))
(use "IVTFinalRealRight" (pt "f") (pt "q"))
(use "Cont f")
(use "f a<<=0")
(use "0<<=f b")
(use "a <_p b")
(use "b-a<=2**p")
(use "HypSlope")
(use "cdsProp1")
(use "cdsProp2")
(use "cdsProp3")
(use "cdsProp4")
(use "cdsProp5")
;; Proof finished.
;; (cdp)
(save "IVTRealAppRight")

;; IVTFinal
(set-goal 
 "all f,q,p(
 Cont f -> 
 f f doml<<=0 -> 
 0<<=f f domr -> 
 f doml+(1#2**p)<=f domr -> 
 f domr-f doml<=2**p -> 
 all c,d,p(f doml<=c -> d<=f domr -> c+(1#2**p)<=d -> RealLt(f c)(f d)(p+q)) -> 
 exl x(Real x andi f x===0))")
(assume "f" "q" "p" "Cont f" "f a<<=0" "0<<=f b"
	"a <_p b" "b-a<=2**p" "HypSlope")
(cut "exl cds(
 cds Zero eqd(f doml pair f domr) andi 
 all n Corr f(lft(cds n))(rht(cds n))(cNatPos(p+n)) andi 
 all n(
  lft(cds n)<=lft(cds(Succ n)) andi rht(cds(Succ n))<=rht(cds n) andi 
  rht(cds(Succ n))+ ~lft(cds(Succ n))==(1#2)*(rht(cds n)+ ~lft(cds n))))")
(assume "Excds")
(by-assume "Excds" "cds" "cdsProp")
(intro 0 (pt "RealConstr([n]lft(cds n))([p0]PosToNat(p0+p))"))
(split)
(use "IVTFinalRealLeft" (pt "f") (pt "q") (pt "p"))
(auto)
(use "cdsProp")
(assume "n")
(use "cdsProp")
(assume "n")
(use "cdsProp")
(assume "n")
(use "cdsProp")
(assume "n")
(use "cdsProp")
;; ?^11:f(RealConstr([n]lft(cds n))([p0]PosToNat(p0+p)))===0
(use "RealLeAntiSym")
(use "LeContAppZero")
(auto)
(use "IVTFinalRealLeft" (pt "f") (pt "q"))
(auto)
(use "cdsProp")
(assume "n")
(use "cdsProp")
(assume "n")
(use "cdsProp")
(assume "n")
(use "cdsProp")
(assume "n")
(use "cdsProp")
;; ?^31:all m f((RealConstr([n]lft(cds n))([p0]PosToNat(p0+p)))seq m)<<=0
(assume "n")
(use "CorrElim4" (pt "rht(cds n)") (pt "cNatPos(p+n)"))
(use "cdsProp")
;; ?^32:all n f doml<=(RealConstr([n0]lft(cds n0))([p0]PosToNat(p0+p)))seq n
(ng #t)
;; ?^51:all n f doml<=lft(cds n)
(assume "n")
(use "CorrElim1" (pt "rht(cds n)") (pt "(cNatPos(p+n))"))
(use "cdsProp")
(assume "n")
(ng #t)
(use "RatLeTrans" (pt "rht(cds n)"))
(use "CorrElim3Cor" (pt "f") (pt "(cNatPos(p+n))"))
(use "cdsProp")
(use "CorrElim2" (pt "lft(cds n)") (pt "(cNatPos(p+n))"))
(use "cdsProp")
;; ?^28:0<<=f(RealConstr([n]lft(cds n))([p0]PosToNat(p0+p)))
(use "RealLeCompat"
     (pt "RealConstr([n](0#1))([p]Zero)")
     (pt "f(RealConstr([n]rht(cds n))([p0]PosToNat(p0+p)))"))
(use "RealEqRefl")
(use "RealRat")
;; ?^61:f(RealConstr([n]rht(cds n))([p0]PosToNat(p0+p)))===
;;      f(RealConstr([n]lft(cds n))([p0]PosToNat(p0+p)))
(use "ContAppCompat")
(use "Cont f")
(use "RatLeTrans" (pt "f doml+(1#2**p)"))
(use "RatLeTrans" (pt "f doml+(0#1)"))
(use "Truth")
(use "RatLeMonPlus")
(use "Truth")
(use "Truth")
(use "a <_p b")
;; ?^66:RealConstr([n]rht(cds n))([p0]PosToNat(p0+p))===
;;      RealConstr([n]lft(cds n))([p0]PosToNat(p0+p))
(use "RealEqChar2")
(use "IVTRealRight" (pt "f doml") (pt "f domr"))
;; ?^76:0<=f domr-f doml
(use "RatLeTrans" (pt "f doml+(1#2**p)+ ~f doml"))
(simp "<-" "RatPlusAssoc")
(simp "RatPlusComm")
(simprat "RatEqvPlusMinus")
(use "Truth")
(ng #t)
(use "a <_p b")
;; ?^77:f domr-f doml<=2**p
(use "b-a<=2**p")
;; ?^78:all n,m(n<=m -> lft(cds n)<=lft(cds m))
(assume "n" "m" "n<=m")
(simp (pf "m=n+(m--n)"))
(use "IVTLeftIncr" (pt "f") (pt "q") (pt "p"))
(auto)
(simp "NatPlusMinus")
(simp "<-" "NatMinusPlus")
(use "Truth")
(use "Truth")
(use "n<=m")
;; ?^79:all n,m(n<=m -> rht(cds m)<=rht(cds n))
(assume "n" "m" "n<=m")
(simp (pf "m=n+(m--n)"))
(use "IVTRightDecr")
(assume "n1")
(use "cdsProp")
(simp "NatPlusMinus")
(simp "<-" "NatMinusPlus")
(use "Truth")
(use "Truth")
(use "n<=m")
;; ?^80:all n lft(cds n)<=rht(cds n)
(assume "n1")
(use "CorrElim3Cor" (pt "f") (pt "(cNatPos(p+n1))"))
(use "cdsProp")
;; ?^81:all n rht(cds n)-lft(cds n)==(1#2**n)*(f domr+ ~f doml)
(use "IVTDiff")
(use "cdsProp")
(assume "n")
(use "cdsProp")
;; ?^74:Real(RealConstr([n]lft(cds n))([p0]PosToNat(p0+p)))
(use "IVTFinalRealLeft" (pt "f") (pt "q"))
(auto)
(use "cdsProp")
(assume "n")
(use "cdsProp")
(assume "n")
(use "cdsProp")
(assume "n")
(use "cdsProp")
(assume "n")
(use "cdsProp")
;; ?^75:all p0 
;;       exnc n 
;;        all n0(
;;         n<=n0 -> 
;;         abs((RealConstr([n1]rht(cds n1))([p1]PosToNat(p1+p)))seq n0+ 
;;             ~((RealConstr([n1]lft(cds n1))([p1]PosToNat(p1+p)))seq n0))<=
;;         (1#2**p0))
(ng #t)
;; ?^130:all p exnc n all n0(n<=n0 -> abs(rht(cds n0)+ ~lft(cds n0))<=(1#2**p))
(assume "p1")
(intro 0 (pt "PosToNat(p+p1)"))
(assume "n1" "p+p1<=n1")
(simprat "IVTDiff" (pt "f"))
(simp "RatAbsId")
(use "RatLeTrans" (pt "(1#2**n1)*2**p"))
(use "RatLeMonTimesTwo")
(use "Truth")
;; ?^142:0<=f domr+ ~f doml
(use "RatLeTrans" (pt "f doml+(1#2**p)+ ~f doml"))
(simp "<-" "RatPlusAssoc")
(simp "RatPlusComm")
(simprat "RatEqvPlusMinus")
(use "Truth")
(ng #t)
(use "a <_p b")
(use "Truth")
(use "b-a<=2**p")
;; ?^140:(1#2**n1)*2**p<=(1#2**p1)
(use "RatLeTrans" (pt "(1#2**(p+p1))*2**p"))
(use "RatLeMonTimesTwo")
(use "Truth")
(use "Truth")
(ng #t)
(use "NatLeMonTwoExp")
(use "p+p1<=n1")
(use "Truth")
(simp "<-" "PosExpTwoPosPlus")
(use "Truth")
;; ?^138:0<=(1#2**n1)*(f domr+ ~f doml)
(use "RatLeTrans" (pt "(0#1)*0"))
(use "Truth")
(use "RatLeMonTimesTwo")
(use "Truth")
(use "Truth")
(use "Truth")
;; ?^170:0<=f domr+ ~f doml ;see above
(use "RatLeTrans" (pt "f doml+(1#2**p)+ ~f doml"))
(simp "<-" "RatPlusAssoc")
(simp "RatPlusComm")
(simprat "RatEqvPlusMinus")
(use "Truth")
(ng #t)
(use "a <_p b")
;; ?^136:all n rht(cds(Succ n))+ ~lft(cds(Succ n))==
;; (1#2)*(rht(cds n)+ ~lft(cds n))
(assume "n2")
(use "cdsProp")
(use "cdsProp")
;; ?^62:0<<=f(RealConstr([n]rht(cds n))([p0]PosToNat(p0+p)))
(use "LeZeroContApp")
(use "Cont f")
(use "IVTFinalRealRight" (pt "f") (pt "q"))
(auto)
(use "cdsProp")
(assume "n")
(use "cdsProp")
(assume "n")
(use "cdsProp")
(assume "n")
(use "cdsProp")
(assume "n")
(use "cdsProp")
;; ?^176:all m 0<<=f((RealConstr([n]rht(cds n))([p0]PosToNat(p0+p)))seq m)
(assume "n")
(use "CorrElim5" (pt "lft(cds n)") (pt "cNatPos(p+n)"))
(use "cdsProp")
;; ?^177:all n f doml<=(RealConstr([n0]rht(cds n0))([p0]PosToNat(p0+p)))seq n
(ng #t)
;; ?^195:all n f doml<=rht(cds n)
(assume "n")
(use "RatLeTrans" (pt "lft(cds n)"))
(use "CorrElim1" (pt "rht(cds n)") (pt "(cNatPos(p+n))"))
(use "cdsProp")
(use "CorrElim3Cor" (pt "f") (pt "(cNatPos(p+n))"))
(use "cdsProp")
(assume "n")
(ng #t)
(use "CorrElim2" (pt "lft(cds n)") (pt "(cNatPos(p+n))"))
(use "cdsProp")

;; ?^4:exl cds(
;;      cds Zero eqd(f doml pair f domr) andnc 
;;      all n Corr f(lft(cds n))(rht(cds n))(cNatPos(p+n)) andnc 
;;      all n(
;;       lft(cds n)<=lft(cds(Succ n)) andnc 
;;       rht(cds(Succ n))<=rht(cds n) andnc 
;;       rht(cds(Succ n))-lft(cds(Succ n))==(2#3)*(rht(cds n)-lft(cds n))))

(use "IVTcds" (pt "q"))
(use "Cont f")
(use "f a<<=0")
(use "0<<=f b")
(use "a <_p b")
(use "HypSlope")
;; Proof finished.
;; (cp)
(save "IVTFinal")

(define IVTFinal-eterm (proof-to-extracted-term))
(define IVTFinal-neterm (rename-variables (nt IVTFinal-eterm)))
;; (pp IVTFinal-neterm)

;; [f,p,p0]RealConstr([n]lft(cIVTcds f p p0 n))([p1]PosToNat(p1+p0))

(add-sound "IVTFinal")

;; ok, IVTFinalSound has been added as a new theorem:

;; allnc f,q,p(
;;  Cont f -> 
;;  f f doml<<=0 -> 
;;  0<<=f f domr -> 
;;  f doml+(1#2**p)<=f domr -> 
;;  f domr-f doml<=2**p -> 
;;  all c,d,p0(
;;   f doml<=c -> d<=f domr -> c+(1#2**p0)<=d -> RealLt(f c)(f d)(p0+q)) -> 
;;  (ExLTMR (cterm (x) Real x andnc f x===0))(cIVTFinal f q p))

;; with computation rule

;; cIVTFinal eqd
;; ([f,p,p0]RealConstr([n]lft(cIVTcds f p p0 n))([p1]PosToNat(p1+p0)))

(deanimate "IVTFinal")

;; (display-animation)

;; IVTApprox
(set-goal
 "all f,q,p(
 Cont f -> 
 f f doml<<=0 -> 
 0<<=f f domr -> 
 f doml+(1#2**p)<=f domr -> 
 f domr+ ~f doml<=2**p -> 
 all c,d,p(f doml<=c -> d<=f domr -> c+(1#2**p)<=d -> RealLt(f c)(f d)(p+q)) -> 
 exr x(Real x andr f x===0 andr all r exl c abs(c+ ~x)<<=(1#2**r)))")
(assume "f" "q" "p" "Cont f" "f a<<=0" "0<<=f b"
	"a <_p b" "b-a<=2**p" "HypSlope")
(cut "exl x(Real x andnc f x===0)")
(assume "ExHyp")
(by-assume "ExHyp" "x" "xProp")

;; ?_8:exr x(Real x andr f x===0 andr all r exl c abs(c+ ~x)<<=(1#2**r))
(intro 0 (pt "x"))
(split)
(use "xProp")
(split)
(use "xProp")

;; ?_13:all r exl c abs(c+ ~x)<<=(1#2**r)
(assume "r")
(use "RealApprox")
(use "xProp")

;; ?_4:exl x(Real x andnc f x===0)
(use "IVTFinal" (pt "q") (pt "p"))
(auto)
;; Proof finished.
;; (cdp)
(save "IVTApprox")

(define IVTApprox-eterm (proof-to-extracted-term))
(define IVTApprox-neterm (rename-variables (nt IVTApprox-eterm)))
;; (pp IVTApprox-neterm)
;; [f,p,p0]cRealApprox(cIVTFinal f p p0)

(add-sound "IVTApprox")

;; ok, IVTApproxSound has been added as a new theorem:

;; allnc f,q,p(
;;  Cont f -> 
;;  f f doml<<=0 -> 
;;  0<<=f f domr -> 
;;  f doml+(1#2**p)<=f domr -> 
;;  f domr+ ~f doml<=2**p -> 
;;  all c,d,p0(
;;   f doml<=c -> d<=f domr -> c+(1#2**p0)<=d -> RealLt(f c)(f d)(p0+q)) -> 
;;  (ExRTMR rea
;;    pos=>rat
;;    (cterm (x,(pos=>rat)^) 
;;    (AndRMR (cterm () Real x)
;;      (cterm ((pos=>rat)^0) 
;;      (AndRMR (cterm () f x===0)
;;        (cterm ((pos=>rat)^1) 
;;        allnc r (ExLTMR (cterm (c) abs(c+ ~x)<<=(1#2**r)))((pos=>rat)^1 r)))
;;      (pos=>rat)^0))
;;    (pos=>rat)^))
;;  (cIVTApprox f q p))

;; with computation rule

;; cIVTApprox eqd([f,p,p0]cRealApprox(cIVTFinal f p p0))

;; Example of a continuous function: a^2-2 on [1,2]
;; ================================================

(add-program-constant "SqRtTwo" (py "cont"))
(add-computation-rules
 "SqRtTwo" "ContConstr 1 2([a,n]a*a-2)([p]Zero)([p]p+3)~1 2")

(set-totality-goal "SqRtTwo")
(use "TotalVar")
;; Proof finished.
;; (cp)
(save-totality)

;; ContSqRtTwo
(set-goal "Cont SqRtTwo")
(intro 0)
;; 2-7
(assume "a" "1<=a" "a<=2")
(intro 0)
(ng #t)
(assume "p" "n" "m" "Useless1" "Useless2")
(simp (pf "(IntN 2#1)= ~(IntP 2#1)"))
(simprat "RatEqvPlusMinusPlus")
;; (simprat "RatEqv2RewRule")
(simprat (pf "a*a+ ~(a*a)==0"))
(use "Truth")
(use "Truth")
(use "Truth")
;; 3
(ng #t)
(assume "a" "b" "p" "n" "1<=a" "a<=2"  "1<=b" "b<=2" "Useless" "abDist")
(simp (pf "(IntN 2#1)= ~(IntP 2#1)"))
(simprat "RatEqvPlusMinusPlus")
(simprat "<-" "RatEqvTimesPlusMinus")
(simp "RatAbsTimes")
(use "RatLeTrans" (pt "4*(1#2**PosPred(p+3))"))
(use "RatLeMonTimesTwo")
(use "Truth")
(use "Truth")
(simp "RatAbsId")
(use "RatLeTrans" (pt "(2#1)+2"))
(use "RatLeMonPlus")
(use "a<=2")
(use "b<=2")
(use "Truth")
(use "RatLeTrans" (pt "RatPlus 1 1"))
(use "Truth")
(use "RatLeMonPlus")
(auto)
;; ?^25:4*(1#2**PosPred(p+3))<=(1#2**p)
(simp (pf "p+3=PosS(p+2)"))
(ng #t)
(simp "PosToNatPlus")
(use "Truth")
;; ?^41:p+3=PosS(p+2)
(cases (pt "p"))
(assume "Useless1")
(use "Truth")
(assume "p0"  "Useless1")
(use "Truth")
(assume "p0"  "Useless1")
(use "Truth")
;; 20
(auto)
;; ?^6:all a,n(1<=a -> a<=2 -> 1<=([a0,n0]a0*a0+IntN 2)a n)
(assume "a" "n" "1<=a" "a<=2")
(ng #t)
(use "RatLePlusCancelR" (pt "(2#1)"))
(simp "<-" "RatPlusAssoc")
(ng #t)
(simp (pf "1=(1#1)*1"))
(use "RatLeMonTimesTwo")
(auto)
;; ?^7:all a,n(1<=a -> a<=2 -> ([a0,n0]a0*a0+IntN 2)a n<=4)
(assume "a" "n" "1<=a" "a<=2")
(ng #t)
(use "RatLePlusCancelR" (pt "(2#1)"))
(simp "<-" "RatPlusAssoc")
(ng #t)
(simp (pf "4=(2#1)*2"))
(use "RatLeMonTimesTwo")
(use "RatLeTrans" (pt "1#1"))
(use "Truth")
(auto)
(use "RatLeTrans" (pt "1#1"))
(use "Truth")
(auto)
;; Proof finished.
;; (cp)
(save "ContSqRtTwo")

;; SqRtTwoApprox
(set-goal
 "exr x(Real x andr SqRtTwo x===0 andr all r exl c abs(c+ ~x)<<=(1#2**r))")
(use "IVTApprox" (pt "1") (pt "1"))
;; 2-7
(use "ContSqRtTwo")
;; 3
(ng #t)
(use "RatLeToRealLe")
(use "Truth")
;; 4
(ng #t)
(use "RatLeToRealLe")
(use "Truth")
;; 5
(use "Truth")
;; 6
(use "Truth")
;; 7
(assume "c" "d" "p")
(ng #t)
(assume "1<=c" "d<=2" "c<_pd")
(simp (pf "(IntN 2#1)= ~(2#1)"))
(simprat "RatEqvPlusMinusPlus")
(simp "RatMaxMinEq")
(simp "RatMaxMinEq")
;; ?^21:(1#2**PosS p)<=d*d+ ~(c*c)
(simprat "<-" "RatEqvTimesPlusMinus")
(use "RatLeTrans" (pt "((1#1)+1)*(1#2**p)"))
(simp "RatOneOverExpTwoPosS")
(use "RatLeMonTimes")
(use "Truth")
(use "Truth")
(use "RatLeMonTimesTwo")
(use "Truth")
(use "Truth")
(use "RatLeMonPlus")
(use "RatLeTrans" (pt "c"))
(use "1<=c")
(use "RatLeTrans" (pt "c+(1#2**p)"))
(use "Truth")
(use "c<_pd")
(use "1<=c")
(simp "RatPlusComm")
(use "RatLePlusLInv")
(use "c<_pd")
;; ?^23:c<=2
(use "RatLeTrans" (pt "c+(1#2**p)"))
(use "Truth")
(use "RatLeTrans" (pt "d"))
(use "c<_pd")
(use "d<=2")
(use "1<=c")
(use "d<=2")
(use "RatLeTrans" (pt "c"))
(use "1<=c")
(use "RatLeTrans" (pt "c+(1#2**p)"))
(use "Truth")
(use "c<_pd")
;; 16
(use "Truth")
;; Proof finished.
;; (cp)
(save "SqRtTwoApprox")

(define eterm (proof-to-extracted-term))
(define neterm (rename-variables (nt eterm)))
;; (pp neterm)

;; cRealApprox
;; (cIVTFinal(ContConstr 1 2([a,n]a*a+IntN 2)([p]Zero)([p]p+3)IntN 1 2)1 1)

(add-sound "SqRtTwoApprox") 

;; ok, SqRtTwoApproxSound has been added as a new theorem:

;; (ExRTMR rea
;;   pos=>rat
;;   (cterm (x,(pos=>rat)^) 
;;   (AndRMR (cterm () Real x)
;;     (cterm ((pos=>rat)^0) 
;;     (AndRMR (cterm () SqRtTwo x===0)
;;       (cterm ((pos=>rat)^1) 
;;       allnc r (ExLTMR (cterm (c) abs(c+ ~x)<<=(1#2**r)))((pos=>rat)^1 r)))
;;     (pos=>rat)^0))
;;   (pos=>rat)^))
;; cSqRtTwoApprox

;; with computation rule

;; cSqRtTwoApprox eqd 
;; cRealApprox
;; (cIVTFinal(ContConstr 1 2([a,n]a*a+IntN 2)([p]Zero)([p]p+3)IntN 1 2)1 1)

(deanimate "SqRtTwoApprox")

(display-animation)

;; Haskell translation
;; ===================

(animate "SqRtTwoApprox")
(animate "RealApprox")
(animate "IVTFinal")
(animate "IVTcds")
(animate "IVTAux")
(animate "NatPos")
(animate "ApproxSplitPos")

(terms-to-haskell-program
 "~/temp/sqrttwo.hs"
 (list (list (pt "cSqRtTwoApprox") "sqrtwo")))

;; To run cauchysds.hs type in terminal

;; $ ghci sqrttwo.hs

;; Then type

;; *Main> cSqRtTwoApprox 10

;; 181 % 128

;; *Main> cSqRtTwoApprox 20
;; 5931641 % 4194304

;; *Main> cSqRtTwoApprox 50
;; 1592262918131443 % 1125899906842624

;; *Main> cSqRtTwoApprox 100
;; 3585457342386312954798844046557 % 2535301200456458802993406410752

;; *Main> cSqRtTwoApprox 200
;; 1136276788042180458070828951474823657989790988021617205464301 % 803469022129495137770981046170581301261101496891396417650688

;; *Main> cSqRtTwoApprox 500
;; 18517093570525735794594778233695623554852620593811191140219615888770805280230743798428624469545743619154166192605819887937633432105940059864134913555731 % 13093562431584567480052758787310396608866568184172259157933165472384535185618698219533080369303616628603546736510240284036869026183541572213314110357504

;; (pp (nt (pt "NatToPos(PosLog 4194304)")))
;; 22

;; (pp (nt (pt "NatToPos(PosLog 1125899906842624)")))
;; 50

;; (pp (nt (pt "NatToPos(PosLog 2535301200456458802993406410752)")))
;; 101

;; (pp (nt (pt "NatToPos(PosLog 803469022129495137770981046170581301261101496891396417650688)")))
;; 199

;; (sqrt 2)
;; 1.4142135623730951

(exact->inexact 181/128)
;; 1.4140625

(exact->inexact 1592262918131443/1125899906842624)
;; 1.414213562373095

;; At 50 we already have 15 corrext decimal digits


;; (pp "cSqRtTwoApprox0CompRule")

;; cSqRtTwoApprox eqd 
;; cRealApprox
;; (cIVTFinal(ContConstr 1 2([a,n]a*a+IntN 2)([p]Zero)([p]p+3)IntN 1 2)1 1)

;; (pp "cRealApprox0CompRule")

;; cRealApprox eqd([x,p]x seq(x mod p))

;; (pp "cIVTFinal0CompRule")

;; cIVTFinal eqd
;; ([f,p,p0]RealConstr([n]lft(cIVTcds f p p0 n))([p1]PosToNat(p1+p0)))

;; (pp "cIVTcds0CompRule")

;; ([f,p,p0,n]
;;   (Rec nat=>rat yprod rat)n(f doml pair f domr)
;;   ([n0,cd]cIVTAux f p(cNatPos(p0+n0))lft cd rht cd))

;; (pp "cIVTAux0CompRule")

;; cIVTAux eqd
;; ([f,p,p0,a,a0]
;;   [let a1
;;     ((1#4)*(3*a+a0))
;;     [let x
;;      (RealConstr(f approx(a1 max f doml min f domr))([p1]f uMod(PosS p1)))
;;      [let a2
;;       ((1#2)*(a+a0))
;;       [let x0
;;        (RealConstr(f approx(a2 max f doml min f domr))([p1]f uMod(PosS p1)))
;;        [if (cApproxSplitPos x x0 0(PosS(PosS(p0+p))))
;;         (a pair a2)
;;         [if (cApproxSplitPos x0
;;              (RealConstr(f approx((1#4)*(a+3*a0)max f doml min f domr))
;;               ([p1]f uMod(PosS p1)))
;;              0
;;              (PosS(PosS(p0+p))))
;;          (a1 pair(1#4)*(a+3*a0))
;;          (a2 pair a0)]]]]]])

;; (pp "cApproxSplitPos0CompRule")

;; cApproxSplitPos eqd
;; ([x,x0,x1,p]
;;   [if x
;;     ([as,M]
;;      [if x0
;;        ([as0,M0]
;;         [if x1
;;           ([as1,M1]
;;            as1(M0(PosS(PosS p))max M(PosS(PosS p))max M1(PosS(PosS p)))<=
;;            (1#2)*
;;            (as(M0(PosS(PosS p))max M(PosS(PosS p)))+
;;             as0(M0(PosS(PosS p))max M(PosS(PosS p)))))])])])


(display-animation)

;; 2022-10-03.  Done up to this point