At:
paren interval
2
1
1
1
1.
T: Type
2.
s1: (T+T) List
3.
s2: (T+T) List
4.
no_repeats(T+T;s1)
(
s1@0,s2,s3:(T+T) List, x:T. s1 = (s1@0 @ [inl(x)] @ s2 @ [inr(x)] @ s3) paren(T;s2))
5.
no_repeats(T+T;s2)
(s1,s2@0,s3:(T+T) List, x:T. s2 = (s1 @ [inl(x)] @ s2@0 @ [inr(x)] @ s3) paren(T;s2@0))
6.
paren(T;s1)
7.
paren(T;s2)
8.
l_disjoint(T+T;s1;s2) & no_repeats(T+T;s1) & no_repeats(T+T;s2)
9.
s1@0: (T+T) List
10.
s2@0: (T+T) List
11.
s3: (T+T) List
12.
x: T
13.
(s1 @ s2) = (s1@0 @ [inl(x)] @ s2@0 @ [inr(x)] @ s3)
14.
e: (T+T) List
15.
s1 = (s1@0 @ e)
16.
([inl(x)] @ s2@0 @ [inr(x)] @ s3) = (e @ s2)
17.
e1: (T+T) List
18.
[inl(x)] = (e @ e1)
19.
s2 = (e1 @ s2@0 @ [inr(x)] @ s3)
20.
e = nil
21.
e1 = [inl(x)]
paren(T;s2@0)
By:
InstHyp [nil;s2@0;s3;x] 5
THEN
SubstFor s2 0
THEN
SubstFor e1 0
THEN
Reduce 0
Generated subgoals:
None
About:
