--#include "alfa/MemoryState.alfa"

package MemoryStateProofs where
  open Logic  use  subst
  open Module_Prelude  use  return,  fst,  snd
  open Module_MemoryState
   use  RelatedResult,  MostlyStateIndependent,  ReturnS_MSI,  BindS_MSI
  open Module_State
   use  StateM,  runS,  returnS,  bindS,
        inst__Monad_StateM = inst__State_11_1
  open Module_Memories  use  Range,  Memory,  EqRange
  return_MSI (A::Set)(r::Range)(a::A)
    :: MostlyStateIndependent
         A
         r
         (return (StateM Memory) A (inst__Monad_StateM Memory) a)
    = \(mem1::Memory) ->
      \(mem2::Memory) ->
      ImpliesIntro
        (EqRange r mem1 mem2)
        (RelatedResult
           A
           r
           (runS Memory A (returnS A Memory a) mem1)
           (runS Memory A (returnS A Memory a) mem2))
        (\(hyp::EqRange r mem1 mem2) ->
         AndIntro
           ((===)
              A
              (fst A Memory (runS Memory A (returnS A Memory a) mem1))
              (fst A Memory (runS Memory A (returnS A Memory a) mem2)))
           (EqRange
              r
              (snd A Memory (runS Memory A (returnS A Memory a) mem1))
              (snd A Memory (runS Memory A (returnS A Memory a) mem2)))
           Ref@_
           hyp)
  proofReturnS_MSI :: ReturnS_MSI
    = return_MSI
  bindS_MSI (A::Set)
            (B::Set)
            (m1::StateM Memory A)
            (xm2::A -> StateM Memory B)
            (r::Range)
            (pm1::MostlyStateIndependent A r m1)
            (pxm2::(a::A) -> MostlyStateIndependent B r (xm2 a))
    :: MostlyStateIndependent B r (bindS Memory A B m1 xm2)
    = \(mem1::Memory) ->
      \(mem2::Memory) ->
      ImpliesIntro
        (Module_Memories.EqRange r mem1 mem2)
        (Logic.And
           (Logic.(===)
              B
              (Module_Prelude.fst
                 B
                 Module_Memories.Memory
                 (Module_State.runS
                    Module_Memories.Memory
                    B
                    (bindS Memory A B m1 xm2)
                    mem1))
              (Module_Prelude.fst
                 B
                 Module_Memories.Memory
                 (Module_State.runS
                    Module_Memories.Memory
                    B
                    (bindS Memory A B m1 xm2)
                    mem2)))
           (Module_Memories.EqRange
              r
              (Module_Prelude.snd
                 B
                 Module_Memories.Memory
                 (Module_State.runS
                    Module_Memories.Memory
                    B
                    (bindS Memory A B m1 xm2)
                    mem1))
              (Module_Prelude.snd
                 B
                 Module_Memories.Memory
                 (Module_State.runS
                    Module_Memories.Memory
                    B
                    (bindS Memory A B m1 xm2)
                    mem2))))
        (\(eqr::EqRange r mem1 mem2) ->
         AndElimCont
           (Logic.(===)
              A
              (Module_Prelude.fst
                 A
                 Module_Memories.Memory
                 (Module_State.runS Module_Memories.Memory A m1 mem1))
              (Module_Prelude.fst
                 A
                 Module_Memories.Memory
                 (Module_State.runS Module_Memories.Memory A m1 mem2)))
           (Module_Memories.EqRange
              r
              (Module_Prelude.snd
                 A
                 Module_Memories.Memory
                 (Module_State.runS Module_Memories.Memory A m1 mem1))
              (Module_Prelude.snd
                 A
                 Module_Memories.Memory
                 (Module_State.runS Module_Memories.Memory A m1 mem2)))
           (Logic.And
              (Logic.(===)
                 B
                 (Module_Prelude.fst
                    B
                    Module_Memories.Memory
                    (Module_State.runS
                       Module_Memories.Memory
                       B
                       (bindS Memory A B m1 xm2)
                       mem1))
                 (Module_Prelude.fst
                    B
                    Module_Memories.Memory
                    (Module_State.runS
                       Module_Memories.Memory
                       B
                       (bindS Memory A B m1 xm2)
                       mem2)))
              (Module_Memories.EqRange
                 r
                 (Module_Prelude.snd
                    B
                    Module_Memories.Memory
                    (Module_State.runS
                       Module_Memories.Memory
                       B
                       (bindS Memory A B m1 xm2)
                       mem1))
                 (Module_Prelude.snd
                    B
                    Module_Memories.Memory
                    (Module_State.runS
                       Module_Memories.Memory
                       B
                       (bindS Memory A B m1 xm2)
                       mem2))))
           (ImpliesElim
              (Module_Memories.EqRange r mem1 mem2)
              (And
                 (Logic.(===)
                    A
                    (Module_Prelude.fst
                       A
                       Module_Memories.Memory
                       (Module_State.runS Module_Memories.Memory A m1 mem1))
                    (Module_Prelude.fst
                       A
                       Module_Memories.Memory
                       (Module_State.runS Module_Memories.Memory A m1 mem2)))
                 (Module_Memories.EqRange
                    r
                    (Module_Prelude.snd
                       A
                       Module_Memories.Memory
                       (Module_State.runS Module_Memories.Memory A m1 mem1))
                    (Module_Prelude.snd
                       A
                       Module_Memories.Memory
                       (Module_State.runS Module_Memories.Memory A m1 mem2))))
              (pm1 mem1 mem2)
              eqr)
           (\(a::(===)
                   A
                   (fst A Memory (runS Memory A m1 mem1))
                   (fst A Memory (runS Memory A m1 mem2))) ->
            \(b::EqRange
                   r
                   (snd A Memory (runS Memory A m1 mem1))
                   (snd A Memory (runS Memory A m1 mem2))) ->
            subst
              A
              (fst A Memory (runS Memory A m1 mem1))
              (Module_Prelude.fst A Memory (runS Memory A m1 mem2))
              (\(h::A) ->
               RelatedResult
                 B
                 r
                 (runS
                    Module_Memories.Memory
                    B
                    (bindS Module_Memories.Memory A B m1 xm2)
                    mem1)
                 (runS
                    Module_Memories.Memory
                    B
                    (xm2 h)
                    (snd
                       A
                       Module_Memories.Memory
                       (runS Module_Memories.Memory A m1 mem2))))
              a
              (ImpliesElim
                 (Module_Memories.EqRange
                    r
                    (snd A Memory (runS Memory A m1 mem1))
                    (snd A Memory (runS Memory A m1 mem2)))
                 (RelatedResult
                    B
                    r
                    (runS
                       Module_Memories.Memory
                       B
                       (bindS Module_Memories.Memory A B m1 xm2)
                       mem1)
                    (runS
                       Module_Memories.Memory
                       B
                       (xm2 (fst A Memory (runS Memory A m1 mem1)))
                       (snd
                          A
                          Module_Memories.Memory
                          (runS Module_Memories.Memory A m1 mem2))))
                 (pxm2
                    (fst A Memory (runS Memory A m1 mem1))
                    (snd A Memory (runS Memory A m1 mem1))
                    (snd
                       A
                       Module_Memories.Memory
                       (runS Module_Memories.Memory A m1 mem2)))
                 b)))
  proofBindS_MSI :: BindS_MSI
    = \(t58::Star) ->
      \(t59::Star) ->
      \(m1::Module_State.StateM Module_Memories.Memory t58) ->
      \(xm2::(h::t58) -> Module_State.StateM Module_Memories.Memory t59) ->
      \(range::Module_Memories.Range) ->
      ImpliesIntro
        ((mem1::Module_Memories.Memory) ->
         (mem2::Module_Memories.Memory) ->
         Logic.Implies
           (Module_Memories.EqRange range mem1 mem2)
           (Logic.And
              (Logic.(===)
                 t58
                 (Module_Prelude.fst
                    t58
                    Module_Memories.Memory
                    (Module_State.runS Module_Memories.Memory t58 m1 mem1))
                 (Module_Prelude.fst
                    t58
                    Module_Memories.Memory
                    (Module_State.runS Module_Memories.Memory t58 m1 mem2)))
              (Module_Memories.EqRange
                 range
                 (Module_Prelude.snd
                    t58
                    Module_Memories.Memory
                    (Module_State.runS Module_Memories.Memory t58 m1 mem1))
                 (Module_Prelude.snd
                    t58
                    Module_Memories.Memory
                    (Module_State.runS Module_Memories.Memory t58 m1 mem2)))))
        (Logic.Implies
           ((x::t58) ->
            (mem1::Module_Memories.Memory) ->
            (mem2::Module_Memories.Memory) ->
            Logic.Implies
              (Module_Memories.EqRange range mem1 mem2)
              (Logic.And
                 (Logic.(===)
                    t59
                    (Module_Prelude.fst
                       t59
                       Module_Memories.Memory
                       (Module_State.runS
                          Module_Memories.Memory
                          t59
                          (xm2 x)
                          mem1))
                    (Module_Prelude.fst
                       t59
                       Module_Memories.Memory
                       (Module_State.runS
                          Module_Memories.Memory
                          t59
                          (xm2 x)
                          mem2)))
                 (Module_Memories.EqRange
                    range
                    (Module_Prelude.snd
                       t59
                       Module_Memories.Memory
                       (Module_State.runS
                          Module_Memories.Memory
                          t59
                          (xm2 x)
                          mem1))
                    (Module_Prelude.snd
                       t59
                       Module_Memories.Memory
                       (Module_State.runS
                          Module_Memories.Memory
                          t59
                          (xm2 x)
                          mem2)))))
           ((mem1::Module_Memories.Memory) ->
            (mem2::Module_Memories.Memory) ->
            Logic.Implies
              (Module_Memories.EqRange range mem1 mem2)
              (Logic.And
                 (Logic.(===)
                    t59
                    (Module_Prelude.fst
                       t59
                       Module_Memories.Memory
                       (Module_State.runS
                          Module_Memories.Memory
                          t59
                          (Module_State.bindS
                             Module_Memories.Memory
                             t58
                             t59
                             m1
                             xm2)
                          mem1))
                    (Module_Prelude.fst
                       t59
                       Module_Memories.Memory
                       (Module_State.runS
                          Module_Memories.Memory
                          t59
                          (Module_State.bindS
                             Module_Memories.Memory
                             t58
                             t59
                             m1
                             xm2)
                          mem2)))
                 (Module_Memories.EqRange
                    range
                    (Module_Prelude.snd
                       t59
                       Module_Memories.Memory
                       (Module_State.runS
                          Module_Memories.Memory
                          t59
                          (Module_State.bindS
                             Module_Memories.Memory
                             t58
                             t59
                             m1
                             xm2)
                          mem1))
                    (Module_Prelude.snd
                       t59
                       Module_Memories.Memory
                       (Module_State.runS
                          Module_Memories.Memory
                          t59
                          (Module_State.bindS
                             Module_Memories.Memory
                             t58
                             t59
                             m1
                             xm2)
                          mem2))))))
        (\(hyp::(mem1::Module_Memories.Memory) ->
                (mem2::Module_Memories.Memory) ->
                Logic.Implies
                  (Module_Memories.EqRange range mem1 mem2)
                  (Logic.And
                     (Logic.(===)
                        t58
                        (Module_Prelude.fst
                           t58
                           Module_Memories.Memory
                           (Module_State.runS Module_Memories.Memory t58 m1 mem1))
                        (Module_Prelude.fst
                           t58
                           Module_Memories.Memory
                           (Module_State.runS Module_Memories.Memory t58 m1 mem2)))
                     (Module_Memories.EqRange
                        range
                        (Module_Prelude.snd
                           t58
                           Module_Memories.Memory
                           (Module_State.runS Module_Memories.Memory t58 m1 mem1))
                        (Module_Prelude.snd
                           t58
                           Module_Memories.Memory
                           (Module_State.runS Module_Memories.Memory t58 m1 mem2))))) ->
         ImpliesIntro
           ((x::t58) ->
            (mem1::Module_Memories.Memory) ->
            (mem2::Module_Memories.Memory) ->
            Logic.Implies
              (Module_Memories.EqRange range mem1 mem2)
              (Logic.And
                 (Logic.(===)
                    t59
                    (Module_Prelude.fst
                       t59
                       Module_Memories.Memory
                       (Module_State.runS
                          Module_Memories.Memory
                          t59
                          (xm2 x)
                          mem1))
                    (Module_Prelude.fst
                       t59
                       Module_Memories.Memory
                       (Module_State.runS
                          Module_Memories.Memory
                          t59
                          (xm2 x)
                          mem2)))
                 (Module_Memories.EqRange
                    range
                    (Module_Prelude.snd
                       t59
                       Module_Memories.Memory
                       (Module_State.runS
                          Module_Memories.Memory
                          t59
                          (xm2 x)
                          mem1))
                    (Module_Prelude.snd
                       t59
                       Module_Memories.Memory
                       (Module_State.runS
                          Module_Memories.Memory
                          t59
                          (xm2 x)
                          mem2)))))
           ((mem1::Module_Memories.Memory) ->
            (mem2::Module_Memories.Memory) ->
            Logic.Implies
              (Module_Memories.EqRange range mem1 mem2)
              (Logic.And
                 (Logic.(===)
                    t59
                    (Module_Prelude.fst
                       t59
                       Module_Memories.Memory
                       (Module_State.runS
                          Module_Memories.Memory
                          t59
                          (Module_State.bindS
                             Module_Memories.Memory
                             t58
                             t59
                             m1
                             xm2)
                          mem1))
                    (Module_Prelude.fst
                       t59
                       Module_Memories.Memory
                       (Module_State.runS
                          Module_Memories.Memory
                          t59
                          (Module_State.bindS
                             Module_Memories.Memory
                             t58
                             t59
                             m1
                             xm2)
                          mem2)))
                 (Module_Memories.EqRange
                    range
                    (Module_Prelude.snd
                       t59
                       Module_Memories.Memory
                       (Module_State.runS
                          Module_Memories.Memory
                          t59
                          (Module_State.bindS
                             Module_Memories.Memory
                             t58
                             t59
                             m1
                             xm2)
                          mem1))
                    (Module_Prelude.snd
                       t59
                       Module_Memories.Memory
                       (Module_State.runS
                          Module_Memories.Memory
                          t59
                          (Module_State.bindS
                             Module_Memories.Memory
                             t58
                             t59
                             m1
                             xm2)
                          mem2)))))
           (\(hyp'::(x::t58) ->
                    (mem1::Module_Memories.Memory) ->
                    (mem2::Module_Memories.Memory) ->
                    Logic.Implies
                      (Module_Memories.EqRange range mem1 mem2)
                      (Logic.And
                         (Logic.(===)
                            t59
                            (Module_Prelude.fst
                               t59
                               Module_Memories.Memory
                               (Module_State.runS
                                  Module_Memories.Memory
                                  t59
                                  (xm2 x)
                                  mem1))
                            (Module_Prelude.fst
                               t59
                               Module_Memories.Memory
                               (Module_State.runS
                                  Module_Memories.Memory
                                  t59
                                  (xm2 x)
                                  mem2)))
                         (Module_Memories.EqRange
                            range
                            (Module_Prelude.snd
                               t59
                               Module_Memories.Memory
                               (Module_State.runS
                                  Module_Memories.Memory
                                  t59
                                  (xm2 x)
                                  mem1))
                            (Module_Prelude.snd
                               t59
                               Module_Memories.Memory
                               (Module_State.runS
                                  Module_Memories.Memory
                                  t59
                                  (xm2 x)
                                  mem2))))) ->
            bindS_MSI t58 t59 m1 xm2 range hyp hyp'))
{-# Alfa unfoldgoals off
brief on
hidetypeannots on
wide

nd
hiding on
var "bindS_MSI" hide 2
 #-}