At:
trace consistent wp
1
2
1
1
1
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()
10.
r@0: rel()
11.
r@0 Q
12.
r wp_rel(A;k;r@0)
13.
trace_consistent_pred(rho;A.da;R;wp_rel(A;k;r@0))
trace_consistent_rel(rho;A.da;R;r)
By:
Unfold `trace_consistent_pred` -1
THEN
Unfold `col_all` -1
THEN
BackThru -1
Generated subgoals:
None
About:
