At:
trace consistent wp
1
2
2
1.
A: ioa{i:l}()
2.
Q: Fmla
3.
rho: Decl
4.
R: Label
Label
5.
k: Label
6.
ioa_mentions_trace(A)
7.
trace_consistent_pred(rho;A.da;R;Q)
8.
r:rel(). r 
Q 
trace_consistent_pred(rho;A.da;R;wp_rel(A;k;r))
9.
r: rel()
wp(A;k;Q) Collection(rel())
By:
Fold `pred` 0
Generated subgoals:
None
About:
