Library assignsound

Require Import include.
Require Import memory.
Require Import memdata.
Require Import language.
Require Import opsem.
Require Import assertion.
Require Import simulation.
Require Import lemmasforseplog.
Require Import inferules.
Require Import tacticsforseplog.
Require Import includeLib.
Require Import baseTac.
Require Import auxdef.

Lemma assign_rule_sound : forall Spec sd I r ri p e1 e2 l v1 v2 tp1 tp2 aop,
                     assign_type_match tp1 tp2 ->
                    ((p ** (addrval_to_addr l)#tp1|-> v1) ==>
                      (Alval e1 tp1 l) //\\ Rv e2@tp2 == v2) ->
                    RuleSem Spec sd I r ri ((p ** (addrval_to_addr l)#tp1|-> v1)
              //\\ <|aop|>) (sassign e1 e2) (p ** (addrval_to_addr l)#tp1|-> v2 //\\ <|aop|>).