1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
library Hofs
logic HasCASL
spec S =
type s;
op f : s ->? s
op g : s -> s
op h : ?s -> s
op i : ?s ->? s
op h1 : (s -> s) ->? s
op h2 : (s ->? s) ->? s
op h3 : (?s ->? s) ->? s
op h4 : (?s -> s) ->? s
op h5 : ?(?s -> s) ->? s
op h6 : (s -> s) -> s
op h7 : (s ->? s) -> s
op h8 : (?s ->? s) -> s
op h9 : (?s -> s) -> s
op h10 : ?(?s -> s) -> s
. g = f
. f = g
. g = h
. h = g
. f = h
. h = f
. f = i
. i = f
. g = i
. i = g
. h = i
. i = h
. h1 = h2
. h1 = h3
%%. h1 = h4
%%. h1 = h5
. h2 = h3
%%. h2 = h4
%%. h2 = h5
%%. h3 = h4
%%. h3 = h5
%%. h4 = h5
. h6 = h2
. h6 = h3
%%. h6 = h4
%%. h6 = h5
. h7 = h2
. h7 = h3
%%. h7 = h4
%%. h7 = h5
. h8 = h2
. h8 = h3
%%. h8 = h4
%%. h8 = h5
%%. h9 = h2
%%. h9 = h3
%%. h9 = h4
%%. h9 = h5
%%. h10 = h2
%%. h10 = h3
%%. h10 = h4
%%. h10 = h5