;; 2025-06-15.  examples/analysis/digits.scm

#|
(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")
;; (set! COMMENT-FLAG #t)
|#

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

(remove-var-name "d") ;will be used as variable name for integers
(add-var-name "d" "e" (py "int"))

;; Add proper signed digits as inductive definition

(add-ids
 (list (list "Psd" (make-arity (py "int")) "boole"))
 '("Psd(IntP One)" "InitPsdTrue")
 '("Psd(IntN One)" "InitPsdFalse"))

(add-mr-ids "Psd")

(remove-var-name "b")
(add-var-name "b" (py "boole"))

;; EfPsd
(set-goal "allnc d^(F -> Psd d^)")
(assume "d^" "Absurd")
(simp (pf "d^ eqd IntP 1"))
(use "InitPsdTrue")
(use "EfEqD")
(use "Absurd")
;; Proof finished.
;; (cp)
(save "EfPsd")

;; PsdToAbsOne
(set-goal "all d(Psd d -> abs d=1)")
(assume "d" "Psdd")
(elim "Psdd")
(use "Truth")
(use "Truth")
;; Proof finished.
;; (cp)
(save "PsdToAbsOne")

;; PsdUMinus
(set-goal "allnc d(Psd d -> Psd(~d))")
(assume "d" "Psdd")
(elim "Psdd")
(use "InitPsdFalse")
(use "InitPsdTrue")
;; Proof finished.
;; (cp)
(save "PsdUMinus")

;; (define eterm (proof-to-extracted-term))
;; (define neterm (nt eterm))
;; (pp neterm)
;; [b0][if b0 False True]

(add-sound "PsdUMinus")
(deanimate "PsdUMinus")

(add-algs "sd" '("SdR" "sd") '("SdM" "sd") '("SdL" "sd"))
(add-var-name "s" (py "sd"))
(add-totality "sd")

(add-totalnc "sd")
(add-co "TotalSd")
(add-co "TotalSdNc")

(add-mr-ids "TotalSd")
(add-co "TotalSdMR")

(add-eqp "sd")
(add-eqpnc "sd")
(add-co "EqPSd")
(add-co "EqPSdNc")

(add-mr-ids "EqPBoole")
(add-mr-ids "EqPSd")
(add-co "EqPSdMR")

;; SdTotalVar
(set-goal "all s TotalSd s")
(use "AllTotalIntro")
(assume "s^" "Ts")
(use "Ts")
;; Proof finished
;; (cp)
(save "SdTotalVar")

;; SdEqToEqD
(set-goal "all s1,s2(s1=s2 -> s1 eqd s2)")
(cases)
(cases)
(assume "Useless")
(intro 0)
(assume "Absurd")
(ng)
(use "EfEqD")
(use "Absurd")
(assume "Absurd")
(ng)
(use "EfEqD")
(use "Absurd")
(cases)
(assume "Absurd")
(use "EfEqD")
(use "Absurd")
(assume "Useless")
(intro 0)
(assume "Absurd")
(use "EfEqD")
(use "Absurd")
(cases)
(assume "Absurd")
(use "EfEqD")
(use "Absurd")
(assume "Absurd")
(use "EfEqD")
(use "Absurd")
(assume "Useless")
(intro 0)
;; Proof finished.
;; (cp)
(save "SdEqToEqD")

(add-ids
 (list (list "Sd" (make-arity (py "int")) "sd"))
 '("Sd(IntPos 1)" "InitSdSdR")
 '("Sd IntZero" "InitSdSdM")
 '("Sd(IntNeg 1)" "InitSdSdL"))

(add-mr-ids "Sd")

(add-ids
 (list (list "Dsd" (make-arity (py "int")) "sd"))
 '("Dsd(IntPos(SZero 1))" "InitDsdTwo")
 '("Dsd IntZero" "InitDsdZero")
 '("Dsd(IntNeg(SZero 1))" "InitDsdMTwo"))

(add-mr-ids "Dsd")

;; EfSd
(set-goal "allnc d^(F -> Sd d^)")
(assume "d^" "Absurd")
(simp (pf "d^ eqd IntZero"))
(intro 1)
(use "EfEqD")
(use "Absurd")
;; Proof finished.
;; (cp)
(save "EfSd")

;; EfDsd
(set-goal "allnc d^(F -> Dsd d^)")
(assume "d^" "Absurd")
(simp (pf "d^ eqd IntZero"))
(intro 1)
(use "EfEqD")
(use "Absurd")
;; Proof finished.
;; (cp)
(save "EfDsd")

;; SdBound
(set-goal "allnc d(Sd d -> abs d<=1)")
(assume "d" "Sdd")
(elim "Sdd")
(use "Truth")
(use "Truth")
(use "Truth")
;; Proof finished.
;; (cp)
(save "SdBound")

;; DsdBound
(set-goal "allnc d(Dsd d -> abs d<=2)")
(assume "d" "Dsdd")
(elim "Dsdd")
(use "Truth")
(use "Truth")
(use "Truth")
;; Proof finished.
;; (cp)
(save "DsdBound")

;; IntTimesUMinusR
(set-goal "all k0,k1 k0*(~ k1)= ~(k0*k1)")
(assume "k0")
(cases)
(use "IntTimesIntNR")
(ng #t)
(use "Truth")
(assume "p")
(ng #t)
(simp "IntTimesIntNR")
(ng #t)
(use "Truth")
;; Proof finished.
;; (cp)
(save "IntTimesUMinusR")

;; SdUMinus
(set-goal "allnc d(Sd d -> Sd(~d))")
(assume "d" "Sdd")
(elim "Sdd")
(intro 2)
(intro 1)
(intro 0)
;; Proof finished.
;; (cp)
(save "SdUMinus")

;; (define eterm (proof-to-extracted-term))
;; (define neterm (rename-variables (nt eterm)))
;; (pp neterm)
;; [s][if s SdL SdM SdR]

(add-sound "SdUMinus")
(deanimate "SdUMinus")

;; DsdUMinus
(set-goal "allnc d(Dsd d -> Dsd(~d))")
(assume "d" "Dsdd")
(elim "Dsdd")
(intro 2)
(intro 1)
(intro 0)
;; Proof finished.
;; (cp)
(save "DsdUMinus")

;; (define eterm (proof-to-extracted-term))
;; (define neterm (rename-variables (nt eterm)))
;; (pp neterm)
;; [s][if s SdL SdM SdR]

(add-sound "DsdUMinus")
(deanimate "DsdUMinus")

;; Corresponding to (display-alg "int") int IntPos: pos=>int IntZero:
;; int IntNeg: pos=>int we add the algebra sdtwo as
;; either even integer <=2 or a proper signed digit

(add-algs "sdtwo"
	  '("RT" "sdtwo")
	  '("RR" "sdtwo")
	  '("MT" "sdtwo")
	  '("LT" "sdtwo")
	  '("LL" "sdtwo"))

(add-var-name "t" (py "sdtwo"))
(add-totality "sdtwo")

;; This adds the c.r. predicate TotalSdtwo of type sdtwo with clauses
;; TotalSdtwoRT:	TotalSdtwo RT
;; TotalSdtwoRR:	TotalSdtwo RR
;; TotalSdtwoMT:	TotalSdtwo MT
;; TotalSdtwoLT:	TotalSdtwo LT
;; TotalSdtwoLL:	TotalSdtwo LL

(add-totalnc "sdtwo")
(add-co "TotalSdtwo")
(add-co "TotalSdtwoNc")

(add-mr-ids "TotalSdtwo")
(add-co "TotalSdtwoMR")

(add-eqp "sdtwo")
(add-eqpnc "sdtwo")
(add-co "EqPSdtwo")
(add-co "EqPSdtwoNc")

(add-mr-ids "EqPSdtwo")
(add-co "EqPSdtwoMR")

;; SdtwoTotalVar
(set-goal "all t TotalSdtwo t")
(use "AllTotalIntro")
(assume "t^" "Tt")
(use "Tt")
;; Proof finished
;; (cp)
(save "SdtwoTotalVar")

;; SdtwoEqToEqD
(set-goal "all t1,t2(t1=t2 -> t1 eqd t2)")
(cases)
(cases)
(assume "Useless")
(use "InitEqD")
(assume "Absurd")
(use "EfEqD")
(use "Absurd")
(assume "Absurd")
(use "EfEqD")
(use "Absurd")
(assume "Absurd")
(use "EfEqD")
(use "Absurd")
(assume "Absurd")
(use "EfEqD")
(use "Absurd")
(cases)
(assume "Absurd")
(use "EfEqD")
(use "Absurd")
(assume "Useless")
(use "InitEqD")
(assume "Absurd")
(use "EfEqD")
(use "Absurd")
(assume "Absurd")
(use "EfEqD")
(use "Absurd")
(assume "Absurd")
(use "EfEqD")
(use "Absurd")
(cases)
(assume "Absurd")
(use "EfEqD")
(use "Absurd")
(assume "Absurd")
(use "EfEqD")
(use "Absurd")
(assume "Useless")
(use "InitEqD")
(assume "Absurd")
(use "EfEqD")
(use "Absurd")
(assume "Absurd")
(use "EfEqD")
(use "Absurd")
(cases)
(assume "Absurd")
(use "EfEqD")
(use "Absurd")
(assume "Absurd")
(use "EfEqD")
(use "Absurd")
(assume "Absurd")
(use "EfEqD")
(use "Absurd")
(assume "Useless")
(use "InitEqD")
(assume "Absurd")
(use "EfEqD")
(use "Absurd")
(cases)
(assume "Absurd")
(use "EfEqD")
(use "Absurd")
(assume "Absurd")
(use "EfEqD")
(use "Absurd")
(assume "Absurd")
(use "EfEqD")
(use "Absurd")
(assume "Absurd")
(use "EfEqD")
(use "Absurd")
(assume "Useless")
(use "InitEqD")
;; Proof finished.
;; (cp)
(save "SdtwoEqToEqD")

(add-ids
 (list (list "Sdtwo" (make-arity (py "int")) "sdtwo"))
 '("Sdtwo(IntP One)" "InitSdtwoRT")
 '("Sdtwo(IntP(SZero One))" "InitSdtwoRR")
 '("Sdtwo IntZero" "InitSdtwoMT")
 '("Sdtwo(IntN One)" "InitSdtwoLT")
 '("Sdtwo(IntN(SZero One))" "InitSdtwoLL"))

(add-mr-ids "Sdtwo")

;; EfSdtwo
(set-goal "allnc d^(F -> Sdtwo d^)")
(assume "d^" "Absurd")
(simp (pf "d^ eqd IntP 1"))
(use "InitSdtwoRT")
(use "EfEqD")
(use "Absurd")
;; Proof finished.
;; (cp)
(save "EfSdtwo")

;; SdtwoBound
(set-goal "all i(Sdtwo i -> abs i<=2)")
(assume "i" "Sdtwoi")
(elim "Sdtwoi")
(use "Truth")
(use "Truth")
(use "Truth")
(use "Truth")
(use "Truth")
;; Proof finished.
;; (cp)
(save "SdtwoBound")

;; SdtwoIntUMinus
(set-goal "allnc i(Sdtwo i -> Sdtwo(~i))")
(assume "i" "Sdtwoi")
(elim "Sdtwoi")
(use "InitSdtwoLT")
(use "InitSdtwoLL")
(use "InitSdtwoMT")
(use "InitSdtwoRT")
(use "InitSdtwoRR")
;; Proof finished.
;; (cp)
(save "SdtwoIntUMinus")

;; (define eterm (proof-to-extracted-term))
;; (define neterm (rename-variables (nt eterm)))
;; (pp neterm)
;; [t][if t LT LL MT RT RR]

;; IntTimesPsdToPsd
(set-goal "allnc d,e(Psd d -> Psd e -> Psd(d*e))")
(assume "d" "e")
(elim)
(elim)
(use "InitPsdTrue")
(use "InitPsdFalse")
(elim)
(use "InitPsdFalse")
(use "InitPsdTrue")
;; Proof finished.
;; (cp)
(save "IntTimesPsdToPsd")

;; (define eterm (proof-to-extracted-term))
;; (define neterm (rename-variables (nt eterm)))
;; (pp neterm)
;; [b,b0][if b b0 [if b0 False True]]

;; IntTimesSdToSd
(set-goal "allnc d,e(Sd d -> Sd e -> Sd(d*e))")
(assume "d" "e")
(elim)
(assume "Sde")
(ng #t)
(use "Sde")
(assume "Sde")
(intro 1)
(assume "Sde")
(simp "IntTimesIntNL")
(use "SdUMinus")
(use "Sde")
;; Proof finished.
;; (cp)
(save "IntTimesSdToSd")

;; (define eterm (proof-to-extracted-term))
;; (define neterm (rename-variables (nt eterm)))
;; (pp neterm)
;; [s,s0][if s s0 SdM (cSdUMinus s0)]

(add-sound "IntTimesSdToSd")
(deanimate "IntTimesSdToSd")

;; IntPlusPsdToDSd
(set-goal "allnc d,e(Psd d -> Psd e -> Dsd(d+e))")
(assume "d" "e" "Psdd" "Psde")
(elim "Psdd")
(elim "Psde")
(simp (pf "IntPlus 1 1=2*IntPos 1"))
(intro 0)
(use "Truth")
(intro 1)
(elim "Psde")
(intro 1)
(simp (pf "IntPlus(IntN 1)(IntN 1)=2*(IntN 1)"))
(intro 2)
(use "Truth")
;; (cp)
(save "IntPlusPsdToDsd")

;; (define eterm (proof-to-extracted-term))
;; (define neterm (rename-variables (nt eterm)))
;; (pp neterm)
;; [b,b0][if b [if b0 SdR SdM] [if b0 SdM SdL]]

(add-program-constant "IntHalf" (py "int=>int"))
(add-computation-rules
 "IntHalf(IntPos p)" "IntPos(PosHalf p)"
 "IntHalf IntZero" "IntZero"
 "IntHalf(IntNeg p)" "IntNeg(PosHalf p)")

;; IntHalfTotal
(set-totality-goal "IntHalf")
(use "AllTotalElim")
(cases)
(assume "p")
(ng #t)
(use "IntTotalVar")
(ng #t)
(intro 1)
(assume "p")
(ng #t)
(use "IntTotalVar")
;; Proof finished.
;; (cp)
(save-totality)

;; IntHalfDoubleId
(set-goal "all k(IntHalf(2*k)=k)")
(cases)
(cases)
(ng #t)
(use "Truth")
(assume "p")
(ng #t)
(use "Truth")
(assume "p")
(ng #t)
(use "Truth")
(ng #t)
(use "Truth")
(assume "p")
(ng #t)
(use "Truth")
;; Proof finished.
;; (cp)
(save "IntHalfDoubleId")

;; IntHalfDsdToSd
(set-goal "allnc d(Dsd d -> Sd(IntHalf d) andl d=2*(IntHalf d))")
(assume "d" "Dsdd")
(elim "Dsdd")
(ng #t)
(split)
(intro 0)
(use "Truth")
(split)
(intro 1)
(use "Truth")
(split)
(ng #t)
(intro 2)
(use "Truth")
;; Proof finished.
;; (cp)
(save "IntHalfDsdToSd")

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

(animate "IntHalfDsdToSd")

;; IntPlusPsdToSdHalf
(set-goal
 "allnc d,e(Psd d -> Psd e -> Sd(IntHalf(d+e)) andl d+e=2*IntHalf(d+e))")
(assume "d" "e" "Psdd" "Psde")
(use "IntHalfDsdToSd")
(use "IntPlusPsdToDsd")
(use "Psdd")
(use "Psde")
;; Proof finished.
;; (cp)
(save "IntPlusPsdToSdHalf")

;; (define eterm (proof-to-extracted-term))
;; (animate "IntPlusPsdToDsd")
;; (define neterm (rename-variables (nt eterm)))
;; (pp neterm)
;; [b,b0][if b [if b0 SdR SdM] [if b0 SdM SdL]]
;; (deanimate "IntPlusPsdToDsd")

;; IntPlusPsdToEq
(set-goal "allnc d,e,d0(Psd d -> Psd e -> Psd d0 -> 2*d0=d+e -> d=d0)")
(assume "d" "e" "d0")
(elim)
(elim)
(elim)
(strip)
(auto)
(elim)
(strip)
(auto)
(elim)
(elim)
(strip)
(auto)
(elim)
(strip)
(auto)
;; Proof finished.
;; (cp)
(save "IntPlusPsdToEq")

;; SdToSdtwo
(set-goal "allnc d(Sd d -> Sdtwo d)")
(assume "d")
(elim)
(intro 0)
(intro 2)
(intro 3)
;; Proof finished.
;; (cp)
(save "SdToSdtwo")

;; (define eterm (proof-to-extracted-term))
;; (define neterm (rename-variables (nt eterm)))
;; (pp neterm)
;; [s][if s RT MT LT]

;; IntPlusSdToSdtwo
(set-goal "allnc d,e(Sd d -> Sd e -> Sdtwo(d+e))")
(assume "d" "e" "Sdd" "Sde")
(elim "Sdd")
(elim "Sde")
(ng #t)
(intro 1)
(intro 0)
(intro 2)
(use "SdToSdtwo")
(use "Sde")
(elim "Sde")
(intro 2)
(intro 3)
(intro 4)
;; Proof finished.
;; (cp)
(save "IntPlusSdToSdtwo")

;; (define eterm (proof-to-extracted-term))
;; (define neterm (rename-variables (nt eterm)))
;; (pp neterm)
;; [s,s0][if s [if s0 RR RT MT] (cSdToSdtwo s0) [if s0 MT LT LL]]

(add-sound "IntPlusSdToSdtwo")
(deanimate "IntPlusSdToSdtwo")

;; IntPlusSdToDsdPsd
(set-goal "allnc d,e(Sd d -> Sd e -> Dsd(d+e) ori Psd(d+e))")
(assume "d" "e" "Sdd" "Sde")
(elim "Sdd")
(elim "Sde")
(intro 0)
(ng #t)
(intro 0)
(intro 1)
(intro 0)
(intro 0)
(intro 1)
(elim "Sde")
(intro 1)
(intro 0)
(intro 0)
(intro 1)
(intro 1)
(intro 1)
(elim "Sde")
(intro 0)
(intro 1)
(intro 1)
(intro 1)
(intro 0)
(intro 2)
;; Proof finished.
;; (cp)
(save "IntPlusSdToDsdPsd")

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

;; [s,s0]
;;  [if s
;;    [if s0 ((InL sd boole)SdR) ((InR boole sd)True) ((InL sd boole)SdM)]
;;    [if s0 ((InR boole sd)True) ((InL sd boole)SdM) ((InR boole sd)False)]
;;    [if s0 ((InL sd boole)SdM) ((InR boole sd)False) ((InL sd boole)SdL)]]

;; PsdToSd
(set-goal "allnc d(Psd d -> Sd d)")
(assume "d" "Psdd")
(elim "Psdd")
(intro 0)
(intro 2)
;; Proof finished.
;; (cp)
(save "PsdToSd")

;; (define eterm (proof-to-extracted-term))
;; (define neterm (rename-variables (nt eterm)))
;; (pp neterm)
;; [b][if b SdR SdL]

(add-sound "PsdToSd")
(deanimate "PsdToSd")

;; PsdToSdtwo
(set-goal "allnc d(Psd d -> Sdtwo d)")
(assume "d" "Psdd")
(elim "Psdd")
(intro 0)
(intro 3)
;; Proof finished.
;; (cp)
(save "PsdToSdtwo")

;; (define eterm (proof-to-extracted-term))
;; (define neterm (rename-variables (nt eterm)))
;; (pp neterm)
;; [b][if b RT LT]

(add-sound "PsdToSdtwo")
(deanimate "PsdToSdtwo")

;; IntTimesSdtwoPsdToSdtwo
(set-goal "allnc i,d(Sdtwo i -> Psd d -> Sdtwo(i*d))")
(assume "i" "d" "Sdtwoi")
(elim)
(use "Sdtwoi")
(simp (pf "i*(IntN 1)= ~(i*IntPos 1)"))
(use "SdtwoIntUMinus")
(use "Sdtwoi")
(ng #t)
(simp "IntTimesIntNR")
(use "Truth")
;; Proof finished.
;; (cp)
(save "IntTimesSdtwoPsdToSdtwo")

;; (define eterm (proof-to-extracted-term))
;; (define neterm (rename-variables (nt eterm)))
;; (pp neterm)
;; [t,b][if b t (cSdtwoIntUMinus t)]

(add-sound "IntTimesSdtwoPsdToSdtwo")
(deanimate "IntTimesSdtwoPsdToSdtwo")

;; IntSquarePsdEqOne
(set-goal "allnc d(Psd d -> d*d=1)")
(assume "d")
(elim)
(use "Truth")
(use "Truth")
;; Proof finished.
;; (cp)
(save "IntSquarePsdEqOne")

;; RealTimesPsdPsd
(set-goal "all d,x(Real x -> Psd d -> x*d*d===x)")
(assume "d" "x" "Rx" "Psdd")
(simpreal "<-" "RealTimesAssoc")
(ng #t)
(simp "IntSquarePsdEqOne")
(simpreal "RealTimesOne")
(use "RealEqRefl")
(autoreal)
(use "Psdd")
(autoreal)
;; Proof finished.
;; (cp)
(save "RealTimesPsdPsd")

;; IntPlusPsdToSdtwo
(set-goal "allnc d,e(Psd d -> Psd e -> Sdtwo(d+e))")
(assume "d" "e" "Psdd" "Psde")
(cut "Dsd(d+e)")
(elim)
(intro 1)
(intro 2)
(intro 4)
(use "IntPlusPsdToDsd")
(use "Psdd")
(use "Psde")
;; Proof finished.
;; (cp)
(save "IntPlusPsdToSdtwo")

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

;; [b,b0][if (cIntPlusPsdToDsd b b0) RR MT LL]

(add-sound "IntPlusPsdToSdtwo")
(deanimate "IntPlusPsdToSdtwo")

;; PsdPsdTpEqDisj
(set-goal "allnc d,e(Psd d -> Psd e -> d=e oru d= ~e)")
(assume "d" "e")
(elim)
(elim)
(intro 0)
(use "Truth")
(intro 1)
(use "Truth")
(elim)
(intro 1)
(use "Truth")
(intro 0)
(use "Truth")
;; Proof finished.
;; (cp)
(save "PsdPsdTpEqDisj")

;; (define eterm (proof-to-extracted-term))
;; (define neterm (rename-variables (nt eterm)))
;; (pp neterm)
;; [b,b0][if b b0 [if b0 False True]]

;; IntTimesTwoSdToSdtwo
(set-goal "allnc d(Sd d -> Sdtwo(2*d))")
(assume "d" "Sdd")
(elim "Sdd")
(intro 1)
(intro 2)
(intro 4)
;; Proof finished.
;; (cp)
(save "IntTimesTwoSdToSdtwo")

;; (define eterm (proof-to-extracted-term))
;; (define neterm (rename-variables (nt eterm)))
;; (pp neterm)
;; [s][if s RR MT LL]

;; SdToZeroOrPsd
(set-goal "allnc d(Sd d -> d=0 ori Psd d)")
(assume "d" "Sdd")
(elim "Sdd")
(intro 1)
(intro 0)
(intro 0)
(use "Truth")
(intro 1)
(intro 1)
;; Proof finished.
;; (cp)
(save "SdToZeroOrPsd")

;; (define eterm (proof-to-extracted-term))
;; (define neterm (rename-variables (nt eterm)))
;; (pp neterm)
;; [s][if s (Inr True) (DummyL boole) (Inr False)]

;; PsdTimesSdToSd
(set-goal "allnc d,e(Psd d -> Sd e -> Sd(d*e))")
(assume "d" "e" "Psdd" "Sde")
(elim "Psdd")
(use "Sde")
(simp "IntTimesIntNL")
(use "SdUMinus")
(use "Sde")
;; Proof finished.
;; (cp)
(save "PsdTimesSdToSd")

;; SdTimesPsdToSd
(set-goal "allnc d,e(Psd d -> Sd e -> Sd(e*d))")
(assume "d" "e" "Psdd" "Sde")
(elim "Psdd")
(use "Sde")
(simp "IntTimesIntNR")
(use "SdUMinus")
(use "Sde")
;; Proof finished.
;; (cp)
(save "SdTimesPsdToSd")

;; SdtwoToDsdDisjPsd
(set-goal "allnc i(Sdtwo i -> Dsd i ori Psd i)")
(assume "i" "Sdtwoi")
(elim "Sdtwoi")
(intro 1)
(intro 0)
(intro 0)
(intro 0)
(intro 0)
(intro 1)
(intro 1)
(intro 1)
(intro 0)
(intro 2)
;; Proof finished.
;; (cp)
(save "SdtwoToDsdDisjPsd")

;; PsdToTwoTimesSdtwo
(set-goal "allnc d(Psd d -> Sdtwo(2*d))")
(assume "d" "Psdd")
(elim "Psdd")
(intro 1)
(intro 4)
;; Proof finished.
;; (cp)
(save "PsdToTwoTimesSdtwo")

;; DsdToZeroDisjPsdIntHalf
(set-goal "allnc d(Dsd d -> d=0 ori Psd(IntHalf d))")
(assume "d" "Dsdd")
(elim "Dsdd")
(intro 1)
(intro 0)
(intro 0)
(use "Truth")
(intro 1)
(intro 1)
;; Proof finished.
;; (cp)
(save "DsdToZeroDisjPsdIntHalf")

;; DsdToSdtwo
(set-goal "allnc d(Dsd d -> Sdtwo d)")
(assume "d" "Dsdd")
(elim "Dsdd")
(intro 1)
(intro 2)
(intro 4)
;; Proof finished.
;; (cp)
(save "DsdToSdtwo")

;; SdtwoToSdDisjPsdIntHalf
(set-goal "allnc i(Sdtwo i -> Sd i ord Psd (IntHalf i))")
(assume "i" "Sdtwoi")
(elim "Sdtwoi")
(intro 0)
(intro 0)
(intro 1)
(intro 0)
(intro 0)
(intro 1)
(intro 0)
(intro 2)
(intro 1)
(intro 1)
;; Proof finished.
;; (cp)
(save "SdtwoToSdDisjPsdIntHalf")