1 | 9. trace_consistent_rel(rho;A.da;tr.proj;r) 10. single_valued_decls(A.ds) 11. s: [[A]] rho de e.state 12. x': [[A]] rho de e.state 13. tc(r;A.ds;dec_lookup(A.da;kind(a));de) 14. covers_rel(A;r) 15. p:pre().
p A.pre

p.kind = kind(a)  [[p.rel]] rho A.ds dec_lookup(A.da;kind(a)) de e s value(a) niltrace() 16. ef:eff().
ef A.eff

ef.kind = kind(a)

x'.ef.smt.lbl = [[ef.smt.term]] 1of(e) s value(a) niltrace() [[ef.smt.typ]] rho 17. fr:frame(). fr A.frame  (kind(a) fr.acts)  x'.fr.var = s.fr.var [[fr.typ]] rho 18. rel_mng_2(r; rho; A.ds; dec_lookup(A.da;kind(a)); de; e; s; x'; value(a); tr) 19. r@0: rel() 20. as: (Label Term) List 21. 1of(unzip(as)) = rel_primed_vars(r) 22. i: . i < ||as||  2of(as[i]) ( x.smts_eff(action_effect(kind(a);A.eff;A.frame);x))(1of(as[i])) 23. r@0 = rel_subst2(as;r) 24. value(a) [[dec_lookup(A.da;kind(a))]] rho 25. subst_mentions_trace(as) e:eff(). e A.eff & mentions_trace(e.smt.term) |