1	import Base
2	import ../../lib/logic.bend as L
3	import ../../../spec/containers/doubly_linked_list.bend as S
4	import ../../../src/containers/doubly_linked_list.bend as D
5	import ./state.bend as ST
6	
7	# The refinement statement of one step: the implementation's result is the
8	# real list of a new shadow with an observation, the specification's the
9	# shadow's model with the same observation, and the shadow is good.
10	
11	def POK(~T: Data, -X: Data, spec: S.DS<T> & X, r: D.DList<T> & X) -> Type:
12	  Sigma<&1, &1, ST.Sh<T>, sh2 => Sigma<&1, &1, X, o => {r == (ST.real(~T, sh2), o) : D.DList<T> & X} & ({spec == (ST.model(~T, sh2), o) : S.DS<T> & X} & {ST.good(~T, sh2) == True{} : Bool})>>
13	
14	# both results rewritten
15	def pok_eq(~T: Data, -X: Data, -spec: S.DS<T> & X, -spec2: S.DS<T> & X, -r: D.DList<T> & X, -r2: D.DList<T> & X, +es: {spec == spec2 : S.DS<T> & X}, +er: {r == r2 : D.DList<T> & X}, p: POK(~T, X, spec2, r2)) -> POK(~T, X, spec, r):
16	  p1 = L.subst(D.DList<T> & X, z => POK(~T, X, spec2, z), r2, r, Equal.sym(D.DList<T> & X, r, r2, er), p)
17	  L.subst(S.DS<T> & X, z => POK(~T, X, z, r), spec2, spec, Equal.sym(S.DS<T> & X, spec, spec2, es), p1)