Nuprl - Pf sm_trans_wf 1

(2steps) PrintForm Definitions mb state machine Sections GenAutomata Doc

At: sm trans wf 1

1. M: da:Declds:Decl({ds}Prop)({ds}(da){ds}Prop)

M.trans {M.ds}(M.da){M.ds}Prop

By: RepeatFor 3 (Analyze -1) THEN Reduce 0 THEN Trivial

Generated subgoals:

None

About:

(2steps) PrintForm Definitions mb state machine Sections GenAutomata Doc