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

At: paren order1 3 1 2 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. [inl(t)] = (s1 @ e)
12. ([inl(i)] @ s2) = (e @ s @ [inr(t)])
13. e = nil
14. s1 = [inl(t)]
15. ([inl(i)] @ s2) = (s @ [inr(t)])
16. e1: (T+T) List
17. s = ([inl(i)] @ e1)
18. s2 = (e1 @ [inr(t)])
(inr(i) s2)
By:
InstHyp [i;nil;e1] 4
THEN
All Reduce
THEN
SubstFor s2 0
Generated subgoal:

14. 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. [inl(t)] = (s1 @ e)
12. [inl(i) / s2] = (e @ s @ [inr(t)])
13. e = nil
14. s1 = [inl(t)]
15. [inl(i) / s2] = (s @ [inr(t)])
16. e1: (T+T) List
17. s = [inl(i) / e1]
18. s2 = (e1 @ [inr(t)])
19. (inr(i) e1)
(inr(i) e1 @ [inr(t)])		1 step

About:
listconsnilunioninlinruniverseequalimpliesall

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