Nuprl - Pf covers_pred_lemma2 1 2 1 1 1 1 1 2 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 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))
9. fr: frame()
10. fr A.frame
11. fr.var = x
12. a:Label. (a fr.acts) (ef:eff(). ef A.eff & ef.kind = a & ef.smt.lbl = x)

t:Term. (x rel_primed_vars(r)) (s:smt(). s action_effect(a;A.eff;A.frame) & s.lbl = x & t = s.term)

By: Assert (s:smt(). s < s action_effect(a;A.eff;A.frame) | s.lbl = x > )

Generated subgoals:

1 s:smt(). s < s action_effect(a;A.eff;A.frame) | s.lbl = x >

2 13. s:smt(). s < s action_effect(a;A.eff;A.frame) | s.lbl = x >
t:Term. (x rel_primed_vars(r)) (s:smt(). s action_effect(a;A.eff;A.frame) & s.lbl = x & t = s.term)

About:

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

1	`s:smt(). s < s action_effect(a;A.eff;A.frame) \| s.lbl = x >`
2	13. `s:smt(). s < s action_effect(a;A.eff;A.frame) \| s.lbl = x >` `t:Term. (x rel_primed_vars(r)) (s:smt(). s action_effect(a;A.eff;A.frame) & s.lbl = x & t = s.term)`