Nuprl - Pf covers_pred_lemma2 1 2 1 1 2

(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. rel_mentions(r;x) covers_var(A;x)
7. 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])))

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

By: ExRepD THEN Reduce 0 THEN InstConcl [rel_subst2(as;r);as] THEN Try BackThruSomeHyp

Generated subgoals:

None

About:

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