(def-language language-for-memory-objects
    (embedded-language  h-o-real-arithmetic)
    (base-types mem%obj word page))


(def-theory memory-objects 
    (language language-for-memory-objects)
    (component-theories h-o-real-arithmetic))

(def-cartesian-product place
    ("mem%obj" "nn")
    (theory memory-objects)
    (constructor make%place)
    (accessors mem index))

(def-cartesian-product istate
    ("[place -> word]" "[place -> place]")
    (theory memory-objects)
    (constructor make%istate)
    (accessors gamma default))

(def-theorem ()
    "forall(x:sets[[place,word],[place,place]],
      #(x,istate)
        iff 
      forsome(%y_0:[place,word],%y_1:[place,place],
          x
          =lambda(%x_0:[place,word],%x_1:[place,place],
                if(%y_0=%x_0 and %y_1=%x_1,
                    an%individual,
                    ?unit%sort))))"
    (theory  memory-objects)
    (proof
      (
        (apply-macete-with-minor-premises istate-defining-axiom_memory-objects)
        simplify
        )))


(def-translation places-to-memory 
    (source places)
    (target memory-objects)
    (fixed-theories h-o-real-arithmetic)
    (sort-pairs (place place) (istate istate))
    (constant-pairs (gamma gamma) (default default) (make%istate make%istate))
    (theory-interpretation-check using-simplification))

(def-transported-symbols (abstr bound%place copy promote raise istore regular%place ifill)
    (translation places-to-memory)
    (renamer places-to-memory-renamer))


(def-constant make%gamma 
    "lambda(g:[mem%obj, nn -> word],
            lambda(p:place,g(mem(p), index(p))))"
    (theory  memory-objects))


(def-constant make%default 
    "lambda(f:[mem%obj ->mem%obj], o:[mem%obj ->nn],
            lambda(p:place,  make%place(f(mem(p)), index(p)+o(mem(p)))))"
    (theory  memory-objects))


(def-constant make%istate_p 
    "lambda(g:[mem%obj, nn -> word], f:[mem%obj ->mem%obj], o:[mem%obj ->nn],
          make%istate(make%gamma(g), make%default(f,o)))"
    (theory  memory-objects))

(def-overloading make%istate
    (memory-objects make%istate)
    (memory-objects make%istate_p)
    (places  make%istate))


(def-constant abstr_p 
    "lambda(sigma:istate, lambda(m:mem%obj, i:nn, abstr(sigma)(make%place(m,i))))"
    (theory  memory-objects))


(def-constant twist 
    "lambda(f:[mem%obj->mem%obj], offset:[mem%obj->nn],
              lambda(p:place, 
                  make%place(f(mem(p)),index(p)+offset(mem(p)))))"
    (theory  memory-objects))


(def-constant bound%mem 
    "lambda(s:istate, indic{m:mem%obj, forsome(p:place, mem(p)=m)})"
    (theory  memory-objects))


(def-theorem raise-condition-corollary 
    "forall(f:[place,place],sigma:istate, 
        forall(x:place,  #(f(f(x))) implies 
                                        (x in bound%place(sigma) or f(x) in bound%place(sigma) or
                                      f(f(x)) in bound%place(sigma))) 
  
          implies
        raise(sigma, f)= 
        lambda(x:place, if(x in bound%place(sigma), x, f(x) in bound%place(sigma), f(x), f oo f(x))))"
    (theory places)
    (usages transportable-macete)
    (proof
      (
        (apply-macete-with-minor-premises raise-condition)
        direct-and-antecedent-inference-strategy
        simplify
        )))


(def-theorem raise-condition-variant 
    "forall(m_1, m_2:mem%obj, s:istate, f:[mem%obj->mem%obj],offset:[mem%obj->nn],
        forall(x:place,  #(twist(f,offset)(twist(f,offset)(x))) implies 
                                        (x in bound%place(s) or mem(x)=m_1 or mem(x)=m_2))
          and
        forall(x:place, mem(x)=m_1 and #(twist(f,offset)(x)) implies twist(f,offset)(x) in bound%place(s))
        and
        f(m_2)=m_1
          implies
        raise(s, twist(f,offset))= 
        lambda(x:place, if(x in bound%place(s), x, twist(f,offset)(x) in bound%place(s), twist(f,offset)(x), twist(f,offset) oo (twist(f,offset))(x))))"
    
    (theory memory-objects)
    (proof
      (
        (apply-macete-with-minor-premises tr%raise-condition-corollary)
        (move-to-sibling 2)
        (unfold-single-defined-constant (0) twist)
        (block 
          (script-comment "`apply-macete-with-minor-premises' at (1)")
          direct-and-antecedent-inference-strategy
          (antecedent-inference "with(p:prop,p and p and p);")
          (backchain "with(p:prop,
    forall(x:place,
        p and p implies 
        with(f:place,f) in with(f:sets[place],f)));")
          direct-and-antecedent-inference-strategy
          (contrapose "with(x:place,f:[place,place],s:istate,
    not(f(x) in bound%place(s)));")
          (backchain "with(p:prop,
    forall(x:place,
        p and p implies 
        with(f:place,f) in with(f:sets[place],f)));")
          direct-and-antecedent-inference-strategy
          (auto-instantiate-universal-antecedent "with(m_2,m_1:mem%obj,s:istate,offset:[mem%obj,nn],f:[mem%obj,mem%obj],
    forall(x:place,
        #(twist(f,offset)(twist(f,offset)(x)))
          implies 
        (x in bound%place(s) or mem(x)=m_1 or mem(x)=m_2)));")
          (contrapose "with(m_1,m:mem%obj,not(m=m_1));")
          (unfold-single-defined-constant (0) twist)
          simplify
          (apply-macete-with-minor-premises mem%make-place)
          simplify
          (cut-with-single-formula "#(offset(m_2))")
          simplify
          (block 
            (script-comment "`cut-with-single-formula' at (1)")
            (cut-with-single-formula "#(twist(f,offset)(x))")
            (incorporate-antecedent "with(x:place,offset:[mem%obj,nn],f:[mem%obj,mem%obj],
    #(twist(f,offset)(x)));")
            (unfold-single-defined-constant (0) twist)
            simplify))
        )))


(def-theorem raise-condition-variant-1 
    "forall(m_1, m_2:mem%obj, s:istate, f:[mem%obj->mem%obj],offset:[mem%obj->nn],
        forall(x:place,  #(twist(f,offset)(x)) implies 
                                        (x in bound%place(s) or mem(x)=m_1 or mem(x)=m_2))
          and
        forall(x:place, mem(x)=m_1 and #(twist(f,offset)(x)) implies twist(f,offset)(x) in bound%place(s))
        and
        f(m_2)=m_1
        and
        not m_1 in bound%mem(s)
          implies
        raise(s, twist(f,offset))= 
        lambda(x:place, if(x in bound%place(s), x, mem(x)=m_1, twist(f,offset)(x),  mem(x)=m_2, twist(f,offset) oo (twist(f,offset))(x), ?place)))"
    
    (theory memory-objects)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises raise-condition-variant)
        extensionality
        simplify
        direct-and-antecedent-inference-strategy
        (case-split ("mem(x_0)=m_1"))
        (block 
          (script-comment "`case-split' at (1)")
          simplify
          (case-split ("#(twist(f,offset)(x_0))"))
          (block 
            (script-comment "`case-split' at (1)")
            simplify
            (instantiate-universal-antecedent "with(p:prop,
    forall(x:place,
        p and p implies 
        with(f:place,f) in with(f:sets[place],f)));"
					("x_0"))
            simplify)
          (block 
            (script-comment "`case-split' at (2)")
            simplify
            insistent-direct-inference
            (antecedent-inference "with(p:prop,p or p);")))
        simplify
        direct-and-antecedent-inference-strategy
        (block 
          (script-comment "`direct-and-antecedent-inference-strategy' at (0)")
          (cut-with-single-formula "not twist(f,offset)(x_0) in bound%place(s)")
          simplify
          (block 
            (script-comment "`cut-with-single-formula' at (1)")
            (unfold-single-defined-constant (0) twist)
            simplify
            (incorporate-antecedent "with(m_1:mem%obj,f:sets[mem%obj],not(m_1 in f));")
            (unfold-single-defined-constant (0) bound%mem)
            simplify-insistently
            direct-and-antecedent-inference-strategy
            (contrapose "with(p:prop,forall(p:place,with(p:prop,not(p))));")
            (instantiate-existential ("make%place(m_1,offset(m_2)+index(x_0))"))
            simplify))
        simplify
        (instantiate-universal-antecedent "with(p:prop,f:place,
    forall(x:place,#(f) implies (p or p or p)));"
				            ("x_0"))
        simplify
        )))