At:
tc wp
1
1
1
2
1
1.
A: ioa{i:l}()
2.
Q: Fmla
3.
de: sig()
4.
a: Label
5.
tc_ioa(A;de)
6.
single_valued_decls(A.ds)
7.
tc_pred(Q;A.ds;dec_lookup(A.da;a);de)
8.
r: rel()
9.
r 
(
rQ.smts_eff_rel(action_effect(a;A.eff;A.frame);r))
10.
r1: rel()
11.
r1 Q
12.
as: (Label
Term) List
13.
1of(unzip(as)) = rel_vars(r1)
14.
i:
. i < ||as|| 
2of(as[i]) (
x.smts_eff(action_effect(a;A.eff;A.frame);x))(1of(as[i]))
15.
r = rel_subst(as;r1)
16.
x: Label
17.
(x rel_vars(r1))
18.
t: SimpleType
19.
mk_dec(x, t) A.ds
20.
i:
21.
i < ||as||
2of(as[i]) smts_eff(action_effect(a;A.eff;A.frame);1of(as[i]))
By:
All Reduce
THEN
BackThruSomeHyp
Generated subgoals:
None
About:
