Nuprl - Pf tc ioa lemma 2 1

(30steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc

1. as: (LabelTerm) List
2. u: LabelTerm
3. v: (LabelTerm) List
4. A:ioa{i:l}(), de:sig(), x:Label, t:SimpleType, k:Label. single_valued_decls(A.ds) tc_ioa(A;de) (i:. i < ||v|| 2of(v[i]) smts_eff(action_effect(k;A.eff;A.frame);1of(v[i]))) mk_dec(x, t) A.ds t term_types(A.ds;dec_lookup(A.da;k);de;apply_alist(v;x;x))
5. A: ioa{i:l}()
6. de: sig()
7. x: Label
8. t: SimpleType
9. k: Label
10. single_valued_decls(A.ds)
11. tc_ioa(A;de)
12. i:. i < ||[u / v]|| 2of([u / v][i]) smts_eff(action_effect(k;A.eff;A.frame);1of([u / v][i]))
13. mk_dec(x, t) A.ds

t term_types(A.ds;dec_lookup(A.da;k);de;apply_alist([u / v];x;x))

By: Subst (apply_alist([u / v];x;x) ~ if 1of(u) = x 2of(u) else apply_alist(v;x;x) fi) 0

Generated subgoals:

1 apply_alist([u / v];x;x) ~ if 1of(u) = x 2of(u) else apply_alist(v;x;x) fi

2 t term_types(A.ds;dec_lookup(A.da;k);de;if 1of(u) = x 2of(u) else apply_alist(v;x;x) fi)

About:

(30steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc

1	`apply_alist([u / v];x;x) ~ if 1of(u) = x 2of(u) else apply_alist(v;x;x) fi`
2	`t term_types(A.ds;dec_lookup(A.da;k);de;if 1of(u) = x 2of(u) else apply_alist(v;x;x) fi)`