A:ioa{i:l}(), Q:Fmla, de:sig(), a:Label. tc_ioa(A;de) tc_pred(Q;A.ds;dec_lookup(A.da;a);de) single_valued_decls(A.ds) tc_pred(wp2(A;a;Q);A.ds;dec_lookup(A.da;a);de)

1	1. A: ioa{i:l}() 2. Q: Fmla 3. de: sig() 4. a: Label 5. tc_ioa(A;de) 6. tc_pred(Q;A.ds;dec_lookup(A.da;a);de) 7. single_valued_decls(A.ds) tc_pred((rQ.col_subst2(x.smts_eff(action_effect(a;A.eff;A.frame);x);r));A.ds;dec_lookup(A.da;a);de)

About: