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

At: paren order1 3 2 2
1. T: Type
2. s: (T+T) List
3. t: T
4. i:T, s1,s2:(T+T) List. s = (s1 @ [inl(i)] @ s2) (inr(i) s2)
5. paren(T;s)
6. i: T
7. s1: (T+T) List
8. s2: (T+T) List
9. ([inl(t)] @ s @ [inr(t)]) = (s1 @ [inl(i)] @ s2)
10. e: (T+T) List
11. s1 = ([inl(t)] @ e)
12. (s @ [inr(t)]) = (e @ [inl(i)] @ s2)
13. e1: (T+T) List
14. e = (s @ e1)
15. [inr(t)] = (e1 @ [inl(i)] @ s2)
(inr(i) s2)
By: SingletonAppendD -1
Generated subgoals:

116. e1 = nil
17. ([inl(i)] @ s2) = [inr(t)]
(inr(i) s2)		1 step
 
216. ([inl(i)] @ s2) = nil
17. e1 = [inr(t)]
(inr(i) s2)		1 step

About:
listconsnilunioninlinruniverseequalimpliesall

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