; ***********************************************************
; ; 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")
;
; NOTICE: Uncomment modules only when file is run on its own
; ***********************************************************


; ==================
;  Section: Lemma 2
; ==================
; contains Lemma 2 of the Normalization Proof

; Lemma: "LemmaTwo"
; -----------------
; Lemma 2 of the Normalization Proof
; Sketch: (SC r1 -> Head r r1 -> SC r)

(set-goal (pf "allnc rho,rhos,r1,r.TypJ rhos r rho ->
                ex a^ SCr rhos rho a^r1 -> Head r r1 -> 
                ex a^ SCr rhos rho a^r"))

(cut (pf "all rho,rhos,r1,r,a^.TypJ rhos r rho ->
           SCr rhos rho a^r1 -> Head r r1 -> SCr rhos rho a^r"))
(assume "[LemmaTwoR]")
(assume "rho" "rhos" "r1" "r" "[TypJ]" "[SC]" "[Head]")
(by-assume-with "[SC]" "a^" "[SC Body]")
(ex-intro (pt "a^"))
(use "[LemmaTwoR]" (pt "r1"))
(use "[TypJ]")
(use "[SC Body]")
(use "[Head]")

; proof of LemmaTwoR:
(ind)

; Ground  type
(assume "rhos" "r1" "r" "a^" "[TypJ]" "[SCr]" "[Head]")
(use "SCrIotaFold")
(use "[TypJ]")
(use "SCrUnfoldTwo" (pt "rhos") (pt "r1"))
(use "[SCr]")
(assume "k" "[Fr]")
(use "Ax5" (pt "r1"))
(use "[Head]")
(use "SCrIotaUnfold")
(use "[SCr]")

(use "Ax8" (pt "r"))
(use "[Head]")
(use "[Fr]")
(use "[TypJ]")

; Step type
(assume "rho" "sig" "[IHrho]" "[IHsig]" "rhos" 
 "r1" "r" "a^" "[TypJ]" "[SCr]" "[Head]")
(use "SCrFold")
(use "[TypJ]")
(use "SCrUnfoldTwo" (pt "rhos") (pt "r1"))
(use "[SCr]")
(assume "sigs" "b^" "s" "[SCr 2]")
(use "[IHsig]" (pt "r1 s"))

(use "TypJAppIntro" (pt "rho"))
(use "[TypJ]")
(use "SCrUnfoldTwo" (pt "b^"))
(use "[SCr 2]")

(use "SCrUnfold" (pt "rho"))
(use "[SCr]")
(use "[SCr 2]")
(use "Ax7")
(use "[Head]")
(save "LemmaTwo")