blob: c01d3f2350c371c2666892d4da3074b38d33a7e2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
% COMMAND-LINE: --uf-ho --full-saturate-quant --ho-elim
% EXPECT: % SZS status Theorem for SYO362^5
thf(cK,type,(
cK: ( $i > $o ) > $i > $o )).
thf(cTHM631A_pme,conjecture,
( ! [X: $i > $o,Y: $i > $o] :
( ( cK
@ ^ [Xz: $i] :
( ( X @ Xz )
| ( Y @ Xz ) ) )
= ( ^ [Xw: $i] :
( ( cK @ X @ Xw )
| ( cK @ Y @ Xw ) ) ) )
=> ! [X: $i > $o,Y: $i > $o] :
( ! [Xx: $i] :
( ( X @ Xx )
=> ( Y @ Xx ) )
=> ! [Xx: $i] :
( ( cK @ X @ Xx )
=> ( cK @ Y @ Xx ) ) ) )).
|
