At:
trace consistent wp rel
1
1
1
1.
A: ioa{i:l}()
2.
rho: Decl
3.
r: rel()
4.
R: LabelLabel
5.
k: Label
6.
ioa_mentions_trace(A)
7.
trace_consistent_rel(rho;A.da;R;r)
8.
r@0: rel()
9.
as: (LabelTerm) List
10.
1of(unzip(as)) = rel_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_subst(as;r)
subst_mentions_trace(as)
By:
Reduce -2
THEN
BackThruLemma'
Thm* A:ioa{i:l}(), as:(LabelTerm) 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: