Nuprl - Proof: paren balance2 3

(5steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc

1. T: Type
2. s': (T+T) List
3. t: T
4. i:T. (inr(i) s') (inl(i) s')
5. paren(T;s')
6. i: T
7. (inr(i) [inl(t)] @ s' @ [inr(t)])

(inl(i) [inl(t)] @ s' @ [inr(t)])

By: All (i. (RWW Thm* x:T, l1,l2:T List. (x l1 @ l2) (x l1) (x l2) i) THEN (RWO Thm* a,x:T. (x [a]) x = a i)) THEN Obvious

Generated subgoals:

None

About:

(5steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc