At:
paren interval
3
1
2
1
2
1
2
1.
T: Type
2.
s: (T+T) List
3.
t: T
4.
no_repeats(T+T;s)
(
s1,s2,s3:(T+T) List, x:T. s = (s1 @ [inl(x) / (s2 @ [inr(x) / s3])]) paren(T;s2))
5.
paren(T;s)
6.
l_disjoint(T+T;[inl(t)];s @ [inr(t)])
7.
no_repeats(T+T;[inl(t)])
8.
l_disjoint(T+T;s;[inr(t)])
9.
no_repeats(T+T;s)
10.
no_repeats(T+T;[inr(t)])
11.
u: T+T
12.
v: (T+T) List
13.
s2: (T+T) List
14.
s3: (T+T) List
15.
x: T
16.
inl(t) = u
17.
(s @ [inr(t)]) = (v @ [inl(x) / (s2 @ [inr(x) / s3])])
18.
u1: T+T
19.
v1: (T+T) List
20.
s = (v @ [inl(x) / v1])
21.
(s2 @ [inr(x) / s3]) = (v1 @ [inr(t)])
22.
e: (T+T) List
23.
s2 = (v1 @ e)
24.
[inr(t)] = (e @ [inr(x) / s3])
25.
[inr(x) / s3] = nil
26.
e = [inr(t)]
paren(T;s2)
By:
ObviousContradiction [-2]
Generated subgoals:
None
About:
