Nuprl - Pf covers_pred_lemma2 1 2 1 1 1 1 1 2 1

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

At: covers pred lemma2 1 2 1 1 1 1 1 2 1

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)
7. x: Label
8. (x rel_primed_vars(r))

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

By: (Assert covers_var(A;x)) THENL [SmAuto;(Unfold `covers_var` -1) THEN ExRepD]

Generated subgoals:

1 covers_var(A;x)

2 9. fr: frame()
10. fr < fr A.frame | fr.var = x >
11. a:Label. (a fr.acts) (ef:eff(). ef < ef A.eff | ef.kind = a & ef.smt.lbl = x > )
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	`covers_var(A;x)`
2	9. `fr:` `frame()` 10. `fr < fr A.frame \| fr.var = x >` 11. `a:Label. (a fr.acts) (ef:eff(). ef < ef A.eff \| ef.kind = a & ef.smt.lbl = x > )` `t:Term. (x rel_primed_vars(r)) t smts_eff(action_effect(a;A.eff;A.frame);x)`