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

; =================
;  Section: Axioms
; =================
; contains the axioms "Ax1" to "Ax10" and "AxNStrict"

; Definition: "Ax1"
; -----------------
(add-global-assumption
 "Ax1" (pf "all rhos,rho,sig,r,k,s.
            Fr rhos(rho to sig)r k ->
            N(rhos :+: ExtCtx rhos k rho)sig(r(Var k))s ->
            N rhos(rho to sig)r (ABS k rho s)"))

; Definition: "Ax2"
; -----------------
(add-global-assumption
 "Ax2" (pf "all rhos,r,s.A rhos Iota r s -> N rhos Iota r s"))

; Definition: "Ax3"
; -----------------
(add-global-assumption
 "Ax3" (pf "all rhos,rho,k.
            TypJ rhos(Var k)rho -> A rhos rho(Var k)(Var k)"))

; Definition: "Ax4"
; -----------------
(add-global-assumption
 "Ax4" (pf "all rhos,rho,sig,r,s,r1,s1.
            A rhos(rho to sig)r s -> TypJ rhos r1 rho -> 
            N rhos rho r1 s1 -> A rhos sig(r r1)(s s1)"))

; Definition: "Ax5"
; -----------------
(add-global-assumption
 "Ax5" (pf "all rhos,rho,r,s,t^.
            Head r s -> N rhos rho s t^ -> 
            TypJ rhos r rho -> N rhos rho r t^"))

; Definition: "Ax6"
; -----------------
(add-global-assumption
 "Ax6" (pf "all rho,r,s,theta.
            Head((Sub(Abs rho r)theta)s)(Sub r(Dot s theta))"))

; Definition: "Ax7"
; -----------------
(add-global-assumption
 "Ax7" (pf "all r,s,t.Head r s -> Head(r t)(s t)"))

; Definition: "Ax8"
; -----------------
(add-global-assumption
 "Ax8" (pf "all rhos,rho,r,r1,k.
            Head r r1 -> Fr rhos rho r k -> Fr rhos rho r1 k"))

; Definition: "Ax9"
; -----------------
(add-global-assumption "Ax9"
   (pf "all rhos, sigs, rho, r, s^. 
        N rhos rho r s^ -> N (rhos:+:sigs) rho r s^"))

; Definition: "Ax10"
; ------------------
(add-global-assumption
 "Ax10" (pf "all rhos,sigs,rho,r,s.
      A rhos rho r s -> A(rhos:+:sigs)rho r s"))


; Subsection: AxNStrict
; =====================

; Definition: "AxNStrict1", "AxNStrict2"
; --------------------------------------
(add-global-assumption
 "AxNStrict1" (pf "all rhos,rho,r^,s^.N rhos rho r^s^ -> E r^"))

(add-global-assumption
 "AxNStrict2" (pf "all rhos,rho,r^,s^.N rhos rho r^s^ -> E s^"))