(40steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc

At: rel effect lemma 1 1 2 2 1 1
1. A: ioa{i:l}()
2. rho: Decl
3. de: sig()
4. act: ([[A.da]] rho)
5. r: rel()
6. r0: rel()
7. tc_ioa(A;de)
8. as: (LabelTerm) List
9. 1of(unzip(as)) = rel_vars(r0)
10. i:. i < ||as|| 2of(as[i]) smts_eff(action_effect(kind(act);A.eff;A.frame);1of(as[i]))
11. r = rel_subst(as;r0)
12. rel_eq(rel_unprime(r);rel_unprime(r0))
13. 2of(unzip(as)) = map(x.x;1of(unzip(as)))
14. i:
15. i < ||as||
16. 2of(as[i]) = 1of(as[i])
17. s:smt(). (e:eff(). e A.eff & e.kind = kind(act) & s = e.smt) (f:frame(). f A.frame & kind(act) f.acts & s = mk_smt(f.var, f.var, f.typ)) & s.lbl = 1of(as[i]) & 2of(as[i]) = s.term

t:dec(). t A.da & t.lbl = kind(act)
By:
ExRepD
THEN
Analyze -3
THEN
ExRepD
Generated subgoals:

117. s: smt()
18. e: eff()
19. e A.eff
20. e.kind = kind(act)
21. s = e.smt
22. s.lbl = 1of(as[i])
23. 2of(as[i]) = s.term
t:dec(). t A.da & t.lbl = kind(act)
217. s: smt()
18. f: frame()
19. f A.frame
20. kind(act) f.acts
21. s = mk_smt(f.var, f.var, f.typ)
22. s.lbl = 1of(as[i])
23. 2of(as[i]) = s.term
t:dec(). t A.da & t.lbl = kind(act)

About:
productlistassertless_thanlambdaequalimpliesandorallexists

(40steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc