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
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
|
Minlog loaded successfully
> ; ok, type variable real added
; ok, type variable open added
> ; ok, variable x: real added
; ok, variable y: real added
> ; ok, variable f: real=>real added
> ; ok, variable U: open added
; ok, variable V: open added
; ok, variable W: open added
> ; ok, predicate constant ee: (arity real open boole) added
> > > ; ?_1: all f.
; (all x,V.f x in V -> ex U.x in U & all y.y in U -> f y in V) ->
; all x,W.f(f x)in W -> ex U.x in U & all y.y in U -> f(f y)in W
> ; ok, we now have the new goal
; ?_2: ex U.x in U & all y.y in U -> f(f y)in W from
; f fCont:all x,V.f x in V -> ex U.x in U & all y.y in U -> f y in V
; x W Hyp1:f(f x)in W
> ; ok, ?_2 can be obtained from
; ?_4: ex U.x in U & all y.y in U -> f(f y)in W from
; f fCont:all x,V.f x in V -> ex U.x in U & all y.y in U -> f y in V
; x W Hyp1:f(f x)in W
; Hyp2:f(f x)in W -> ex U.f x in U & all y.y in U -> f y in W
> ; ok, ?_4 can be obtained from
; ?_6: ex U.x in U & all y.y in U -> f(f y)in W from
; f fCont:all x,V.f x in V -> ex U.x in U & all y.y in U -> f y in V
; x W Hyp1:f(f x)in W
; Hyp2:f(f x)in W -> ex U.f x in U & all y.y in U -> f y in W
; W-ExHyp:ex U.f x in U & all y.y in U -> f y in W
> ; ok, we now have the new goal
; ?_7: ex U.x in U & all y.y in U -> f(f y)in W from
; f fCont:all x,V.f x in V -> ex U.x in U & all y.y in U -> f y in V
; x W W-ExHyp:ex U.f x in U & all y.y in U -> f y in W
> ; ok, we now have the new goal
; ?_10: ex U.x in U & all y.y in U -> f(f y)in W from
; f fCont:all x,V.f x in V -> ex U.x in U & all y.y in U -> f y in V
; x W V VHyp:f x in V & all y.y in V -> f y in W
> ; ok, ?_10 can be obtained from
; ?_12: ex U.x in U & all y.y in U -> f(f y)in W from
; f fCont:all x,V.f x in V -> ex U.x in U & all y.y in U -> f y in V
; x W V VHyp:f x in V & all y.y in V -> f y in W
; Hyp3:f x in V -> ex U.x in U & all y.y in U -> f y in V
> ; ok, ?_12 can be obtained from
; ?_13: (ex U.x in U & all y.y in U -> f y in V) ->
; ex U.x in U & all y.y in U -> f(f y)in W from
; f fCont:all x,V.f x in V -> ex U.x in U & all y.y in U -> f y in V
; x W V VHyp:f x in V & all y.y in V -> f y in W
; Hyp3:f x in V -> ex U.x in U & all y.y in U -> f y in V
; ?_14: ex U.x in U & all y.y in U -> f y in V from
; f fCont:all x,V.f x in V -> ex U.x in U & all y.y in U -> f y in V
; x W V VHyp:f x in V & all y.y in V -> f y in W
; Hyp3:f x in V -> ex U.x in U & all y.y in U -> f y in V
> ; ok, ?_14 can be obtained from
; ?_15: f x in V from
; f fCont:all x,V.f x in V -> ex U.x in U & all y.y in U -> f y in V
; x W V VHyp:f x in V & all y.y in V -> f y in W
; Hyp3:f x in V -> ex U.x in U & all y.y in U -> f y in V
> ; ok, ?_15 is proved. The active goal now is
; ?_13: (ex U.x in U & all y.y in U -> f y in V) ->
; ex U.x in U & all y.y in U -> f(f y)in W from
; f fCont:all x,V.f x in V -> ex U.x in U & all y.y in U -> f y in V
; x W V VHyp:f x in V & all y.y in V -> f y in W
; Hyp3:f x in V -> ex U.x in U & all y.y in U -> f y in V
> ; ok, we now have the new goal
; ?_16: ex U.x in U & all y.y in U -> f(f y)in W from
; f fCont:all x,V.f x in V -> ex U.x in U & all y.y in U -> f y in V
; x W V VHyp:f x in V & all y.y in V -> f y in W
; Hyp3:f x in V -> ex U.x in U & all y.y in U -> f y in V
; V-ExHyp:ex U.x in U & all y.y in U -> f y in V
> ; ok, we now have the new goal
; ?_19: ex U.x in U & all y.y in U -> f(f y)in W from
; f fCont:all x,V.f x in V -> ex U.x in U & all y.y in U -> f y in V
; x W V VHyp:f x in V & all y.y in V -> f y in W
; Hyp3:f x in V -> ex U.x in U & all y.y in U -> f y in V
; U UHyp:x in U & all y.y in U -> f y in V
> ; ok, ?_19 can be obtained from
; ?_20: x in U & all y.y in U -> f(f y)in W from
; f fCont:all x,V.f x in V -> ex U.x in U & all y.y in U -> f y in V
; x W V VHyp:f x in V & all y.y in V -> f y in W
; Hyp3:f x in V -> ex U.x in U & all y.y in U -> f y in V
; U UHyp:x in U & all y.y in U -> f y in V
> ; ok, we now have the new goals
; ?_22: all y.y in U -> f(f y)in W from
; f fCont:all x,V.f x in V -> ex U.x in U & all y.y in U -> f y in V
; x W V VHyp:f x in V & all y.y in V -> f y in W
; Hyp3:f x in V -> ex U.x in U & all y.y in U -> f y in V
; U UHyp:x in U & all y.y in U -> f y in V
; ?_21: x in U from
; f fCont:all x,V.f x in V -> ex U.x in U & all y.y in U -> f y in V
; x W V VHyp:f x in V & all y.y in V -> f y in W
; Hyp3:f x in V -> ex U.x in U & all y.y in U -> f y in V
; U UHyp:x in U & all y.y in U -> f y in V
> ; ok, ?_21 is proved. The active goal now is
; ?_22: all y.y in U -> f(f y)in W from
; f fCont:all x,V.f x in V -> ex U.x in U & all y.y in U -> f y in V
; x W V VHyp:f x in V & all y.y in V -> f y in W
; Hyp3:f x in V -> ex U.x in U & all y.y in U -> f y in V
; U UHyp:x in U & all y.y in U -> f y in V
> ; ok, we now have the new goal
; ?_23: f(f y)in W from
; f fCont:all x,V.f x in V -> ex U.x in U & all y.y in U -> f y in V
; x W V VHyp:f x in V & all y.y in V -> f y in W
; Hyp3:f x in V -> ex U.x in U & all y.y in U -> f y in V
; U UHyp:x in U & all y.y in U -> f y in V
; y yHyp:y in U
> ; ok, ?_23 can be obtained from
; ?_24: f y in V from
; f fCont:all x,V.f x in V -> ex U.x in U & all y.y in U -> f y in V
; x W V VHyp:f x in V & all y.y in V -> f y in W
; Hyp3:f x in V -> ex U.x in U & all y.y in U -> f y in V
; U UHyp:x in U & all y.y in U -> f y in V
; y yHyp:y in U
> ; ok, ?_24 can be obtained from
; ?_25: y in U from
; f fCont:all x,V.f x in V -> ex U.x in U & all y.y in U -> f y in V
; x W V VHyp:f x in V & all y.y in V -> f y in W
; Hyp3:f x in V -> ex U.x in U & all y.y in U -> f y in V
; U UHyp:x in U & all y.y in U -> f y in V
; y yHyp:y in U
> ; ok, ?_25 is proved. Proof finished.
> ; ok, ContLemma has been added as a new theorem.
; ok, program constant cContLemma: (real=>real)=>(real=>open=>open)=>real=>open=>open
; of t-degree 1 and arity 0 added
> ; ok, variable M: real=>open=>open added
> [f0,M1,x2,U3]M1 x2(M1(f0 x2)U3)
> ; ?_1: all f.
; (all x,V.f x in V -> excl U.x in U & all y.y in U -> f y in V) ->
; all x,W.f(f x)in W -> excl U.x in U & all y.y in U -> f(f y)in W
> ; ok, ?_1 is proved by minimal quantifier logic. Proof finished.
>
|
