Nuprl - Pf term mng tappend 2

(3steps) PrintForm Definitions mb automata 2 Sections GenAutomata Doc

1. u: Term
2. u1: TermType{i'}
3. w: u:{v:Term| u1(v) }d:Decl{i}, tr:trace_env(d), a:(d), e,s,v:Top. affects_trace(tr.proj;kind(a);u) ([[u]] e s v tappend(tr;a) ~ [[u]] e s v tr)
4. y1: {v:Term| u1(v) }
5. y2: {v:Term| u1(v) }

d:Decl{i}, tr:trace_env(d), a:(d), e,s,v:Top. (affects_trace(tr.proj;kind(a);y1) affects_trace(tr.proj;kind(a);y2)) (([[y1]] e s v tappend(tr;a)([[y2]] e s v tappend(tr;a))) ~ ([[y1]] e s v tr([[y2]] e s v tr)))

By: UnivCD THEN Analyze THEN BackThruSomeHyp THEN ParallelOp -1 THEN RW assert_pushdownC 0 THEN SimpConcl

Generated subgoals:

None

About:

(3steps) PrintForm Definitions mb automata 2 Sections GenAutomata Doc