At:
trace consistent wp2 rel
1
1
1
1.
A: ioa{i:l}()
2.
rho: Decl
3.
r: rel()
4.
R: Label
Label

5.
k: Label
6.
ioa_mentions_trace(A)
7.
trace_consistent_rel(rho;A.da;R;r)
8.
r@0: rel()
9.
as: (Label
Term) List
10.
1of(unzip(as)) = rel_primed_vars(r)
11.
i:
. i < ||as|| 
2of(as[i])
(
x.smts_eff(action_effect(k;A.eff;A.frame);x))(1of(as[i]))
12.
r@0 = rel_subst2(as;r)
subst_mentions_trace(as)
By:
Reduce -2
THEN
BackThruLemma'
Thm*
A:ioa{i:l}(), as:(Label
Term) List, k:Label.
ioa_mentions_trace(A) 
(
i:
. i < ||as|| 
2of(as[i])
smts_eff(action_effect(k;A.eff;A.frame);1of(as[i]))) 
subst_mentions_trace(as)
Generated subgoals:
None
About: