Nuprl - Pf tc ioa lemma 1

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

1. as: (LabelTerm) List

A:ioa{i:l}(), de:sig(), x:Label, t:SimpleType, k:Label. single_valued_decls(A.ds) tc_ioa(A;de) (i:. i < ||nil|| 2of(nil[i]) smts_eff(action_effect(k;A.eff;A.frame);1of(nil[i]))) mk_dec(x, t) A.ds t term_types(A.ds;dec_lookup(A.da;k);de;apply_alist(nil;x;x))

By: Unfold `apply_alist` 0 THEN Unfold `find` 0 THEN Reduce 0

Generated subgoal:

1 A:ioa{i:l}(), de:sig(), x:Label, t:SimpleType, k:Label. single_valued_decls(A.ds) tc_ioa(A;de) (i:. i < 0 2of(nil[i]) smts_eff(action_effect(k;A.eff;A.frame);1of(nil[i]))) mk_dec(x, t) A.ds t dec_lookup(A.ds;x)

About:

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