Nuprl - Pf covers_pred_lemma2 1 2 1 1 1 1 2 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. (x rel_vars(r)) covers_var(A;x)
7. x:Label. t:Term. (x rel_primed_vars(r)) t smts_eff(action_effect(a;A.eff;A.frame);x)
8. f:(LabelTerm). x:Label. (x rel_primed_vars(r)) f(x) smts_eff(action_effect(a;A.eff;A.frame);x)

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])))

By: ExRepD THEN InstConcl [zip(rel_primed_vars(r);map(f;rel_primed_vars(r)))]

Generated subgoals:

1 8. f: LabelTerm
9. x:Label. (x rel_primed_vars(r)) f(x) smts_eff(action_effect(a;A.eff;A.frame);x)
1of(unzip(zip(rel_primed_vars(r);map(f;rel_primed_vars(r))))) = rel_primed_vars(r)

2 8. f: LabelTerm
9. x:Label. (x rel_primed_vars(r)) f(x) smts_eff(action_effect(a;A.eff;A.frame);x)
10. i:
11. i < ||zip(rel_primed_vars(r);map(f;rel_primed_vars(r)))||
2of(zip(rel_primed_vars(r);map(f;rel_primed_vars(r)))[i]) smts_eff(action_effect(a;A.eff;...);...)

About:

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

1	8. `f:` `LabelTerm` 9. `x:Label. (x rel_primed_vars(r)) f(x) smts_eff(action_effect(a;A.eff;A.frame);x)` `1of(unzip(zip(rel_primed_vars(r);map(f;rel_primed_vars(r))))) = rel_primed_vars(r)`
2	8. `f:` `LabelTerm` 9. `x:Label. (x rel_primed_vars(r)) f(x) smts_eff(action_effect(a;A.eff;A.frame);x)` 10. `i:` 11. `i < \|\|zip(rel_primed_vars(r);map(f;rel_primed_vars(r)))\|\|` `2of(zip(rel_primed_vars(r);map(f;rel_primed_vars(r)))[i]) smts_eff(action_effect(a;A.eff;...);...)`