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