Nuprl - Pf covers_pred_lemma2 1 2 1 1 1 1 1

(36steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc

1. r: rel()
2. I: Collection(rel())
3. A: ioa{i:l}()
4. a: Label
5. r I
6. x:Label. (x rel_vars(r)) covers_var(A;x)

x:Label. t:Term. (x rel_primed_vars(r)) t smts_eff(action_effect(a;A.eff;A.frame);x)

By: Analyze 0 THEN Assert ((x rel_primed_vars(r)) (x rel_primed_vars(r)))

Generated subgoals:

1 7. x: Label
(x rel_primed_vars(r)) (x rel_primed_vars(r))

2 7. x: Label
8. (x rel_primed_vars(r)) (x rel_primed_vars(r))
t:Term. (x rel_primed_vars(r)) t smts_eff(action_effect(a;A.eff;A.frame);x)

About:

(36steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc

1	7. `x:` `Label` `(x rel_primed_vars(r)) (x rel_primed_vars(r))`
2	7. `x:` `Label` 8. `(x rel_primed_vars(r)) (x rel_primed_vars(r))` `t:Term. (x rel_primed_vars(r)) t smts_eff(action_effect(a;A.eff;A.frame);x)`