; ***********************************************************
; ; 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")
; (pload "./trivial.scm")
; (pload "./auxSC.scm")
; (pload "./auxGlobal_SHORT.scm")
; (pload "./auxLem1_SHORT.scm")
; (pload "./Lem1.scm")
;
; NOTICE: Uncomment modules only when file is run on its own
; ***********************************************************


; ====================================================
;  Section: Auxiliaries for the Normalization Theorem
; ====================================================
; contains all auxiliaries for the Normalization Theorem


; Subsection: "SCrsSeq"
; =====================

; Lemma: "TypJVar"
; ----------------
; an auxiliary for "SCrsSeq"
(add-global-assumption "TypJVar"
 (pf "all sigs,rhos,rho TypJ(sigs:+: (rho::rhos))(Var Lh sigs)rho"))

; Lemma: "SCrsSeq"
; ----------------
; Note: Lemma has computational content

(set-goal
 (pf "all rhos,sigs ex as^.
 SCrs(sigs:+:rhos)rhos as^ (Var map(Seq(Lh sigs)(Lh rhos)))"))

(ind)
; Base Case: (Nil type)
(assume "sigs")
(ex-intro (pt "(Nil omega)"))
(simp "ListAppendNil")
(use "SCrsDefNil")

; Step Case: r :: rhos
(assume "rho" "rhos" "[IH]" "sigs")
(inst-with-to "[IH]" (pt "sigs:+:rho:") "[IH 2]")
(by-assume-with "[IH 2]" "as^" "[IHInst]")

(assert (pf "ex a^ SCr(sigs:+: (rho::rhos)) rho a^(Var(Lh sigs))"))
(use "LemmaOne")
(use "TypJVar")
(assume "k" 4)
(ex-intro (pt "Var Lh sigs"))
(use "Ax3")
(use "TypJVar")
(assume "[SC]")

(by-assume-with "[SC]" "a^" "[SC Body]")
(ex-intro (pt "a^ ::as^"))

(ng #t)
(use "SCrsDef")
(use "SCrsSTotal" (pt "(sigs:+:rho: :+:rhos)") 
 (pt "rhos")(pt "(Var map Seq Lh(sigs:+:rho:)Lh rhos)"))
(prop)
(use "[SC Body]")
(simp (pf "(sigs:+:(rho::rhos))=(sigs:+:rho: :+:rhos)"))
(use "[IHInst]")
(simp "ListAppendAssoc")
(use "Truth-Axiom")
(save "SCrsSeq")


; Subsection: "SubIds"
; ====================

; Lemma: "SubIds"
; ---------------
(add-global-assumption "SubIds"
 (pf "all r,rhos, n.Cor rhos r -> Sub r (Wrap n (Var map(Seq 0(Lh rhos))))=r"))


; Subsection: "FrIntro1"
; ======================

; Lemma: "FrIntro1"
; -----------------
(add-global-assumption "FrIntro1"
     (pf "all rhos,r,rho.TypJ rhos r rho -> Fr rhos rho r(Lh rhos)"))