At: n0n1 irregular 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 2
1. S: ActionSet(
)
2. s: S.car
3. q: S.car
4. n: 
5. f: S.car
n
6. g: nS.car
7. g o f = Id
8. f o g = Id
9. 
k:. (S:n0n1(k)
s) = q
10. i: (n+1)
11. j: (n+1)
12. i < j
13. f((S:([1]
i)s)) = f((S:([1]j)s))
14. (S:([1]i)s) = (S:([1]j)s)
15. (S:([0]j) @ ([1]i)s) = (S:([0]j) @ ([1]j)s)
(S:([0]j) @ ([1]i)s) = q
By: RWH (HypC 15) 0
Generated subgoal:| 1 | (S:([0]j) @ ([1]j)s) = q |
About:
