;; 2023-07-18.  ss23/sdindav.scm.  Based on ss22/sdindav.scm.
;; Adapted to changes in rea.scm:
;; In rea.scm K was used as var-name of type nat=>pos.  Here we need K
;; for JK.scm.  Hence we remove K

;; 2022-07-24.  ss22/sdindav.scm.  Taken from temp/examplesanalyssdindavaux.scm

;; 2022-07-02.  Based on Nils Koepp's sd_lookahead_ind.scm using an
;; inductive predicate L intended to hold for reals x with 0<<=x and
;; x<1 only.  Proof of LMultAux made more structured.  The rest is
;; obsolete.

;; 2022-06-26.  examplesanalysissdindavaux.scm.  Based on Nils Koepp's
;; sd_lookahead_ind.scm using his inductive predicate L (was G).

(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")

(load "~/git/minlog/examples/analysis/digits.scm")
;; (set! COMMENT-FLAG #t)

;; In int.scm

;; IntTimesCompat
(set-goal "all k,j,i,i0(k=j -> i=i0 -> k*i=j*i0)")
(assume "k" "j" "i" "i0" "k=j" "i=i0")
(simp "k=j")
(simp "i=i0")
(use "Truth")
;; Proof finished.
;; (cp)
(save "IntTimesCompat")

;; End of changes in int.scm

;; The inductive predicate L
;; =========================

(add-algs "al"
	  '("U" "al")
	  '("C" "sd=>al=>al"))
(add-var-name "u" "v" "w" (py "al"))

(add-eqpnc "al")
(add-totality "al")
(add-totalnc "al")
(add-mr-ids "TotalAl")

;; (remove-var-name "L")
;; (remove-token "L")

(add-ids
 (list (list "L" (make-arity (py "rea") (py "nat")) "al"))
 '("allnc x (Real x -> abs x<<=1 -> L x Zero)" "InitL")
 '("allnc d,x,x0,n(Sd d -> L x n -> x0===(1#2)*(x+d) -> L x0(Succ n))" "GenL"))

;; If we know the first n digits of a representation of x and
;; x0===(1#2)*(x+d), then we know the first n+1 digits of a
;; representation of x0.

(add-mr-ids "L")

;; LToReal
(set-goal "allnc x,n(L x n -> Real x)")
(assume "x" "n" "Lxn")
(elim "Lxn")
;; 3,4
(assume "y" "Ry" "yBd")
(use "Ry")
;; 4
(assume "d" "y" "y0" "n0" "Sdd" "Iy" "Ry" "y0Def")
(autoreal)
;; Proof finished.
;; (cp)
(save "LToReal")

;; SdBoundReal
(set-goal "allnc d(Sd d -> RealAbs d<<=1)")
(assume "d" "Sdd")
(use "RatLeToRealLe")
(use "SdBound")
(use "Sdd")
;; Proof finished.
;; (cp)
(save "SdBoundReal")

;; LToBd
(set-goal "allnc x,n(L x n -> abs x<<=1)")
(assume "x" "n" "Lx")
(elim "Lx")
(assume "y" "Ry" "yBd")
(use "yBd")
(assume "d" "x1" "y" "n1" "Sdd" "Lx1n1" "x1Bd" "yDef")
(assert "Real x1")
(use "LToReal" (pt "n1"))
(use "Lx1n1")
(assume "Rx1")
(simpreal "yDef")
(use "RealLeAbs")
;; 12,13
(simpreal (pf "RealConstr([n](1#1))([p]Zero)===RealTimes(1#2)(RealPlus 1 1)"))
(use "RealLeMonTimesR")
(use "RatLeToRealLe")
(use "Truth")
(use "RealLeMonPlusTwo")
(use "RealLeTrans" (pt "abs x1"))
(use "RealLeIdAbs")
(use "Rx1")
(use "x1Bd")
(use "RealLeTrans" (pt "RealAbs d"))
(use "RealLeIdAbs")
(use "RealRat")
(use "SdBoundReal")
(use "Sdd")
;; ?^15:1===(1#2)*RealPlus 1 1
(use "RealEqRefl")
(use "RealRat")
;; ?^13:~((1#2)*(x1+d))<<=1
(simpreal "<-" (pf "~(RealUMinus 1)===1"))
(use "RealLeUMinus")
(simpreal
 (pf "RealUMinus 1===RealTimes(1#2)(RealPlus(RealUMinus 1)(RealUMinus 1))"))
(use "RealLeMonTimesR")
(use "RatLeToRealLe")
(use "Truth")
(use "RealLeMonPlusTwo")
(simpreal "<-" (pf "~ ~x1===x1"))
(use "RealLeUMinus")
(use "RealLeTrans" (pt "abs x1"))
(simpreal "<-" "RealAbsUMinus")
(use "RealLeIdAbs")
(autoreal)
(use "x1Bd")
(use "RealUMinusUMinus")
(use "Rx1")
(simpreal "<-" (pf "~(RealUMinus d)===d"))
(use "RealLeUMinus")
(use "RealLeTrans" (pt "RealAbs d"))
(simpreal "<-" "RealAbsUMinus")
(use "RealLeIdAbs")
(autoreal)
(use "SdBoundReal")
(use "Sdd")
(use "RealUMinusUMinus")
(use "RealRat")
(use "RealEqRefl")
(use "RealRat")
(use "RealUMinusUMinus")
(use "RealRat")
;; Proof finished.
;; (cp)
(save "LToBd")

;; LCompat
(set-goal "allnc x,y,n(x===y -> L x n -> L y n)")
(cut "allnc x,n(L x n -> allnc y(x===y -> L y n))")
(assume "CutHyp" "x0" "x1" "n1" "x0=x1" "Lx0")
(use "CutHyp" (pt "x0"))
(auto)
(assume "x" "n" "Lx")
(elim "Lx")
(assume "z" "Rz" "zBd" "y" "z=y")
(intro 0)
(use "RealEqToReal1" (pt "z"))
(use "z=y")
(simpreal "<-" "z=y")
(use "zBd")
(assume "d0" "y0" "y1" "n2" "Sdd" "Ly0" "IH" "y1Def" "y2" "y1=y")
(intro 1 (pt "d0") (pt "y0"))
(auto)
(simpreal "<-" "y1=y")
(auto)
;; Proof finished.
;; (cp)
(save "LCompat")

(define eterm (proof-to-extracted-term (current-proof)))
(define neterm (rename-variables (nt eterm)))
;; (pp neterm)
;; [u]u

(animate "LCompat")
;; We leave LCompat animated because it is simple.

;; EfL
(set-goal "F -> allnc x,n L x n")
(assume "Absurd" "x" "n")
(simp (pf "n eqd Zero"))
(use "InitL")
(use "EfReal")
(use "Absurd")
(use "EfRealLe")
(use "Absurd")
(use "EfEqD")
(use "Absurd")
;; Proof finished.
;; (cp)
(save "EfL")

;; LClosure
(set-goal
 "allnc x,n(L x(Succ n) -> exr d,x0(Sd d andi x===(1#2)*(x0+d) andi L x0 n))")
(cut "allnc x,n,m(
 L x m -> m=n+1 -> exr d,x0(Sd d andi x===(1#2)*(x0+d) andi L x0 n))")
;; 2,3
(assume "CutHyp" "x" "n" "LxSn")
(use "CutHyp" (pt "Succ n"))
(use "LxSn")
(use "Truth")
;; 3
(assume "x" "n" "m" "Lxm")
(elim "Lxm")
(assume "x0" "Rx0" "x0Bd" "0=Sn")
(intro 0 (pt "0"))
(intro 0 (pt "x0"))
(split)
(use "EfSd")
(use "0=Sn")
(split)
(use "EfRealEq")
(use "0=Sn")
(use "EfL")
(use "0=Sn")
(assume "d0" "x1" "y1" "n1" "Sdd0" "Lxn1" "IH" "y1Def" "n1=n")
(intro 0 (pt "d0"))
(intro 0 (pt "x1"))
(split)
(use "Sdd0")
(split)
(use "y1Def")
(simp "<-" "n1=n")
(use "Lxn1")
;; Proof finished.
;; (cp)
(save "LClosure")

(define eterm (proof-to-extracted-term))
(define neterm (rename-variables (nt eterm)))
;; (ppc neterm)
;; [u][case u (U -> cEfSd pair cEfL) (C s u -> s pair u)]

;; End of material parallel to sdcode.scm

;; Here begins material parallel to sdavaux.scm

;; Average
;; =======

(remove-var-name "K")
(remove-token "K")

(set! COMMENT-FLAG #f)
(load "~/git/minlog/examples/analysis/JK.scm")
(set! COMMENT-FLAG #t)

;; 2022-05-28
;; LAvToAvc
(set-goal "allnc x,y,n(L x(Succ n) -> L y(Succ n) -> 
 exr i,x1,y1((1#2)*(x+y)===(1#4)*(x1+y1+i) andi
 Sdtwo i andi L x1 n andi L y1 n))")
(cut "allnc x,y,n,m(L x m -> L y m -> m=Succ n ->
 exr i,x1,y1((1#2)*(x+y)===(1#4)*(x1+y1+i) andi
 Sdtwo i andi L x1 n andi L y1 n))")
;; 2,3
(assume "CutHyp" "x" "y" "n" "Lx" "Ly")
(use "CutHyp" (pt "Succ n"))
(auto)
;; 3
(assume "x" "y" "n" "m" "Lxm" "Lym" "m=Sn")
(assert "Real x")
(use "LToReal" (pt "m"))
(use "Lxm")
(assume "Rx")
(assert "Real y")
(use "LToReal" (pt "m"))
(use "Lym")
(assume "Ry")
(simphyp-to "Lxm" "m=Sn" "LxSn")
(simphyp-to "Lym" "m=Sn" "LySn")
(inst-with-to "LClosure" (pt "x") (pt "n") "LxSn" "Instx")
(inst-with-to "LClosure" (pt "y") (pt "n") "LySn" "Insty")
(by-assume "Instx" "d" "dProp")
(by-assume "dProp" "x1" "dx1Prop")
(by-assume "Insty" "e" "eProp")
(by-assume "eProp" "y1" "ey1Prop")
(assert "Real x1")
(use "LToReal" (pt "n"))
(use "dx1Prop")
(assume "Rx1")
(assert "Real y1")
(use "LToReal" (pt "n"))
(use "ey1Prop")
(assume "Ry1")
(intro 0 (pt "d+e"))
(intro 0 (pt "x1"))
(intro 0 (pt "y1"))
(split)
(assert "Real((1#4)*(x1+y1+(d+e)))")
(autoreal)
(assume "R")
(simpreal "dx1Prop")
(simpreal "ey1Prop")
(use "RealEqSToEq")
(autoreal)
(cases (pt "x1"))
(assume "as" "M" "x1Def")
(cases (pt "y1"))
(assume "bs" "N" "y1Def")
(use "RealEqSIntro")
(assume "n2")
(ng #t)
(simprat "<-" "RatTimesPlusDistr")
(ng #t)
(simp "<-" "RatPlusAssoc")
(simp "<-" "RatPlusAssoc")
(simp "<-" "RatPlusAssoc")
(use "RatPlusCompat")
(use "Truth")
(ng #t)
(simp (pf "d+bs n2=bs n2+d"))
(simp "<-" "RatPlusAssoc")
(use "RatPlusCompat")
(use "Truth")
(use "Truth")
(use "RatPlusComm")
;; ?_49:Sdtwo(d+e) andd L x1 n andd L y1 n
(split)
(use "IntPlusSdToSdtwo")
(use "dx1Prop")
(use "ey1Prop")
(split)
(use "dx1Prop")
(use "ey1Prop")
;; Proof finished.
;; (cp)
(save "LAvToAvc")

(define LAvToAvc-eterm (proof-to-extracted-term))
(pp (term-to-type LAvToAvc-eterm))
;; al=>al=>sdtwo yprod al yprod al

(define LAvToAvc-neterm (rename-variables (nt LAvToAvc-eterm)))
;; (ppc LAvToAvc-neterm)

;; [u,u0]
;;  cIntPlusSdToSdtwo clft(cLClosure u)clft(cLClosure u0)pair 
;;  crht(cLClosure u)pair crht(cLClosure u0)

;; LAvcSatLClAuxJ
(set-goal "allnc d,e,i(Sd d -> Sd e -> Sdtwo i -> Sdtwo(J(d+e+i*2)))")
(assume "d" "e" "i" "Sdd" "Sde" "Sdtwoi")
(assert "exl s1 SdInj d s1")
(use "SdInjIntro")
(use "Sdd")
(assume "ExHyp1")
(by-assume "ExHyp1" "s1" "s1Prop")
(assert "exl s2 SdInj e s2")
(use "SdInjIntro")
(use "Sde")
(assume "ExHyp2")
(by-assume "ExHyp2" "s2" "s2Prop")
(assert "exl t SdtwoInj i t")
(use "SdtwoInjIntro")
(use "Sdtwoi")
(assume "ExHyp3")
(by-assume "ExHyp3" "t" "tProp")
(use "SdtwoInjElim"
     (pt "IntToSdtwo(J(SdToInt s1+SdToInt s2+SdtwoToInt t*2))"))
(simp (pf "J(SdToInt s1+SdToInt s2+SdtwoToInt t*2)=J(d+e+i*2)"))
(use "SdtwoInjIntToSdtwo")
;; ?^27:abs(J(d+e+i*2))<=2
(use "JProp")
(simp (pf "SdToInt s1+SdToInt s2+SdtwoToInt t*2=d+e+i*2"))
(use "Truth")
;; ?^29:SdToInt s1+SdToInt s2+SdtwoToInt t*2=d+e+i*2
(inst-with-to "SdInjId" (pt "d") (pt "s1") "s1Prop" "SdInjIdInst1")
(inst-with-to "SdInjId" (pt "e") (pt "s2") "s2Prop" "SdInjIdInst2")
(inst-with-to "SdtwoInjId" (pt "i") (pt "t") "tProp" "SdtwoInjIdInst")
(simp "SdInjIdInst1")
(simp "SdInjIdInst2")
(simp "SdtwoInjIdInst")
(use "Truth")
;; Proof finished.
;; (cp)
(save "LAvcSatLClAuxJ")

(define eterm (proof-to-extracted-term))
(define neterm (rename-variables (nt eterm)))
;; (pp neterm)
;; [s,s0,t]IntToSdtwo(J(SdToInt s+SdToInt s0+SdtwoToInt t*2))

;; LAvcSatLClAuxK
(set-goal "allnc d,e,i(Sd d -> Sd e -> Sdtwo i -> Sd(K(d+e+i*2)))")
(assume "d" "e" "i" "Sdd" "Sde" "Sdtwoi")
(assert "exl s1 SdInj d s1")
(use "SdInjIntro")
(use "Sdd")
(assume "ExHyp1")
(by-assume "ExHyp1" "s1" "s1Prop")
(assert "exl s2 SdInj e s2")
(use "SdInjIntro")
(use "Sde")
(assume "ExHyp2")
(by-assume "ExHyp2" "s2" "s2Prop")
(assert "exl t SdtwoInj i t")
(use "SdtwoInjIntro")
(use "Sdtwoi")
(assume "ExHyp3")
(by-assume "ExHyp3" "t" "tProp")
(use "SdInjElim" (pt "IntToSd(K(SdToInt s1+SdToInt s2+SdtwoToInt t*2))"))
(simp (pf "K(SdToInt s1+SdToInt s2+SdtwoToInt t*2)=K(d+e+i*2)"))
(use "SdInjIntToSd")
;; ?^27:abs(K(d+e+i*2))<=1
(use "KProp")
;; ?^28:abs(d+e+i*2)<=6
(use "IntLeTrans" (pt "IntP 2+IntP 4"))
(use "IntLeTrans" (pt "abs(d+e)+abs(i*2)"))
(use "IntLeAbsPlus")
(use "IntLeMonPlus")
(use "IntLeTrans" (pt "IntP 1+IntP 1"))
(use "IntLeTrans" (pt "abs d+abs e"))
(use "IntLeAbsPlus")
(use "IntLeMonPlus")
(use "SdBound")
(use "Sdd")
(use "SdBound")
(use "Sde")
(use "Truth")
(ng #t)
(use "IntLeTrans" (pt "IntP 2*IntP 2"))
(use "IntLeMonTimes")
(use "Truth")
(use "SdtwoBound")
(use "Sdtwoi")
(use "Truth")
(use "Truth")
(simp (pf "SdToInt s1+SdToInt s2+SdtwoToInt t*2=d+e+i*2"))
(use "Truth")
;; ?^50:SdToInt s1+SdToInt s2+SdtwoToInt t*2=d+e+i*2
(inst-with-to "SdInjId" (pt "d") (pt "s1") "s1Prop" "SdInjIdInst1")
(inst-with-to "SdInjId" (pt "e") (pt "s2") "s2Prop" "SdInjIdInst2")
(inst-with-to "SdtwoInjId" (pt "i") (pt "t") "tProp" "SdtwoInjIdInst")
(simp "SdInjIdInst1")
(simp "SdInjIdInst2")
(simp "SdtwoInjIdInst")
(use "Truth")
;; Proof finished.
;; (cp)
(save "LAvcSatLClAuxK")

(define eterm (proof-to-extracted-term))
(define neterm (rename-variables (nt eterm)))
;; (pp neterm)
;; [s,s0,t]IntToSd(K(SdToInt s+SdToInt s0+SdtwoToInt t*2))

;; LAvcSatLCl
(set-goal "allnc i,x,y,n(Sdtwo i andi L x(Succ n) andi L y(Succ n) ->
 exr d,j,x1,y1((1#4)*(x+y+i)===(1#2)*((1#4)*(x1+y1+j)+d) andi
 Sd d andi Sdtwo j andi L x1 n andi L y1 n))")
(assume "i" "x" "y" "n" "Conj")
(inst-with-to "Conj" 'left "Sdtwoi")
(inst-with-to "Conj" 'right 'left "Lx")
(inst-with-to "Conj" 'right 'right "Ly")
(drop "Conj")
(inst-with-to "LClosure" (pt "x") (pt "n") "Lx" "LClosureInst1")
(by-assume "LClosureInst1" "d" "dProp")
(by-assume "dProp" "x1" "dx1Prop")
(assert "L x1 n")
 (use "dx1Prop")
(assume "Lx1")
(inst-with-to "LClosure" (pt "y") (pt "n") "Ly" "LClosureInst2")
(by-assume "LClosureInst2" "e" "eProp")
(by-assume "eProp" "y1" "ey1Prop")
(assert "L y1 n")
(use "ey1Prop")
(assume "Ly1")
(intro 0 (pt "K(d+e+i*2)"))
(intro 0 (pt "J(d+e+i*2)"))
(intro 0 (pt "x1"))
(intro 0 (pt "y1"))
(assert "Real x")
(use "LToReal" (pt "Succ n"))
(use "Lx")
(assume "Rx")
(assert "Real y")
(use "LToReal" (pt "Succ n"))
(use "Ly")
(assume "Ry")
(assert "Real x1")
(use "LToReal" (pt "n"))
(use "Lx1")
(assume "Rx1")
(assert "Real y1")
(use "LToReal" (pt "n"))
(use "Ly1")
(assume "Ry1")
(split)

(simpreal "dx1Prop")
(simpreal "ey1Prop")
(use "RealEqSToEq")
(autoreal)
(cases (pt "x1"))
(assume "as" "M" "x1Def")
(cases (pt "y1"))
(assume "bs" "N" "y1Def")
(use "RealEqSIntro")
(assume "n2")
(ng #t)
(simprat "RatTimesPlusDistr")
(simprat "RatTimesPlusDistr")
(simprat "RatTimesPlusDistr")
(simprat "RatTimesPlusDistr")
(simprat "RatTimesPlusDistr")
(simprat "RatTimesPlusDistr")
(simprat "RatTimesPlusDistr")
(simprat "RatTimesPlusDistr")
(simprat "RatTimesPlusDistr")
(simprat "RatTimesPlusDistr")
(simprat "RatTimesPlusDistr")
(ng)
(use "RatEqvTrans" (pt "(1#8)*as n2+((d#8)+(1#8)*bs n2+(e#8)+(i#4))"))
(use "Truth")
(use "RatEqvTrans"
 (pt "(1#8)*as n2+((1#8)*bs n2+(J(d+e+i*2)#8)+(K(d+e+i*2)#2))"))
(use "RatPlusCompat")
(use "Truth")
(simp (pf "(d#8)+(1#8)*bs n2=(1#8)*bs n2+(d#8)"))
(simp "<-" "RatPlusAssoc")
(simp "<-" "RatPlusAssoc")
(simp "<-" "RatPlusAssoc")
(use "RatPlusCompat")
(use "Truth")
(simprat (pf "(i#4)==(i*2#8)"))
(simprat (pf "(K(d+e+i*2)#2)==(K(d+e+i*2)*4#8)"))
(simprat "<-" "RatEqvConstrPlus")
(simprat "<-" "RatEqvConstrPlus")
(simprat "<-" "RatEqvConstrPlus")
(simp (pf "J(d+e+i*2)+K(d+e+i*2)*4=K(d+e+i*2)*4+J(d+e+i*2)"))
(simp "KJProp")
(use "Truth")
(use "IntPlusComm")
(ng #t)
(simp "<-" "IntTimesAssoc")
(use "Truth")
(ng #t)
(simp "<-" "IntTimesAssoc")
(use "Truth")
(use "RatPlusComm")
(use "Truth")
;; ?_53:Sd(K(d+e+i*2)) andd Sdtwo(J(d+e+i*2)) andd L x1 n andd L y1 n
(split)
(use "LAvcSatLClAuxK")
(use "dx1Prop")
(use "ey1Prop")
(use "Sdtwoi")
(split)
(use "LAvcSatLClAuxJ")
(use "dx1Prop")
(use "ey1Prop")
(use "Sdtwoi")
(split)
(use "Lx1")
(use "Ly1")
;; Proof finished.
;; (cp)
(save "LAvcSatLCl")

(define LAvcSatLCl-eterm (proof-to-extracted-term))
(add-var-name "tuv" (py "sdtwo yprod al yprod al"))
(define LAvcSatLCl-neterm (rename-variables (nt LAvcSatLCl-eterm)))
;; (pp LAvcSatLCl-neterm)

;; [tuv]
;;  cLAvcSatLClAuxK clft(cLClosure clft crht tuv)clft(cLClosure crht crht tuv)
;;  clft tuv pair 
;;  cLAvcSatLClAuxJ clft(cLClosure clft crht tuv)clft(cLClosure crht crht tuv)
;;  clft tuv pair 
;;  crht(cLClosure clft crht tuv)pair crht(cLClosure crht crht tuv)

;; SdtwoBoundReal
(set-goal "all k(Sdtwo k -> RealAbs k<<=2)")
(assume "i" "Sdtwoi")
(use "RatLeToRealLe")
(use "SdtwoBound")
(use "Sdtwoi")
;; Proof finished.
;; (cp)
(save "SdtwoBoundReal")

;; Putting things together.
;; LAvcToL
;; (set! COMMENT-FLAG #f)
(set-goal
 "allnc x,y,i all n(Sdtwo i andi L x n andi L y n  -> L((1#4)*(x+y+i))n)")
(cut " all n allnc x,y,i(Sdtwo i andi L x n andi L y n  -> L((1#4)*(x+y+i))n)")
(assume "CutHyp" "x" "y" "i" "n" "Conj")
(use "CutHyp")
(auto)
;; ?_3:all n allnc x,y,i(Sdtwo i andd L x n andd L y n -> L((1#4)*(x+y+i))n)
(ind)
(assume "x" "y" "i" "Conj0")
(inst-with-to "Conj0" 'left "Sdtwoi")
(inst-with-to "Conj0" 'right 'left "Lx0")
(inst-with-to "Conj0" 'right 'right "Ly0")
(drop "Conj0")
(assert "Real x")
(use-with "LToReal" (pt "x") (pt "Zero") "Lx0")
(assume "Rx")
(assert "Real y")
(use-with "LToReal" (pt "y") (pt "Zero") "Ly0")
(assume "Ry")
(intro 0)
(autoreal)
(assert "abs x<<=1")
(use-with "LToBd" (pt "x") (pt "Zero") "Lx0")
(assume "xBd")
(assert "abs y<<=1")
(use-with "LToBd" (pt "y") (pt "Zero") "Ly0")
(assume "yBd")
(simpreal "RealAbsTimes")
(use "RealLeTrans" (pt "RealAbs(1#4)*((RealPlus 1 1)+2)"))
(use "RealLeMonTimesR")
(use "RatLeToRealLe")
(use "Truth")
(use "RealLeTrans" (pt "abs(x+y)+RealAbs i"))
;; 38,39
(use "RealLeAbsPlus")
(autoreal)
(use "RealLeMonPlusTwo")
(use "RealLeTrans" (pt "abs x+abs y"))
(use "RealLeAbsPlus")
(autoreal)
(use "RealLeMonPlusTwo")
(use "xBd")
(use "yBd")
(use "SdtwoBoundReal")
(use "Sdtwoi")
(use "RatLeToRealLe")
(use "Truth")
(autoreal)
;; 7
(assume "n" "IH" "x" "y" "i" "Conj1")
(assert "exr d,j,x0,y0(
 (1#4)*(x+y+i)===(1#2)*((1#4)*(x0+y0+j)+d) andi Sd d andi 
 Sdtwo j andi L x0 n andi L y0 n)")
(use "LAvcSatLCl")
(use "Conj1")
(use-with "Id" (make-cterm (goal-to-formula (current-goal))) "?")
(assume "LAvcSatLClInst")
(by-assume "LAvcSatLClInst" "d" "dProp")
(by-assume "dProp" "j" "djProp")
(by-assume  "djProp" "x2" "djx2Prop")
(by-assume "djx2Prop" "y2" "djx2y2Prop")
(assert "Real x2")
(use "LToReal" (pt "n"))
(use "djx2y2Prop")
(assume "Rx2")
(assert "Real y2")
(use "LToReal" (pt "n"))
(use "djx2y2Prop")
(assume "Ry2")
(assert "Real x")
(use "LToReal" (pt "n+1"))
(use "Conj1")
(assume "Rx")
(assert "Real y")
(use "LToReal" (pt "n+1"))
(use "Conj1")
(assume "Ry")
(intro 1 (pt "d") (pt "(1#4)*(x2+y2+j)"))
(use "djx2y2Prop")
(use "IH")
(inst-with-to "djx2y2Prop" 'right "djx2y2PropInst")
(use "djx2y2Prop")
(use "djx2y2Prop")
;; Proof finished.
;; (cp)
(save "LAvcToL")

(define LAvcToL-eterm (proof-to-extracted-term))
;; (pp (term-to-type LAvcToL-eterm))
;; nat=>sdtwo yprod al yprod al=>al

(add-var-name "step" (py "sdtwo yprod al yprod al=>al"))
(add-var-name "dtuv" (py "sd yprod sdtwo yprod al yprod al"))
(define LAvcToL-neterm (rename-variables (nt LAvcToL-eterm)))
;; (pp LAvcToL-neterm)

;; [n]
;;  (Rec nat=>sdtwo yprod al yprod al=>al)n([tuv]U)
;;  ([n0,step,tuv][let dtuv (cLAvcSatLCl tuv) (C clft dtuv(step crht dtuv))])

;; LAverage
(set-goal "allnc x,y all n(L x(Succ n) -> L y(Succ n) -> L((1#2)*(x+y))n)")
(assume "x" "y" "n" "Lx" "Ly")
(assert "Real x")
(use "LToReal" (pt "Succ n"))
(use "Lx")
(assume "Rx")
(assert "Real y")
(use "LToReal" (pt "Succ n"))
(use "Ly")
(assume "Ry")
(cut "exr i,x0,y0((1#2)*(x+y)===(1#4)*(x0+y0+i) andi Sdtwo i andi
                  L x0 n andi L y0 n)")
;; 11,12
;; (use-with "Id" (make-cterm (goal-to-formula (current-goal))) "?")
(assume "LAvToAvcInst")
(by-assume "LAvToAvcInst" "i" "iProp")
(by-assume "iProp" "x1" "ix1Prop")
(by-assume "ix1Prop" "y1" "ix1y1Prop")
(use "LCompat" (pt "(1#4)*(x1+y1+i)"))
(use "RealEqSym")
(use "ix1y1Prop")
(use "LAvcToL")
(use "ix1y1Prop")
;; 12
(use "LAvToAvc")
(use "Lx")
(use "Ly")
;; Proof finished.
;; (cp)
(save "LAverage")

(add-var-name "tuv" (py "sdtwo yprod al yprod al"))

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

;; [n,u,u0]cLAvcToL n(cLAvToAvc u u0)

;; 2022-07-18.  Adding soundness proofs.

;; In sdcode.scm

(add-sound "EfSd")

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

;; allnc d^(F -> SdMR d^ cEfSd)

;; with computation rule

;; cEfSd eqd SdR

(deanimate "EfSd")

;; End of additions to sdcode.scm

(add-sound "LCompat")

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

;; allnc x,y,n(x===y -> allnc u^(LMR x n u^ -> LMR y n(cLCompat u^)))

;; with computation rule

;; cLCompat eqd([u]u)

(display-animation)
;; cLCompat ...

(add-sound "EfL")

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

;; F -> allnc x,n LMR x n cEfL

;; with computation rule

;; cEfL eqd U

(display-animation)
;; cEfL cLCompat ...

(add-sound "LClosure")

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

;; allnc x,n,u^(
;;  LMR x(Succ n)u^ -> 
;;  (ExRTMR int
;;    sd yprod al
;;    (cterm (d,(sd yprod al)^) 
;;    (ExRTMR rea
;;      sd yprod al
;;      (cterm (x0,(sd yprod al)^0) 
;;      (AndDMR (cterm (s^) SdMR d s^)
;;        (cterm (u^0) 
;;        (AndRMR (cterm () x===(1#2)*(x0+d)) (cterm (u^1) LMR x0 n u^1))u^0))
;;      (sd yprod al)^0))
;;    (sd yprod al)^))
;;  (cLClosure u^))

;; with computation rule

;; cLClosure eqd([u][if u (cEfSd pair U) (PairConstr sd al)])

(display-animation)
;; cLClosure cEfL cLCompat ...

(deanimate "LClosure")

(add-sound "LAvToAvc")

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

;; allnc x,y,n,u^(
;;  LMR x(Succ n)u^ -> 
;;  allnc u^0(
;;   LMR y(Succ n)u^0 -> 
;;   (ExRTMR int
;;     sdtwo yprod al yprod al
;;     (cterm (i,tuv^) 
;;     (ExRTMR rea
;;       sdtwo yprod al yprod al
;;       (cterm (x0,tuv^0) 
;;       (ExRTMR rea
;;         sdtwo yprod al yprod al
;;         (cterm (y0,tuv^1) 
;;         (AndRMR (cterm () (1#2)*(x+y)===(1#4)*(x0+y0+i))
;;           (cterm (tuv^2) 
;;           (AndDMR (cterm (t^) SdtwoMR i t^)
;;             (cterm ((al yprod al)^) 
;;             (AndDMR (cterm (u^1) LMR x0 n u^1) (cterm (u^1) LMR y0 n u^1))
;;             (al yprod al)^))
;;           tuv^2))
;;         tuv^1))
;;       tuv^0))
;;     tuv^))
;;   (cLAvToAvc u^ u^0)))

;; with computation rule

;; cLAvToAvc eqd
;; ([u,u0]
;;   cIntPlusSdToSdtwo clft(cLClosure u)clft(cLClosure u0)pair 
;;   crht(cLClosure u)pair crht(cLClosure u0))

(display-animation)
;; cLAvToAvc cEfL cLCompat ...
(deanimate "LAvToAvc")
(display-animation)
;; cEfL cLCompat ...

(add-sound "LAvcSatLClAuxJ")

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

;; allnc d,e,i,s^(
;;  SdMR d s^ -> 
;;  allnc s^0(
;;   SdMR e s^0 -> 
;;   allnc t^(SdtwoMR i t^ -> SdtwoMR(J(d+e+i*2))(cLAvcSatLClAuxJ s^ s^0 t^))))

;; with computation rule

;; cLAvcSatLClAuxJ eqd
;; ([s,s0,t]IntToSdtwo(J(SdToInt s+SdToInt s0+SdtwoToInt t*2)))

(deanimate "LAvcSatLClAuxJ")

(display-animation)
;;  cEfL cLCompat ...

(add-sound "LAvcSatLClAuxK")

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

;; allnc d,e,i,s^(
;;  SdMR d s^ -> 
;;  allnc s^0(
;;   SdMR e s^0 -> 
;;   allnc t^(SdtwoMR i t^ -> SdMR(K(d+e+i*2))(cLAvcSatLClAuxK s^ s^0 t^))))

;; with computation rule

;; cLAvcSatLClAuxK eqd([s,s0,t]IntToSd(K(SdToInt s+SdToInt s0+SdtwoToInt t*2)))

(deanimate "LAvcSatLClAuxK")
(display-animation)
;; cEfL cLCompat ...

(add-var-name "uv" (py "al yprod al"))

(add-sound "LAvcSatLCl")

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

;; allnc i,x,y,n,tuv^(
;;  (AndDMR (cterm (t^) SdtwoMR i t^)
;;    (cterm (uv^) 
;;    (AndDMR (cterm (u^) LMR x(Succ n)u^) (cterm (u^) LMR y(Succ n)u^))uv^))
;;  tuv^ -> 
;;  (ExRTMR int
;;    sd yprod sdtwo yprod al yprod al
;;    (cterm (d,dtuv^) 
;;    (ExRTMR int
;;      sd yprod sdtwo yprod al yprod al
;;      (cterm (j,dtuv^0) 
;;      (ExRTMR rea
;;        sd yprod sdtwo yprod al yprod al
;;        (cterm (x0,dtuv^1) 
;;        (ExRTMR rea
;;          sd yprod sdtwo yprod al yprod al
;;          (cterm (y0,dtuv^2) 
;;          (AndRMR (cterm () (1#4)*(x+y+i)===(1#2)*((1#4)*(x0+y0+j)+d))
;;            (cterm (dtuv^3) 
;;            (AndDMR (cterm (s^) SdMR d s^)
;;              (cterm (tuv^0) 
;;              (AndDMR (cterm (t^) SdtwoMR j t^)
;;                (cterm (uv^) 
;;                (AndDMR (cterm (u^) LMR x0 n u^) (cterm (u^) LMR y0 n u^))uv^))
;;              tuv^0))
;;            dtuv^3))
;;          dtuv^2))
;;        dtuv^1))
;;      dtuv^0))
;;    dtuv^))
;;  (cLAvcSatLCl tuv^))

;; with computation rule

;; cLAvcSatLCl eqd
;; ([tuv]
;;   cLAvcSatLClAuxK clft(cLClosure clft crht tuv)clft(cLClosure crht crht tuv)
;;   clft tuv pair 
;;   cLAvcSatLClAuxJ clft(cLClosure clft crht tuv)clft(cLClosure crht crht tuv)
;;   clft tuv pair 
;;   crht(cLClosure clft crht tuv)pair crht(cLClosure crht crht tuv))

(deanimate "LAvcSatLCl")
(display-animation)
;; cEfL cLCompat ...

(animate "Id")
(animate "LAvcToL")
(add-sound "LAvcToL")

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

;; allnc x,y,i,n,tuv^(
;;  (AndDMR (cterm (t^) SdtwoMR i t^)
;;    (cterm (uv^) (AndDMR (cterm (u^) LMR x n u^) (cterm (u^) LMR y n u^))uv^))
;;  tuv^ -> 
;;  LMR((1#4)*(x+y+i))n(cLAvcToL n tuv^))

;; with computation rule

;; cLAvcToL eqd
;; ([n]
;;   (Rec nat=>sdtwo yprod al yprod al=>al)n([tuv]U)
;;   ([n0,step,tuv]C clft(cLAvcSatLCl tuv)(step crht(cLAvcSatLCl tuv))))

(deanimate "LAvcToL")
(deanimate "Id")

(animate "Id")
(animate "LAverage")
(add-sound "LAverage")

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

;; allnc x,y,n,u^(
;;  LMR x(Succ n)u^ -> 
;;  allnc u^0(LMR y(Succ n)u^0 -> LMR((1#2)*(x+y))n(cLAverage n u^ u^0)))

;; with computation rule

;; cLAverage eqd([n,u,u0]cLAvcToL n(cLAvToAvc u u0))

(cp (theorem-name-to-proof "LAverageSound"))

;; Ok, proof is correct.
;; No free assumption variables.
;; No global assumptions used.
;; No implicit global assumptions (unproven rewrite rules).
;; Theorems used: (LCompatSound RealEqSym LAvcToLSound LAvToAvcSound LToReal)