; ***********************************************************
; ; 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 "./subst_Joachimski_SHORT.scm")
; (pload "./omega.scm")
; (pload "./defsNT.scm")
; (pload "./defsAxiomsSpecial.scm")
; (pload "./trivial.scm")
; (pload "./auxGlobal_SHORT.scm")
; (pload "./defsPred.scm")
; (pload "./proofAxiomsGlobal_SHORT.scm")
;
; NOTICE: Uncomment modules only when file is run on its own
; ***********************************************************

; ============================================
;  Section: The Proofs of the Axioms (Part 2)
; ============================================
; builds upon the proofs in proofAxiomsGlobal;
; contains "Ax2" to "Ax10" ("Ax1" is covered in Part 1)


; Subsection: "Ax2"
; =================

; Subsubsection: Auxiliaries for "Ax2"
; ::::::::::::::::::::::::::::::::::::

; Lemma: "ATypJ"
; --------------
(set-goal (pf "all rhos,rho,r,s.
 AInd rhos rho r s ->
 TypJ rhos r rho"))

(assume "rhos" "rho" "r" "s")
(elim)
(assume "rhos2" "rho2" "k2") 
(prop)

(assume "rhos2" "rho2" "sig2"
 "r2" "s2" "r1" "s1")
(assume 1 2 3 4)
(ng)
(split)
(split)
(split)
(use-with 4 'left)
(use-with 2 'left)
(simp-with 2 'right)
(simp-with 4 'right)
(ng)
(prop)
(simp-with 4 'right) 
(ng)
(prop)
(save "ATypJ")

; Lemma "LemFoldApp"
; ------------------
(set-goal (pf "all rs,r,s.
 (FoldApp r rs)s = FoldApp r (rs:+:s:)"))

(ind)
(assume "r" "s")
(ng)
(prop)

(assume "t" "rs" 1)
(assume "r" "s")
(ng)
(use 1)
(save "LemFoldApp")

; Definition: "AAtwo"
; -------------------
(add-ids (list (list 
 "Atwo" (make-arity (py "list type")(py "type")
                     (py "term")(py "term")) ))
 '("all rhos,rho,sigs,n,rs,ss,ts.
    BNs rs ts -> Exps rhos sigs ts ss ->
    TypJ rhos (Var n) (---> sigs rho) ->
    Atwo rhos rho 
     (FoldApp (Var n) rs)
     (FoldApp (Var n) ss)" "AtwoIntro"))

; Lemma "AAtwoAux1"
; ----------------
(add-global-assumption "AAtwoAux1"
 (pf "all rs,ss,rs1,ss1.
 BNs rs ss -> BNs rs1 ss1 ->
 BNs (rs:+:rs1) (ss:+:ss1)"))

; Lemma "AAtwoAux2"
; ----------------
(add-global-assumption "AAtwoAux2"
 (pf "all rhos,sigs1,sigs2,
 rs1,rs2,ss1,ss2.
 Exps rhos sigs1 rs1 ss1 ->
 Exps rhos sigs2 rs2 ss2 ->
 Exps rhos (sigs1:+:sigs2)
  (rs1:+:rs2)(ss1:+:ss2)"))

; Lemma "AAtwoAux3"
; ----------------
(add-global-assumption "AAtwoAux3"
 (pf "all sigs,rho,sig.
 --->(sigs:+:rho:)sig =
 --->sigs(rho to sig)"))

; Lemma: "AAtwo"
; --------------
(set-goal (pf "all rhos,rho,r,s.
 AInd rhos rho r s -> Atwo rhos rho r s"))

(assume "rhos" "rho" "r" "s")
(elim)

; Case 1
(assume "rhos1" "rho1" "k" 1)
(simp (pf "(Var k)= 
 FoldApp (Var k) (Nil term)"))
(intro 0 (pt "(Nil type)")
 (pt "(Nil term)"))
(intro 0)
(intro 0)
(ng)
(use 1)
(ng)
(prop)

; Case 2
(assume "rhos1" "rho1" "sig1" 
 "r2" "s2" "r1" "s1")
(assume 1 2 3 4)

; Inversion on Atwo
(inversion 4)

(assume "rhos2" "rho2" "sigs2" 
 "n2" "rs2" "ss2" "ts2")
(assume 1 2 3 4 5 6 7)

(simp 10)
(simp 11)

(simp (pf "(FoldApp(Var n2)rs2 r1) =
 (FoldApp(Var n2) (rs2:+:r1:))"))
(simp (pf "(FoldApp(Var n2)ss2 s1) =
 (FoldApp(Var n2) (ss2:+:s1:))"))

; Inversion on N
(inversion 3)
(assume "rhos3" "rho3" "r3"
 "s3" "t3") 
(assume 1 2 3 4 5 6 7)

(intro 0 (pt "(sigs2:+:rho1:)")
 (pt "(ts2:+:t3:)"))

(use "AAtwoAux1")
(use 5)
(intro 1)
(simp 17)
(use 13)
(intro 0)

(use "AAtwoAux2")
(simp 8)
(use 6)
(intro 1)
(simp 15)
(simp 16)
(simp 18)
(use 14)
(intro 0)

(simp (pf "(--->(sigs2:+:rho1:)sig1) =
(---> sigs2 (rho1 to sig1))"))
(simp 9)
(simp 8)
(use 7)

(use "AAtwoAux3")

(use "LemFoldApp")
(use "LemFoldApp")
(save "AAtwo")


; Subsubsection: Proof of "Ax2"
; :::::::::::::::::::::::::::::

; Lemma: "Ax2Ind"
; ---------------
(set-goal (pf " all rhos,r,s.
 AInd rhos Iota r s -> 
 NInd rhos Iota r s"))

(assume "rhos" "r" "s")
(assume 1)
(assert (pf "Atwo rhos Iota r s"))
(use "AAtwo")
(use 1)
(assume 1)

; Inversion on Atwo
(inversion 2)
(assume "rhos2" "rho2" "sigs2"
"n2" "rs2" "ss2" "ts2")
(assume 1 2 3 4 5 6 7)
(simp 8)
(simp 9)
(intro 0 (pt "(FoldApp (Var n2) ts2)"))

; TypJ
(simp "<-" 8)
(use "ATypJ" (pt "s"))
(use 1)

; BN
(intro 0)
(use 3)

; Exp
(simp (pf "rhos= (rhos:+:(Nil type))"))
(intro 0 (pt "sigs2") (pt "ss2"))

; TypJ
(simp 7)
(simp "<-" 
 (pf "rhos = rhos:+:(Nil type)"))
(simp 6)
(use 5)
(use "NilAppend")

; Exps
(simp "<-" 
 (pf "rhos = rhos:+:(Nil type)"))
(simp 6)
(use 4)
(use "NilAppend")
(ng)
(prop)
(use "NilAppend")
(save "Ax2Ind")


; Lemma: "Ax2"
; ------------
(set-goal (pf " all rhos,r,s.
 A rhos Iota r s -> 
 N rhos Iota r s"))

(assume "rhos" "r" "s" 1)
(use "NDefRev")
(assert (pf "AInd rhos Iota r s"))
(use "ADef")
(use 1)
(use "Ax2Ind")
(save "Ax2")


; Subsection: "Ax3"
; =================

; Lemma: "Ax3"
; ------------
(set-goal (pf "all rhos,rho,k. 
 TypJ rhos(Var k)rho -> A rhos rho(Var k)(Var k)"))

(assume "rhos" "rho" "k" 1)
(use "ADefRev")
(intro 0)
(use 1)
(save "Ax3")


; Subsection: "Ax4"
; =================

; Lemma: "Ax4Ind"
; ---------------
(set-goal
 (pf "all rhos,rho,sig,r,s,r1,s1.
 AInd rhos(rho to sig)r s ->
 TypJ rhos r1 rho -> 
 NInd rhos rho r1 s1 -> 
 AInd rhos sig(r r1)(s s1)"))

(assume "rhos" "rho" "sig" "r" "s"
 "r1" "s1")
(assume 1 2 3)
(intro 1 (pt "rho"))
(use 1)
(use 2)
(use 3)
(save "Ax4Ind")

; Lemma: "Ax4"
; ------------
(set-goal
 (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)"))

(assume "rhos" "rho" "sig" "r" "s"
 "r1" "s1")
(assume 1 2 3)
(use "ADefRev")
(assert (pf "NInd rhos rho r1 s1"))
(use "NDef")
(use 3)
(assert (pf "TypJ rhos r1 rho"))
(use 2)
(assert (pf "AInd rhos(rho to sig)r s"))
(use "ADef")
(use 1)
(use "Ax4Ind")
(save "Ax4")


; Subsection: "Ax5"
; =================

(add-program-constant "Id" 
 (py "term => term") 1)

(add-computation-rule (pt "Id r")
                      (pt "r"))
; Lemma: "Ax5Ind"
; ---------------
(set-goal
 (pf "all rhos,rho,r,s,t^.
 HeadInd r s -> NInd rhos rho s t^ ->
 TypJ rhos r rho -> NInd rhos rho r t^"))

(assume "rhos" "rho" "r" "s" "t^")
(elim)
(assume "rho1" "r1" "s1" "rs")
(assume 1)

(assert (pf "
 Id (FoldApp(Sub r1(Dot s1(Up 0)))rs) =
 (FoldApp(Sub r1(Dot s1(Up 0)))rs)"))
(ng)
(prop)

(assume 1)
(assert (pf " NInd rhos rho 
 (Id (FoldApp(Sub r1(Dot s1(Up 0)))rs)) t^"))
(simp 2)
(use 1)
(assume 1)

(assert (pf "
 Id (FoldApp(Sub r1(Dot s1(Up 0)))rs) =
 (FoldApp(Sub r1(Dot s1(Up 0)))rs)"))
(use 2)

(assert (pf " NInd rhos rho 
 (Id (FoldApp(Sub r1(Dot s1(Up 0)))rs)) t^"))
(use 3)

(elim)
(assume "rhos2" "rho2" "r2" "s2" "t2")
(assume 1 2 3 4 5)
(intro 0 (pt "t2"))
(use 8)

(simp (pf "(FoldApp(Abs rho1 r1 s1)rs) = 
(FoldApp(Abs rho1 r1) (s1::rs))"))
(intro 2)
(ng #t)

(simp "<-" 7)
(use 5)
(ng)
(prop)
(use 6)
(save "Ax5Ind")

; Lemma: "Ax5"
; ------------
(set-goal
 (pf "all rhos,rho,r,s,t^.
 Head r s -> N rhos rho s t^ -> 
 TypJ rhos r rho -> N rhos rho r t^"))

(assume "rhos" "rho" "r" "s" "t^" 1 2 3)
(use "NDefRev")
(assert (pf "TypJ rhos r rho"))
(use 3)
(assert (pf "NInd rhos rho s t^"))
(use "NDef")
(use 2)
(assert (pf "HeadInd r s"))
(use "HeadDef")
(use 1)
(use "Ax5Ind")
(save "Ax5")


; Subsection: "Ax6"
; =================

; Subsubsection: Auxiliaries for "Ax6"
; ::::::::::::::::::::::::::::::::::::

; Lemma: "UpIdGeneral"
; --------------------
; a more general lemma to prove "UpId"

(set-goal
  (pf "all r,n.Sub r (Spare n (Up n)) = r"))

(ind)
(assume "k")
(cases)
(ng)
(prop)

(assume "n")
(casedist (pt "k< Succ n"))
(use "SubVarSpareLt")
(assume 1)
(assert (pf "k=(k-Succ n)+Succ n"))

(use "Trivial10")
(use 1)
(assume 1)
(simp 2)
(simp "SubVarSpare")
(ng)
(prop)

; Case: App
(assume "r" "s" "IH r" "IH s")
(assume "n")
(ng)
(split)
(use 1)
(use 2)

; Case: Abs
(assume "rho" "r" "IH")
(assume "n")
(ng)
(inst-with "IH" (pt "Succ n"))
(simp "DotVarSubliftSpare")
(ng)
(use 2)
(save "UpIdGeneral")

; Lemma: "UpId"
; -------------
(set-goal
  (pf "all r.Sub r (Up 0) = r"))

(assume "r")
(assert (pf "Up 0 = (Spare 0 (Up 0))"))
(ng)
(prop)
(assume 1)
(simp 1)
(use "UpIdGeneral")
(save "UpId")

; Lemma: "Ax6AuxAux"
; ---------------------
(set-goal
 (pf "all r,s. Sub (Lift r 0 1) (Dot s (Up 0)) = r "))

(assume "r" "s")
(assert 
 (pf "Sub(Lift r 0 (Lh (s:)))(Spare 0 (Pushlist (s:) (Up 0))) =
      Sub r (Spare 0 (Up 0))"))
(use "SubLiftSpare")
(assume 1)
(ng)
(simp-with 1)
(use "UpId")
(save "Ax6AuxAux")


; Lemma: "Ax6Aux"
; ---------------
(set-goal
 (pf "all theta, s. (Sublift theta 1) circ (Dot s (Up 0)) =
                    theta"))

(ind)
(assume "n" "s")
(ng)
(prop)

(assume "r" "theta" "IH")
(assume "s")
(ng)
(split)
(use "Ax6AuxAux")
(use 1)
(save "Ax6Aux")


; Subsubsection: Proof of "Ax6"
; :::::::::::::::::::::::::::::

; Lemma: "Ax6Ind"
; ---------------
(set-goal (pf "all rho,r,s,theta 
 HeadInd((Sub(Abs rho r)theta)s)(Sub r(Dot s theta))"))

(assume "rho" "r" "s" "theta")
(ng)

(assert 
 (pf "(Sub (Sub r (Dot(Var 0)(Sublift theta 1))) (Dot s (Up 0))) =
      (Sub r (Dot(Var 0)(Sublift theta 1) circ (Dot s (Up 0)) ))"))
(use "SubSub") ;Joachimski lemma
(assume 2)

(assert (pf "HeadInd
 ((Abs rho (Sub r(Dot(Var 0)(Sublift theta 1)))) s)
 ((Sub (Sub r(Dot(Var 0)(Sublift theta 1))) (Dot s (Up 0))))"))

(simp (pf "((Abs rho (Sub r(Dot(Var 0)(Sublift theta 1)))) s) =
FoldApp ((Abs rho (Sub r(Dot(Var 0)(Sublift theta 1)))) s) 
 (Nil term)"))
(simp 
 (pf "((Sub (Sub r(Dot(Var 0)(Sublift theta 1))) (Dot s (Up 0)))) =
      FoldApp ((Sub (Sub r(Dot(Var 0)(Sublift theta 1))) 
       (Dot s (Up 0)))) (Nil term)"))

(intro 0)
(ng)
(prop)
(ng)
(prop)

(simp-with 1)
(ng)
(simp-with "Ax6Aux" (pt "theta") (pt "s"))
(prop)
(save "Ax6Ind")

; Lemma: "Ax6"
; ------------
(set-goal
 (pf "all rho,r,s,theta 
      Head((Sub(Abs rho r)theta)s)(Sub r(Dot s theta))"))

(assume "rho" "r" "s" "theta")
(use "HeadDefRev")
(use "Ax6Ind")
(save "Ax6")


; Subsection: "Ax7"
; =================

; Subsubsection: Auxiliaries for "Ax7"
; ::::::::::::::::::::::::::::::::::::

; Lemma: "Ax7Aux"
; ---------------
(set-goal (pf "all t,rs,r.
 (FoldApp r rs) t = (FoldApp r (rs:+:(t:)))")) 

(assume "t")
(ind)
(assume "r")
(ng)
(prop)

(assume "s" "ss" "IH")
(assume "r")
(ng)
(use "IH")
(save "Ax7Aux")


; Subsubsection: Proof of "Ax7"
; :::::::::::::::::::::::::::::

; Lemma: "Ax7Ind"
; ---------------
(set-goal (pf "all r,s,t.
 HeadInd r s -> HeadInd(r t)(s t)"))

(assume "r" "s" "t")
(elim)
(assume "rho" "r1" "s1" "rs")
(simp "Ax7Aux")
(simp "Ax7Aux")
(intro 0)
(save "Ax7Ind")

; Lemma: "Ax7"
; ------------
(set-goal (pf "all r,s,t.
 Head r s -> Head(r t)(s t)"))

(assume "r" "s" "t" 1)
(use "HeadDefRev")
(assert (pf "HeadInd r s"))
(use "HeadDef")
(use 1)
(use "Ax7Ind")
(save "Ax7")


; Subsection: "Ax8"
; =================

; Subsubsection: Auxiliaries for "Ax8"
; ::::::::::::::::::::::::::::::::::::

; Lemma: "HeadTypJAux1Aux1"
; -------------------------
(add-global-assumption "HeadTypJAux1Aux1"
 (pf "all rhos,r,s,ss.
 Cor rhos(FoldApp(r s)ss) -> Cor rhos (r s)"))

; Lemma: "HeadTypJAux1Aux2"
; -------------------------
(add-global-assumption "HeadTypJAux1Aux2"
 (pf "all rhos,r,r1,s,ss.
      Cor rhos(FoldApp(r s)ss) -> 
      Typ rhos r=Typ rhos r1 ->
      Cor rhos(FoldApp(r1 s)ss)"))

; Lemma: "HeadTypJAux1"
; ---------------------
(set-goal (pf "all rhos, r, r1, rho, sig.
 TypJ rhos r sig -> TypJ rhos r1 sig ->
 TypJ rhos(FoldApp r rs)rho -> 
 TypJ rhos(FoldApp r1 rs)rho"))

(ind)
(assume "rhos" "r" "r1" "rho" "sig" 1 2 3)
(ng)
(split)
(use-with 2 'left)
(simp (pf "Typ rhos r1 = Typ rhos r"))
(use-with 3 'right)
(simp-with 1 'right)
(use-with 2 'right)

(assume "s" "ss" "IH")
(assume "rhos" "r" "r1" "rho" "sig" 1 2 3)
(ng)
(inst-with "IH" (pt "rhos") (pt "(r s)")
 (pt "(r1 s)") (pt "rho") (pt "Typ rhos (r s)"))
(use 5)
(split)

(use "HeadTypJAux1Aux1" (pt "ss"))
(use-with 4 'left)
(prop)

(split)
(use "HeadTypJAux1Aux1" (pt "ss"))
(use "HeadTypJAux1Aux2" (pt "r"))
(use-with 4 'left)
(simp-with 3 'right)
(use-with 2 'right)
(ng)
(simp-with 3 'right)
(simp-with 2 'right)
(prop)
(use 4)
(save "HeadTypJAux1")

; Lemma: "HeadTypJAux2"
; --------------------
(add-global-assumption "HeadTypJAux2"
 (pf "all rhos,r,rs,rho. TypJ rhos(FoldApp r rs)rho ->
      Cor rhos r"))

; Lemma: "HeadTypJ"
; -----------------
; needs Subject Reduction

(set-goal (pf "all rho,rhos,r,r1.
 HeadInd r r1 -> TypJ rhos r rho -> TypJ rhos r1 rho"))

(assume "rho" "rhos" "r" "r1")
(elim)
(assume "rho1" "r2" "s" "rs" 1)
(use "HeadTypJAux1" 
 (pt "(Abs rho1 r2 s)") (pt "Typ rhos (Abs rho1 r2 s)"))
(use "CorTypJ")

(use "HeadTypJAux2" (pt "rs") (pt "rho"))
(use 1)
(simp (pf "(Dot s(Up 0)) = (Wrap 0 (s:))"))
(use "SR" (pt "rho1") )

(use "CorTypJ")
(use "HeadTypJAux2" (pt "rs") (pt "rho"))
(use 1)

(ng)
(prop)
(use 1)
(save "HeadTypJ")


; Subsubsection: Proof of "Ax8"
; :::::::::::::::::::::::::::::

; Lemma: "Ax8Ind"
; ----------------
(set-goal (pf "all rhos,rho,r,r1,k.
 HeadInd r r1 -> Fr rhos rho r k -> 
 Fr rhos rho r1 k"))

(assume "rhos" "rho" "r" "r1" "k")
(assume 1 2)
(use "FrDefRev")
(assert (pf "TypJ rhos r rho"))
(use "FrDef" (pt "k"))
(use 2)
(assume 1)
(use "HeadTypJ" (pt "r"))
(use 1)
(use 3)
(use "FrDef" (pt "rho") (pt "r") )
(use 2)
(save "Ax8Ind")

; Lemma: "Ax8"
; ------------

(set-goal (pf "all rhos,rho,r,r1,k.
 Head r r1 -> Fr rhos rho r k -> 
 Fr rhos rho r1 k"))

(assume "rhos" "rho" "r" "r1" "k")
(assume 1 2)
(use "Ax8Ind" (pt "r"))
(use "HeadDef")
(use 1)
(use 2)
(save "Ax8")


; Subsection: "Ax9"
; =================

; Subsubsection: Auxiliaries for "Ax9"
; ::::::::::::::::::::::::::::::::::::

; Lemma: "ExpExtCtx"
; ------------------
(set-goal (pf "Exp rhos rho r s ->
 Exp(rhos:+:sigs)rho r s"))

(assume "rhos" "rho" "r" "s" "sigs")
(elim (pf "Exps rhos sigs2 rs ss -> 
 Exps (rhos:+:sigs) sigs2 rs ss"))

; Case 1
(assume "rhos2" "sigs2" 
 "rs2" "ss2" "k2" "t2" "rho2")
(assume 1 2 3 4)
(intro 0 (pt "sigs2")(pt "ss2"))
(use "TypJExtCtx")
(use 1)
(use 4)
(use 3)

; Case 2
(assume "rhos3" "rhos4" "sigs2" "taus2" "rho2"
 "sig2" "r2" "s2" "k2")
(assume 1 2 3 4)
(simp (pf "(rhos3:+:taus2:+:sigs) =
 (rhos3:+:(taus2:+:sigs))"))
(intro 1 (pt "rhos4") (pt "sigs2"))
(use 1)
(use 2)
(use 3)
(use "ListAssoc")

; Case 3
(assume "rhos3")
(intro 0)

; Case 4
(assume "rhos2" "sigs2"
 "r2" "s2" "rs2" "ss2")
(assume 1 2 3 4)
(intro 1)
(use 3)
(use 4)
(save "ExpExtCtx")


; Subsubsection: Proof of "Ax9"
; :::::::::::::::::::::::::::::

; Lemma: "Ax9Ind"
; ---------------
(set-goal
   (pf "all sigs,rhos,rho,r,s^. 
        NInd rhos rho r s^ -> 
        NInd (rhos:+:sigs) rho r s^"))

(assume "sigs" "rhos" "rho" "r" "s^")
(elim)

(assume "rhos1" "rho1" "r1" "s1" "t1")
(assume 1 2 3)
(intro 0 (pt "t1"))
(use "TypJExtCtx")
(use 1)

; BN
(use 2)

; Exp
(use "ExpExtCtx")
(use 3)
(save "Ax9Ind")

; Lemma: "Ax9"
; -------------
(set-goal
   (pf "all sigs,rhos,rho,r,s^. 
        N rhos rho r s^ -> 
        N (rhos:+:sigs) rho r s^"))

(assume "sigs" "rhos" "rho" "r" "s^")
(assume 1)
(use "NDefRev")
(assert (pf "NInd rhos rho r s^"))
(use "NDef")
(use 1)
(use "Ax9Ind")
(save "Ax9")


; Subsection: "Ax10"
; =================

; Lemma: "Ax10Ind"
; ---------------

(set-goal
  (pf "all sigs,rhos,rho,r,s.
      AInd rhos rho r s -> AInd(rhos:+:sigs)rho r s"))

(assume "sigs" "rhos" "rho" "r" "s")
(elim)

; Case 1
(assume "rhos1" "rho1" "k1" 1)
(intro 0)
(use "TypJExtCtx")
(use 1)

; Case 2
(assume "rhos2" "rho2" "sig2" "r2" "s2" "r1" "s1")
(assume 1 2 3 4)
(intro 1 (pt "rho2"))
(use 4)
(use "TypJExtCtx")
(use 2)

(use "Ax9Ind")
(use 3)
(save "Ax10Ind")

; Lemma: "Ax10"
; ------------
(set-goal
  (pf "all sigs,rhos,rho,r,s.
      A rhos rho r s -> A(rhos:+:sigs)rho r s"))

(assume "sigs" "rhos" "rho" "r" "s" 1)
(use "ADefRev")
(assert (pf "AInd rhos rho r s"))
(use "ADef")
(use 1)
(use "Ax10Ind")
(save "Ax10")


; Subsection: AxNStrict
; =====================
; used in auxSC.scm

; Lemma: "AxNStrict1Ind"
; ----------------------

(set-goal
 (pf "all rhos,rho,r^,s^.NInd rhos rho r^s^ -> E r^"))

(assume "rhos" "rho" "r^" "s^")
(elim)
(assume "rhos1" "rho1" "r1" "s1" "t1")
(assume 1 2 3)
(ng)
(prop)
(save "AxNStrict1Ind")

; Lemma: "AxNStrict1"
; ----------------------
(set-goal
 (pf "all rhos,rho,r^,s^.N rhos rho r^s^ -> E r^"))

(assume "rhos" "rho" "r^" "s^")
(assume 1)
(assert (pf "NInd rhos rho r^s^"))
(use "NDef")
(use 1)
(use "AxNStrict1Ind")
(save "AxNStrict1")


; Lemma: "AxNStrict2Ind"
; ----------------------
(set-goal
 (pf "all rhos,rho,r^,s^.NInd rhos rho r^s^ -> E s^"))

(assume "rhos" "rho" "r^" "s^")
(elim)
(assume "rhos1" "rho1" "r1" "s1" "t1")
(assume 1 2 3)
(ng)
(prop)
(save "AxNStrict2Ind")

; Lemma: "AxNStrict2"
; -------------------
(set-goal
 (pf "all rhos,rho,r^,s^.N rhos rho r^s^ -> E s^"))

(assume "rhos" "rho" "r^" "s^")
(assume 1)
(assert (pf "NInd rhos rho r^s^"))
(use "NDef")
(use 1)
(use "AxNStrict2Ind")
(save "AxNStrict2")