%{
   A formalization of Chapter 13 from _Types and Programming Languages_:
   the simply typed lambda-calculus with references. Only the progress and
   preservation theorems are included here (with associated lemmas).
   
   Author: Brian E. Aydemir (baydemir [at] cis.upenn.edu).
}%



%%% The one block of interest here.

%block bind : some {t:tp} block {x:exp} {d:var x t}.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Store typings reflexively extend themselves.

store_extends_refl : {S} store_extends S S -> type.
%mode store_extends_refl +S -X.

-: store_extends_refl store_nil store_extends_base.

-: store_extends_refl (store_cons _ S) (store_extends_ind P)
   <- store_extends_refl S P.

%worlds () (store_extends_refl _ _).
%total S (store_extends_refl S _).
%unique store_extends_refl +S -1P.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% If a heap is well-typed with respect to a store typing, then the length
%%% of the store typing is the same as the length of the heap.

wt_same_length_store_check :
   check_wt S1 S2 H -> length_heap H N -> length_store S2 N -> type.
%mode wt_same_length_store_check +W +L1 -L2.

-: wt_same_length_store_check
      check_wt_nil
      length_heap_nil
      length_store_nil.

-: wt_same_length_store_check
      (check_wt_cons C _)
      (length_heap_cons H)
      (length_store_cons S)
   <- wt_same_length_store_check C H S.

%worlds (bind) (wt_same_length_store_check _ _ _).
%total W (wt_same_length_store_check W _ _).
%unique wt_same_length_store_check +W +L1 -1L2.



wt_same_length_store :
   wt_heap S H -> length_heap H N -> length_store S N -> type.
%mode wt_same_length_store +W +L1 -L2.

-: wt_same_length_store (wt_heap_def C) L1 L2
   <- wt_same_length_store_check C L1 L2.

%worlds (bind) (wt_same_length_store _ _ _).
%total W (wt_same_length_store W _ _).
%unique wt_same_length_store +W +L1 -1L2.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% It is always possible to append a type to a store typing.

can_append_store : {S} {T} append_store S T S' -> type.
%mode can_append_store +S +T -A.

-: can_append_store
      store_nil
      T
      append_store_nil.

-: can_append_store
      (store_cons T1 S)
      T2
      (append_store_cons A)
   <- can_append_store S T2 A.

%worlds () (can_append_store _ _ _).
%total S (can_append_store S _ _).
%unique can_append_store +S +E -1A.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Appending something to a store typing does indeed extend it.

does_extend : append_store S T S' -> store_extends S S' -> type.
%mode does_extend +A -E.

-: does_extend append_store_nil store_extends_base.

-: does_extend (append_store_cons A) (store_extends_ind E)
   <- does_extend A E.

%worlds () (does_extend _ _).
%total A (does_extend A _).
%unique does_extend +A -1E.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% It is always possible to compute the length of a heap.

can_length_heap : {H} length_heap H N -> type.
%mode can_length_heap +H -L.

-: can_length_heap heap_nil length_heap_nil.

-: can_length_heap (heap_cons _ H) (length_heap_cons L)
   <- can_length_heap H L.

%worlds () (can_length_heap _ _).
%total H (can_length_heap H _).
%unique can_length_heap +H -1L.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% It is always possible to append an expression to a heap.

can_append_heap : {H} {E} append_heap H E H' -> type.
%mode can_append_heap +H +E -A.

-: can_append_heap heap_nil E append_heap_nil.

-: can_append_heap (heap_cons E1 H) E2 (append_heap_cons A)
   <- can_append_heap H E2 A.

%worlds () (can_append_heap _ _ _).
%total H (can_append_heap H _ _).
%unique can_append_heap +H +E -1A.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% We can always find the element we just appended to a store typing.

append_store_findable :
   %{ if   }%   append_store S T S' -> length_store S N ->
   %{ then }%   find_in_store (lbl N) S' T -> type.
%mode append_store_findable +A +L -F.

-: append_store_findable
      append_store_nil
      length_store_nil
      find_in_store_yes.

-: append_store_findable
      (append_store_cons A)
      (length_store_cons L)
      (find_in_store_no F)
   <- append_store_findable A L F.

%worlds () (append_store_findable _ _ _).
%total A (append_store_findable A _ _).
%unique append_store_findable +A +L -1F.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% We can always find the element we just appended to a heap.

append_heap_findable :
   %{ if   }%   append_heap H E H' -> length_heap H N ->
   %{ then }%   find_in_heap (lbl N) H' E -> type.
%mode append_heap_findable +A +L -F.

-: append_heap_findable append_heap_nil length_heap_nil find_in_heap_yes.

-: append_heap_findable
      (append_heap_cons A)
      (length_heap_cons L)
      (find_in_heap_no F)
   <- append_heap_findable A L F.

%worlds () (append_heap_findable _ _ _).
%total A (append_heap_findable A _ _).
%unique append_heap_findable +A +L -1F.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% If a heap is well-typed with respect to a store typing, if we can find a
%%% label in the store typing, then we can find it in the heap.

check_find_lemma :
   check_wt S1 S2 H -> find_in_store L S2 T -> find_in_heap L H E -> type.
%mode check_find_lemma +W +F1 -F2.

-: check_find_lemma
      _
      find_in_store_yes
      find_in_heap_yes.

-: check_find_lemma
      (check_wt_cons C _)
      (find_in_store_no F)
      (find_in_heap_no F')
   <- check_find_lemma C F F'.

%worlds () (check_find_lemma _ _ _).
%total F (check_find_lemma _ F _).
%unique check_find_lemma +W +F1 -1F2.



find_lemma :
   wt_heap S H -> find_in_store L S T -> find_in_heap L H E -> type.
%mode find_lemma +W +F1 -F2.

-: find_lemma (wt_heap_def C) F H
   <- check_find_lemma C F H.

%worlds () (find_lemma _ _ _).
%total {} (find_lemma _ _ _).
%unique find_lemma +W +F1 -1F2.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% If a heap is well-typed with respect to a store typing, and if we can
%%% find a label in the store typing, then we can replace its binding in the
%%% heap.

check_replace_lemma :
   %{ if   }%   {E:exp} check_wt S1 S2 H -> find_in_store L S2 T ->
   %{ then }%   replace_in_heap H L E H' -> type.
%mode check_replace_lemma +E +C +F -R.

-: check_replace_lemma
      _
      _
      find_in_store_yes
      replace_in_heap_yes.

-: check_replace_lemma
      E
      (check_wt_cons C _)
      (find_in_store_no F)
      (replace_in_heap_no R)
   <- check_replace_lemma E C F R.

%worlds () (check_replace_lemma _ _ _ _).
%total F (check_replace_lemma _ _ F _).
%unique check_replace_lemma +E +C +F -1R.



replace_lemma :
   %{ if   }%   {E:exp} wt_heap S H -> find_in_store L S T ->
   %{ then }%   replace_in_heap H L E H' -> type.
%mode replace_lemma +E +W +F -R.

-: replace_lemma E (wt_heap_def C) F R
   <- check_replace_lemma E C F R.

%worlds () (replace_lemma _ _ _ _).
%total {} (replace_lemma _ _ _ _).
%unique replace_lemma +E +W +F -1R.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Basically prove an inversion lemma for wt_heap here that lets us recover
%%% typing judgments.

check_wt_inv :
   %{ if   }%   check_wt S' S H ->
                find_in_store L S T -> find_in_heap L H E ->
   %{ then }%   of S' E T -> type.
%mode check_wt_inv +Z +Fstore +Fheap -Q.

-: check_wt_inv
      (check_wt_cons _ Q)
      find_in_store_yes
      find_in_heap_yes
      Q.

-: check_wt_inv
      (check_wt_cons C _)
      (find_in_store_no Fstore)
      (find_in_heap_no Fheap)
      Q
   <- check_wt_inv C Fstore Fheap Q.
      
%worlds (bind) (check_wt_inv _ _ _ _).
%total F (check_wt_inv _ _ F _).
%unique check_wt_inv +Z +Fstore +Fheap -1Q.



wt_heap_inv :
   %{ if   }%   wt_heap S H -> find_in_store L S T -> find_in_heap L H E ->
   %{ then }%   of S E T -> type.
%mode wt_heap_inv +Z +Fstore +Fheap -Q.

-: wt_heap_inv (wt_heap_def C) Fstore Fheap Q
   <- check_wt_inv C Fstore Fheap Q.

%worlds (bind) (wt_heap_inv _ _ _ _).
%total {} (wt_heap_inv _ _ _ _).
%unique wt_heap_inv +Z +Fstore +Fheap -1Q.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Lemma 13.5.4 (substitution). And you thought we wouldn't need this...

substitution : 
   %{ if   }%   ({x:exp} var x T2 -> of S (E1 x) T1) -> of S E2 T2 ->
   %{ then }%   of S (E1 E2) T1 -> type.
%mode substitution +D +Q1 -Q2.

-: substitution ([x] [d] t_var d) Q Q.

-: substitution ([x] [d] t_var D') _ (t_var D').

-: substitution
      ([x:exp] [d:var x T1] t_abs ([y:exp] [f:var y T2] Q1 y f x d))
      Q2
      (t_abs Q1') %% : of _ (lam T4 _) (T10 => T11))
   <- ({y:exp} {f:var y T2} substitution (Q1 y f) Q2 (Q1' y f)).

-: substitution ([x] [d] t_app (Q1 x d) (Q2 x d)) Q3 (t_app Q1' Q2')
   <- substitution Q1 Q3 Q1'
   <- substitution Q2 Q3 Q2'.

-: substitution ([x] [d] t_unit) _ t_unit.
 
-: substitution ([x] [d] t_loc L) _ (t_loc L).

-: substitution ([x] [d] t_ref (Q1 x d)) Q2 (t_ref Q1')
   <- substitution Q1 Q2 Q1'.

-: substitution ([x] [d] t_deref (Q1 x d)) Q2 (t_deref Q1')
   <- substitution Q1 Q2 Q1'.

-: substitution ([x] [d] t_assign (Q1 x d) (Q2 x d)) Q3 (t_assign Q1' Q2')
   <- substitution Q1 Q3 Q1'
   <- substitution Q2 Q3 Q2'.

%worlds (bind) (substitution _ _ _).
%total D (substitution D _ _).
%unique substitution +D +Q1 -1Q2.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Lemma 13.5.6 (but first an auxiliary, "obvious" lemma).

store_find_extends :
   find_in_store L S T -> store_extends S S' -> find_in_store L S' T -> type.
%mode store_find_extends +F1 +P -F2.

-: store_find_extends
      find_in_store_yes
      (store_extends_ind X)
      find_in_store_yes.

-: store_find_extends
      (find_in_store_no F)
      (store_extends_ind X)
      (find_in_store_no F')
   <- store_find_extends F X F'.

%worlds () (store_find_extends _ _ _).
%total F (store_find_extends F _ _).
%unique store_find_extends +F1 +P -1F2.



of_store_extends : of S1 E T -> store_extends S1 S2 -> of S2 E T -> type.
%mode of_store_extends +Q1 +P -Q2.

-: of_store_extends (t_abs Q) P (t_abs Q')
   <- ({x:exp} {d:var x T} of_store_extends (Q x d) P (Q' x d)).

-: of_store_extends (t_var V) P (t_var V).

-: of_store_extends (t_app Qarg Qfun) P (t_app Qarg' Qfun')
   <- of_store_extends Qarg P Qarg'
   <- of_store_extends Qfun P Qfun'.
   
-: of_store_extends t_unit P t_unit.

-: of_store_extends (t_loc F) P (t_loc F')
   <- store_find_extends F P F'.
   
-: of_store_extends (t_ref Q) P (t_ref Q')
   <- of_store_extends Q P Q'.

-: of_store_extends (t_deref Q) P (t_deref Q')
   <- of_store_extends Q P Q'.

-: of_store_extends (t_assign Q1 Q2) P (t_assign Q1' Q2')
   <- of_store_extends Q1 P Q1'
   <- of_store_extends Q2 P Q2'.

%worlds (bind) (of_store_extends _ _ _).
%total Q (of_store_extends Q _ _).
%unique of_store_extends +Q1 +P -1Q2.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% If a heap and related store-typing are extended appropriately, then we
%%% can extend the proof that they're well-typed as well.

extend_check_wt_store :
   check_wt S1 S2 H -> store_extends S1 S1' -> check_wt S1' S2 H -> type.
%mode extend_check_wt_store +W1 +P -W2.

-: extend_check_wt_store check_wt_nil _ check_wt_nil.

-: extend_check_wt_store (check_wt_cons C Q) P (check_wt_cons C' Q')
   <- of_store_extends Q P Q'
   <- extend_check_wt_store C P C'.

%worlds (bind) (extend_check_wt_store _ _ _).
%total W (extend_check_wt_store W _ _).
%unique extend_check_wt_store +W1 +P -1W2.



extend_check_wt :
   %{ if   }%    check_wt S1 S2 H -> of S1 E T ->
                 append_store S2 T S2' -> append_heap H E H' ->
   %{ then }%    check_wt S1 S2' H' -> type.
%mode extend_check_wt +W1 +Q +S +H -W2.

-: extend_check_wt
      check_wt_nil
      Q
      append_store_nil
      append_heap_nil
      (check_wt_cons check_wt_nil Q).

-: extend_check_wt
      (check_wt_cons C Qc)
      Q
      (append_store_cons S)
      (append_heap_cons H)
      (check_wt_cons C' Qc)
   <- extend_check_wt C Q S H C'.

%worlds (bind) (extend_check_wt _ _ _ _ _).
%total W (extend_check_wt W _ _ _ _).
%unique extend_check_wt +W1 +Q +S +H -1W2.



extend_wt_heap :
   %{ if   }%    wt_heap S H -> of S E T ->
                 append_store S T S' -> append_heap H E H' ->
   %{ then }%    wt_heap S' H' -> type.
%mode extend_wt_heap +W1 +Q +S +H -W2.

-: extend_wt_heap (wt_heap_def C) Q As Ah (wt_heap_def C'')
   <- extend_check_wt C Q As Ah C'
   <- does_extend As P
   <- extend_check_wt_store C' P C''.

%worlds (bind) (extend_wt_heap _ _ _ _ _).
%total {} (extend_wt_heap _ _ _ _ _).
%unique extend_wt_heap +W1 +Q +S +H -1W2.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Replacing an element of a heap can preserve its well-typedness with
%%% respect to a store. (Similar to Lemma 13.5.5.)

assign_lemma_check :
   %{ if   }%   check_wt S1 S2 H -> of S1 E T ->
                find_in_store L S2 T -> replace_in_heap H L E H' ->
   %{ then }%   store_extends S2 S2' -> check_wt S1 S2' H' -> type.
%mode assign_lemma_check +W1 +Q +F +R -P -W2.

-: assign_lemma_check
      (check_wt_cons C Qc : check_wt _ (store_cons T S) _)
      Q
      find_in_store_yes
      replace_in_heap_yes
      P
      (check_wt_cons C Q)
   <- store_extends_refl (store_cons T S) P.

-: assign_lemma_check
      (check_wt_cons C Qc)
      Q
      (find_in_store_no F)
      (replace_in_heap_no R)
      (store_extends_ind P)
      (check_wt_cons C' Qc)
   <- assign_lemma_check C Q F R P C'.

%worlds (bind) (assign_lemma_check _ _ _ _ _ _).
%total F (assign_lemma_check _ _ F _ _ _).
%unique assign_lemma_check +W1 +Q +F +R -1P -1W2.



assign_lemma :
   %{ if   }%   wt_heap S H -> of S E T ->
                find_in_store L S T -> replace_in_heap H L E H' ->
   %{ then }%   store_extends S S' -> wt_heap S' H' -> type.
%mode assign_lemma +W1 +Q +F +R -P -W2.

-: assign_lemma (wt_heap_def C) Q F R P' (wt_heap_def C'')
   <- assign_lemma_check C Q F R P' C'
   <- extend_check_wt_store C' P' C''.

%worlds (bind) (assign_lemma _ _ _ _ _ _).
%total {} (assign_lemma _ _ _ _ _ _).
%unique assign_lemma +W1 +Q +F +R -1P -1W2.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Preservation.

preservation :
   %{ if   }%   of S E T -> wt_heap S H -> step H E H' E' ->
   %{ then }%   store_extends S S' -> wt_heap S' H' -> of S' E' T -> type.
%mode preservation +Q1 +W1 +S1 -P1 -W2 -Q2.



%%% Easy stuff: Cases for congruence rules.

-: preservation (t_app Qarg Qfun) W (e_app1 S) P' W' (t_app Qarg' Q')
   <- preservation Qfun W S P' W' Q'
   <- of_store_extends Qarg P' Qarg'.

-: preservation (t_app Qarg Qfun) W (e_app2 S V) P' W'(t_app Q' Qfun')
   <- preservation Qarg W S P' W' Q'
   <- of_store_extends Qfun P' Qfun'.

-: preservation (t_ref Q) W (e_alloc S) P' W' (t_ref Q')
   <- preservation Q W S P' W' Q'.

-: preservation (t_deref Q) W (e_deref S) P' W' (t_deref Q')
   <- preservation Q W S P' W' Q'.
   
-: preservation (t_assign Qv Ql) W (e_gets1 S) P' W' (t_assign Qv' Ql')
   <- preservation Ql W S P' W' Ql'
   <- of_store_extends Qv P' Qv'.

-: preservation (t_assign Qv Ql) W (e_gets2 S V) P' W' (t_assign Qv' Ql')
   <- preservation Qv W S P' W' Qv'
   <- of_store_extends Ql P' Ql'.



%%% Cases for computation rules.

-: preservation
      (t_app Qarg (t_abs Qbody))
      (W : wt_heap S _)
      (e_appabs V)
      P
      W
      Qres
   <- substitution Qbody Qarg Qres
   <- store_extends_refl S P.
   
-: preservation
      (t_ref Q : of S (alloc E) (ref T))
      W
      (e_allocVal Lh Ah V)
      P
      W'
      (t_loc F')
   <- can_append_store S T As
   <- does_extend As P
   <- wt_same_length_store W Lh L
   <- append_store_findable As L F'
   <- extend_wt_heap W Q As Ah W'.

-: preservation
      (t_deref (t_loc Fstore))
      (W : wt_heap S _)
      (e_derefVal Fheap)
      P
      W
      Qres
   <- wt_heap_inv W Fstore Fheap Qres
   <- store_extends_refl S P.

-: preservation
      (t_assign Qval (t_loc F))
      W
      (e_getsVal R V)
      P'
      W'
      t_unit
   <- assign_lemma W Qval F R P' W'.



%%% No more cases.

%worlds (bind) (preservation _ _ _ _ _ _).
%total S (preservation _ _ S _ _ _).
%unique preservation +Q1 +W1 +S1 -1P1 -1W2 -1Q2.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Progress.



%%% A judgment declaring that with respect to the given heap, an expression
%%% can step or is a value.

progresses : heap -> exp -> type.
%mode progresses +H +E.

can_step : progresses H E <- step H E H' E'.
is_val   : progresses _ E <- value E.



%%% (Most of) The statement of progress.

progress : of S E T -> wt_heap S H -> progresses H E -> type.
%mode progress +Q +Z -P.



%%% Easy cases: values.

-: progress t_unit    _ (is_val v_dot).
-: progress (t_loc _) _ (is_val v_loc).
-: progress (t_abs _) _ (is_val v_lam).



%%% Less easy case: allocations.

alloc_progresses : progresses H E -> progresses H (alloc E) -> type.
%mode alloc_progresses +P1 -P2.

-: alloc_progresses
      (is_val V : progresses H E)
      (can_step (e_allocVal L A V))
   <- can_append_heap H E A
   <- can_length_heap H L.
   
-: alloc_progresses (can_step S) (can_step (e_alloc S)).

%worlds () (alloc_progresses _ _).
%total P (alloc_progresses P _).
%unique alloc_progresses +P1 -1P2.

-: progress (t_ref Q) Z P
   <- progress Q Z Pind
   <- alloc_progresses Pind P.



%%% Less easy case: applications.

app_progresses :
   %{ if   }%   of S E1 (T1 => T2) -> progresses H E1 -> progresses H E2 ->
   %{ then }%   progresses H (E1 @ E2) -> type.
%mode app_progresses +Q +P1 +P2 -P3.

-: app_progresses _ (can_step S)    _            (can_step (e_app1 S)).
-: app_progresses _ (is_val V)      (can_step S) (can_step (e_app2 S V)).
-: app_progresses _ (is_val v_lam)  (is_val V2)  (can_step (e_appabs V2)).

%worlds () (app_progresses _ _ _ _).
%total {P1 P2} (app_progresses _ P1 P2 _).
%unique app_progresses +Q +P1 +P2 -1P3.

-: progress (t_app Qarg Qbody) Z P
   <- progress Qarg Z Parg
   <- progress Qbody Z Pbody
   <- app_progresses Qbody Pbody Parg P.



%%% Less easy case: dereferences.

deref_progresses:
   %{ if   }%   of S E (ref T) -> wt_heap S H -> progresses H E ->
   %{ then }%   progresses H (deref E) -> type.
%mode deref_progresses +Q +Z +P1 -P2.

-: deref_progresses _ _ (can_step S) (can_step (e_deref S)).

-: deref_progresses
      (t_loc X)
      W
      (is_val v_loc)
      (can_step (e_derefVal Y))
   <- find_lemma W X Y.
   
%worlds () (deref_progresses _ _ _ _).
%total P (deref_progresses _ _ P _).
%unique deref_progresses +Q +Z +P1 -1P2.

-: progress (t_deref Q) Z P
   <- progress Q Z Pind
   <- deref_progresses Q Z Pind P.



%%% Less easy case: assignments.

assign_progresses:
   %{ if   }%   of S E1 (ref T) -> wt_heap S H ->
                progresses H E1 -> progresses H E2 ->
   %{ then }%   progresses H (E1 gets E2) -> type.
%mode assign_progresses +Q +Z +P1 +P2 -P3.

-: assign_progresses _ _ (can_step S) _ (can_step (e_gets1 S)).
-: assign_progresses _ _ (is_val V) (can_step S) (can_step (e_gets2 S V)).

-: assign_progresses
      (t_loc X)
      W
      (is_val v_loc)
      (is_val (V2 : value E))
      (can_step (e_getsVal Y V2))
   <- replace_lemma E W X Y.

%worlds () (assign_progresses _ _ _ _ _).
%total {P1 P2} (assign_progresses _ _ P1 P2 _).
%unique assign_progresses +Q +Z +P1 +P2 -1P3.

-: progress (t_assign Qval Qloc) Z P
   <- progress Qval Z Pval
   <- progress Qloc Z Ploc
   <- assign_progresses Qloc Z Ploc Pval P.
   


%%% No more cases.

%worlds () (progress _ _ _).
%total Q (progress Q _ _).
%unique progress +Q +Z -1P.