; ***********************************************************
; ; Adapt path if necessary:
; (define path "~/minlog/examples/tait/diplomarbeit_schlenker/")

; ; Defines the function "pload" to load files 
; ; from the path defined above
; (define pload (lambda (x) (load (string-append path x))))

; ; Used Modules:
; (pload "./initiate.scm")
; (pload "./defsLamCalc.scm")
; (pload "./defsSubst.scm")
; (pload "./omega.scm")
; (pload "./defsNT.scm")
; (pload "./defsAxiomsSpecial.scm")
; (pload "./defsAxioms.scm")
; 
; NOTICE: Uncomment modules only when file is run on its own
; ***********************************************************


; ============================================
;  Section: Lemmas for original SC Definition
; ============================================
; contains the proofs of the original SC Definition
; provided by the refined Version with SCr


; Subsection: Proof of former SC-Definition
; =========================================

; Lemma: "LemmaSCIotaUnfold"
; --------------------------
; (allnc r.SC Iota r -> FN Iota r)

(set-goal
 (pf "allnc rhos,r.ex a^ SCr rhos Iota a^r -> 
                   all k.Fr rhos Iota r k -> ex s N rhos Iota r s"))

(assume "rhos" "r" "SC r" "k" "Fr r k")
(by-assume-with "SC r" "a^" "SCr a^r")
(assert (pf "N rhos Iota r(ModIota a^k)"))
 (use "SCrIotaUnfold")
 (prop)
 (prop)
(assume "N r(ModIota a^k)")
(assert (pf "E(ModIota a^ k)"))
 (use "AxNStrict2" (pt "rhos") (pt "Iota") (pt "r"))
 (prop)
(assume "E(ModIota a^k)")
(use-with (make-proof-in-aconst-form
	   (finalg-to-expartial-ex-aconst (py "term")))
	  (make-cterm (pv "s") (pf "N rhos Iota r s"))
	  "?")
(ex-intro (pt "ModIota a^k"))
(split)
(prop)
(prop)
(save "LemmaSCIotaUnfold")

; Lemma: "LemmaSCIotaFold"
; ------------------------
; (allnc r.FN Iota r -> SC Iota r)

(set-goal
 (pf "allnc rhos,r.
       TypJ rhos r Iota ->
       (all k.Fr rhos Iota r k -> ex s N rhos Iota r s) ->
       ex a^ SCr rhos Iota a^r"))

(assume "rhos" "r" "TypJ rhos r Iota" "FN r")
(assert (pf "ex g all k.Fr rhos Iota r k -> N rhos Iota r(g k)"))
 (use-with "ACL"
	   (make-cterm (pv "k") (pf "Fr rhos Iota r k"))
	   (make-cterm (pv "k") (pv "s") (pf "N rhos Iota r s"))
	   "FN r")
(assume "FN r realizable")
(by-assume-with "FN r realizable" "g" "g realizes FN r")
(ex-intro (pt "OmegaInIota g"))
(use "SCrIotaFold")
(use "TypJ rhos r Iota")
(ng)
(use "Truth-Axiom")
(assume "k" "Fr r k")
(use "g realizes FN r")
(use "Fr r k")
(save "LemmaSCIotaFold")

; Lemma: "LemmaSCUnfold"
; ----------------------
; (allnc rho,sig,r. 
; SC (rho to sig)r -> allnc s.SC rho s -> SC sig(r s)

(set-goal
 (pf "allnc rhos,rho,sig,r.ex a^ SCr rhos(rho to sig)a^r -> 
       allnc sigs,s.ex b^ SCr(rhos:+:sigs)rho b^s -> 
                    ex c^ SCr(rhos:+:sigs)sig c^(r s)"))

(assume "rhos" "rho" "sig" "r" "SC(rho to sig)r" 
 "sigs" "s" "SC rho s")
(by-assume-with "SC(rho to sig)r" "a^" "SCr a(rho to sig)r")
(by-assume-with "SC rho s" "b^" "SCr b rho s")
(ex-intro (pt "Mod a^b^"))
(use "SCrUnfold" (pt "rho"))
(prop)
(prop)
(save "LemmaSCUnfold")

; Lemma: "LemmaSCFold"
; --------------------
; all rho,sig allnc r.
; (allnc s.SC rho s -> SC sig(r s)) -> SC(rho to sig)r

(set-goal (pf "allnc rhos all rho,sig allnc r.
                TypJ rhos r(rho to sig) ->
                (allnc sigs,s.ex b^ SCr(rhos:+:sigs)rho b^s -> 
                    ex c^ SCr(rhos:+:sigs)sig c^(r s)) -> 
                ex a^ SCr rhos(rho to sig)a^r"))

(assume "rhos" "rho" "sig" "r" "TypJ rhos r(rho to sig)"
	"allnc s.SC rho s -> SC sig(r s)")
(assert (pf "ex h^ all b^ allnc sigs,s.SCr(rhos:+:sigs)rho b^s -> 
              SCr(rhos:+:sigs)sig(h^b^)(r s)"))
 (use-with "AC" (py "omega") (py "omega")
	   (make-cterm (pv "b^") (pv "c^")
		       (pf "allnc sigs,s.SCr(rhos:+:sigs)rho b^s -> 
                            SCr(rhos:+:sigs)sig c^(r s)")) "?")
 (assume "b^")
 (use-with "UNC" (py "list type") (py "omega")
	   (make-cterm (pv "sigs") (pv "c^")
	    (pf "allnc s.SCr(rhos:+:sigs)rho b^s -> 
                         SCr(rhos:+:sigs)sig c^(r s)")) "?")
 (assume "sigs")
 (use-with "UNC" (py "term") (py "omega")
	   (make-cterm (pv "s") (pv "c^")
	    (pf "SCr(rhos:+:sigs)rho b^s -> 
                 SCr(rhos:+:sigs)sig c^(r s)")) "?")
 (assume "s")
 (inst-with-to "allnc s.SC rho s -> SC sig(r s)" (pt "sigs") "H1")
 (inst-with-to "H1" (pt "s") "H2")
 (use-with "IP" (py "omega")
    (make-cterm (pf "SCr(rhos:+:sigs)rho b^s"))
    (make-cterm (pv "c^") (pf "SCr(rhos:+:sigs)sig c^(r s)")) "?")
 (assume "H3")
 (use "H2")
 (ex-intro (pt "b^"))
 (use "H3")
(assume "ExHyp")
(by-assume-with "ExHyp" "h^" "ExHypInst")
(ex-intro (pt "Hat rho sig h^"))
(use "SCrFold")
(prop)
(use "TypeHat")
(assume "sigs" "b^" "s" "SCr b rho s")
(simp "ModHat")
(simp (pf "Equal(InOut rho b^)b^"))
(simp (pf "Equal(InOut sig(h^b^))(h^b^)"))
(use "ExHypInst")
(use "SCr b rho s")
(use "InOutId")
(use "SCrUnfoldTwo" (pt "rhos:+:sigs") (pt "r s"))
(use "ExHypInst")
(use "SCr b rho s")
(use "InOutId")
(use "SCrUnfoldTwo" (pt "rhos:+:sigs") (pt "s"))
(use "SCr b rho s")
(save "LemmaSCFold")