;;Man wundert sich viellicht über einige Benunngen von Annahmen.
;;Diese Benunngen haben jedoch den Vorteil, dass man sich die Annahmen leichter merken kann, was man selbst auch einmal testen sollte.

(set! COMMENT-FLAG #f)
(libload "nat.scm")
(libload "numbers.scm")
(libload "simpreal.scm")
(libload "real.scm")
(libload "realnneg.scm")
(set! COMMENT-FLAG #t)

(add-global-assumption
 "RatNotLeToLe"
 "all rat1,rat2((rat1<=rat2 -> F) -> rat2<=rat1)") 

;;Lemma1
(set-goal "all k, as, M, n, m (Cauchy as M -> M(k)<=m -> M(k) <= n -> as(m)<=as(n)+1/2**(k))")
(assume "k" "as" "M" "n" "m")
(assume "Ca" "M(k)<=m" "M(k)<=n")
(assert "as m -as n <= 1/2**k")
(use "RatLeTrans" (pt "abs(as m -as n)"))
(use "RatAbsUB1")
(use "CauchyElim" (pt "M"))
(use "Ca")
(use "M(k)<=m")
(use "M(k)<=n")
(assume "Spam")
(ord-field-simp-bwd)
(ord-field-simp-fwd "Spam")
(use 5)
(save "Lemma1")
;;Fertig

;;RealApprox
(set-goal "all as,M,k(Mon M ->  Cauchy as M -> ex a all l (abs(a -as(M l)))<= 1/2**k + 1/2**l)")
(assume "as" "M" "k")
(assume "monM" "Cx")
(ex-intro (pt "as(M (k))"))
(assume "l")
(use "RatLeTrans" (pt "abs(as(M k)-as(M(k max l)))+abs(as(M(k max l))-as(M l))" ))
(use "RatAbsLe2")
(use "RatLeMonPlus")
(use "CauchyElim" (pt "M"))
(use "Cx")
(use "Truth")
(use "MonElim")
(use "monM")
(use "IntMaxUB1")
(use "CauchyElim" (pt "M"))
(use "Cx")
(use "Truth")
(use "MonElim")
(use "monM")
(use "IntMaxUB2")
(use "Truth")

(save "RealApprox2")
(define eterm (proof-to-extracted-term))
(define neterm (rename-variables (nt eterm)))
(pp neterm)
;;FERTIG!

;;PlusPos
(set-goal "allnc as,bs,M,N all k (Cauchy as M -> Cauchy bs N -> (all l ex l0 all n (l0 <= n -> 0 <= as(n)+1/2**l)) -> ex l1 all n(l1 <= n -> 1/2**k <= bs(n)) -> ex l2 all n((l2 <= n) -> 1/2**(k+1) <=bs(n) + as(n))) ")
(assume "as" "bs" "M" "N" "k")
(assume "Cx" "Cy")
(assume "0<=x" "0<y")
(by-assume "0<y" "l0" "0<l0y")
(inst-with-to "0<=x" (pt "k+1") "k+1:0<=x")
(drop "0<=x")
(by-assume "k+1:0<=x" "l1" "Defl1")
(ex-intro (pt "l0 max l1"))
(assume "n")
(assume "Maxi")
(inst-with-to "0<l0y" (pt "n") "Peter")
(inst-with-to "Defl1" (pt "n") "Günter")
(assert "1/2**(k+1)<= bs n - 1/2**(k+1)")
(ord-field-simp-bwd)
(assert "1/2**k<=bs n")
(use "Peter")
(use "IntLeTrans" (pt "l0 max l1"))
(use "IntMaxUB1")
(use "Maxi")
(assume "Langweilig")
(ord-field-simp-fwd "Langweilig")
(use 12)
(assume "Rüdiger")
(use "RatLeTrans" (pt "bs n -1/2**(k+1)"))
(use "Rüdiger")
(ord-field-simp-bwd)
(assert "0<=as n+1/2**(k+1)")
(use "Günter")
(use "IntLeTrans" (pt "l0 max l1"))
(use "IntMaxUB2")
(use "Maxi")
(assume "Franziskus")
(ord-field-simp-fwd "Franziskus")
(use 13)
(save "PlusPos")
(pp "PlusPos")

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

;;LeIsNotGt1
(set-goal "all as, M, k, m (Cauchy as M -> all n(m<= n -> 1/2**k <= as n) -> all l ex m0 all n ( m0<=n -> as n <=1/2**l) -> F)")
(assume "as" "M" "k" "m" )
(assume "Cx")
(assume "0<x")
(assume "x<=0")
(inst-with-to "x<=0" (pt "k+1") "x<=0neu")
(by-assume "x<=0neu" "m0" "x<=0ganzneu")
(inst-with-to "0<x" (pt "m0 max m ") "0<xneu")
(inst-with-to "x<=0ganzneu" (pt "m0 max m") "AAA")
(assert "1/2**k <= as(m0 max m)")
(use "0<xneu")
(use "NatMaxUB2")
(assume "AB")
(assert "as(m0 max m)<= 1/2**(k+1)")
(use "AAA")
(use "NatMaxUB1")
(assume "AC")
(assert "1/2**k<=1/2**(k+1)")
(use "RatLeTrans" (pt "as(m0 max m)"))
(auto)
(assume "Ende")
(ord-field-simp-fwd "Ende")
(auto)

(save "LeIsBotGt1")
;;Fertig

;;LeIsNotGf2
(set-goal "all as, M (Cauchy as M -> all k (as(M(k+1))<=1/2**k) -> all k ex m all n (m<= n -> as(n) <= 1/2**k))")
(assume "as" "M")
(assume "Cx")
(assume "Neg0<x")
(assume "k")
(inst-with-to "Neg0<x" (pt "k+1") "Neu")
(ex-intro (pt "M(k+2)"))
(assume "n")
(assume "M(k+2)<=n")
(use "RatLeTrans" (pt "as(M(k+2))+1/2**(k+2)"))
(use "Lemma1" (pt "M"))
(use "Cx")
(use "M(k+2)<=n")
(use "Truth")
(use "RatLeTrans" (pt "1/2**(k+1) +1/2**(k+2)"))
(use "RatLeMonPlus")
(use "Neu")
(use "Truth")
(ord-field-simp-bwd)

(save "LeIsNotGf2")
;;Fertig


;;ApproxSplit
(set-goal "all as,bs,cs,M,N,L,k (Cauchy as M -> Cauchy bs N -> Cauchy cs L ->  as(M(k+2) max N(k+2))+1/2**k<= bs(M(k+2) max N(k+2)) -> ex m all n (m<= n -> cs(n) <= bs(n)) oru ex m all n (m<= n -> as(n) <= cs(n)))")
(assume "as" "bs" "cs" "M" "N" "L" "k")
(assume "Cx" "Cy" "Cz")
(assume "x<y")
(cases (pt "cs((M(k+2) max N(k+2)) max L(k+2)) <= (as(M(k+2) max N(k+2)) + bs(M(k+2) max N(k+2)))/2") )
(assume "Fall1")
(intro 0)
(ex-intro (pt "(M(k+2) max N(k+2)) max L(k+2)"))
(assume "n")
(assume "q<=n")
(use "RatLeTrans" (pt  " cs((M(k+2) max N(k+2)) max L(k+2)) + 1/2**(k+2)"))
(use "Lemma1" (pt "L" ))
(use "Cz")
(use "NatLeTrans" (pt "M(k+2)max N(k+2)max L(k+2)"))
(use "NatMaxUB2")
(use "q<=n")
(use "NatMaxUB2")
(use "RatLeTrans" (pt "(as(M(k+2) max N(k+2))+ bs(M(k+2) max N(k+2)))/2 + (bs(M(k+2) max N(k+2))-as(M(k+2) max N(k+2)))/4"))
(use "RatLeMonPlus")
(use "Fall1")
(ord-field-simp-bwd)
(ord-field-simp-fwd "x<y")
(search) 
(use "RatLeTrans" (pt "bs(M(k+2) max N(k+2))-(bs(M(k+2) max N(k+2))-as(M(k+2) max N(k+2)))/4"))
(ord-field-simp-bwd)
(use "RatLeTrans" (pt "bs(M(k+2) max N(k+2))-1/2**(k+2)"))
(ord-field-simp-bwd)
(ord-field-simp-fwd "x<y")
(search)
(assert "bs(M(k+2) max N(k+2))<= bs n +1/2**(k+2)")
(use "Lemma1" (pt "N"))
(use "Cy")
(use "NatMaxUB2")
(use "NatLeTrans" (pt "M(k+2) max N(k+2)"))
(use "NatMaxUB2")
(use "NatLeTrans" (pt "M(k+2) max N(k+2) max L(k+2)"))
(use "NatMaxUB1")
(use "q<=n")
(assume "TOR!")
(ord-field-simp-bwd)
(ord-field-simp-fwd "TOR!")
(use 8)
(assume "Fall2")
(intro 1)
(ex-intro "M(k+2) max N(k+2) max L(k+2)")
(assume "n" "q<=n")
(use "RatLeTrans" (pt "as(M(k+2) max N(k+2)) +1/2**(k+2)"))
(use "Lemma1" (pt "M"))
(use "Cx")
(use "NatLeTrans" (pt "M(k+2) max N(k+2)"))
(use "NatMaxUB1")
(use "NatLeTrans" (pt "M(k+2) max N(k+2) max L(k+2)"))
(use "NatMaxUB1")
(use "q<=n")
(use "NatMaxUB1")
(use "RatLeTrans" (pt "as(M(k+2) max N(k+2))+(bs(M(k+2) max N(k+2)) - as(M(k+2) max N(k+2)))/4"))
(ord-field-simp-bwd)
(ord-field-simp-fwd "x<y")
(search)
(use "RatLeTrans" (pt "(as(M(k+2) max N(k+2))+ bs(M(k+2) max N(k+2)))/2 - (bs(M(k+2) max N(k+2))- as(M(k+2) max N(k+2)))/4"))
(ord-field-simp-bwd)
(assert "(as(M(k+2)max N(k+2))+bs(M(k+2)max N(k+2)))/2 <= cs(M(k+2)max N(k+2)max L(k+2))")
(use "RatNotLeToLe")
(use "Fall2")
(assume "Tillman")
(use "RatLeTrans" (pt "cs(M(k+2)max N(k+2)max L(k+2)) -1/2**(k+2)" ))
(assert "(as(M(k+2)max N(k+2))+bs(M(k+2)max N(k+2)))/2 +1/2**(k+2) <= 
      cs(M(k+2)max N(k+2)max L(k+2)) + (bs(M(k+2)max N(k+2))-as(M(k+2)max N(k+2)))/4 ")
(use "RatLeMonPlus")
(use "Tillman")
(assert "1/2**k<=bs(M(k+2)max N(k+2))-as(M(k+2)max N(k+2)) ")
(ord-field-simp-fwd "x<y")
(ord-field-simp-bwd)
(search)
(assume "Schere")
(ord-field-simp-fwd "Schere")
(ord-field-simp-bwd)
(search)
(assume "Papier")
(ord-field-simp-fwd "Papier")
(ord-field-simp-bwd)
(search)
(assert "cs(M(k+2) max N(k+2) max L(k+2)) <= cs(n) +1/2**(k+2)")
(use "Lemma1" (pt "L"))
(use "Cz")
(use "NatMaxUB2")
(use "NatLeTrans" (pt "M(k+2) max N(k+2) max L(k+2) "))
(use "NatMaxUB2")
(use "q<=n")
(assume "TOOOR!")
(ord-field-simp-bwd)
(ord-field-simp-fwd "TOOOR!")
(search)

(save "ApproxSplit1")

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