Nuprl - Pf wp2 addprime 1 2

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

1. A: ioa{i:l}()
2. a: Label
3. P: Fmla
4. x: rel()
5. r:rel(). r P & (as:(LabelTerm) List. 1of(unzip(as)) = rel_vars(r) & (i:. i < ||as|| 2of(as[i]) (x.smts_eff(action_effect(a;A.eff;A.frame);x))(1of(as[i]))) & x = rel_subst(as;r))

r:rel(). (r@0:rel(). r@0 P & r = (r@0)') & (as:(LabelTerm) List. 1of(unzip(as)) = rel_primed_vars(r) & (i:. i < ||as|| 2of(as[i]) smts_eff(action_effect(a;A.eff;A.frame);1of(as[i]))) & x = rel_subst2(as;r))

By: (ExRepD THEN (InstConcl [(r)'])) THENA (Auto THEN (Try (Fold `pred` 0))) THEN Analyze 0 THEN Try ((AutoInstConcl []) THEN (Try (Fold `pred` 0))) THEN InstConcl [as] THEN All Reduce THEN Analyze 0 THEN Try ((Analyze 0) THEN (Try Trivial))

Generated subgoals:

1 5. r: rel()
6. r P
7. as: (LabelTerm) List
8. 1of(unzip(as)) = rel_vars(r)
9. i:. i < ||as|| 2of(as[i]) smts_eff(action_effect(a;A.eff;A.frame);1of(as[i]))
10. x = rel_subst(as;r)
1of(unzip(as)) = rel_primed_vars((r)')

2 5. r: rel()
6. r P
7. as: (LabelTerm) List
8. 1of(unzip(as)) = rel_vars(r)
9. i:. i < ||as|| 2of(as[i]) smts_eff(action_effect(a;A.eff;A.frame);1of(as[i]))
10. x = rel_subst(as;r)
x = rel_subst2(as;(r)')

About:

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

1	5. `r:` `rel()` 6. `r P` 7. `as:` `(LabelTerm) List` 8. `1of(unzip(as)) = rel_vars(r)` 9. `i:. i < \|\|as\|\| 2of(as[i]) smts_eff(action_effect(a;A.eff;A.frame);1of(as[i]))` 10. `x = rel_subst(as;r)` `1of(unzip(as)) = rel_primed_vars((r)')`
2	5. `r:` `rel()` 6. `r P` 7. `as:` `(LabelTerm) List` 8. `1of(unzip(as)) = rel_vars(r)` 9. `i:. i < \|\|as\|\| 2of(as[i]) smts_eff(action_effect(a;A.eff;A.frame);1of(as[i]))` 10. `x = rel_subst(as;r)` `x = rel_subst2(as;(r)')`