:: QUIN_1 semantic presentation
begin
definition
let
a
,
b
,
c
be ( (
complex
) (
complex
)
number
) ;
func
delta
(
a
,
b
,
c
)
->
( ( ) ( )
set
)
equals
:: QUIN_1:def 1
(
b
: ( (
ext-real
) (
ext-real
)
set
)
^2
)
: ( ( ) ( )
set
)
-
(
(
4 : ( ( ) ( non
zero
natural
complex
ext-real
positive
real
V16
()
V17
()
V18
()
V19
()
V20
()
V21
() )
M3
(
REAL
: ( ( ) (
V16
()
V17
()
V18
()
V22
() )
set
) ,
NAT
: ( ( ) (
V16
()
V17
()
V18
()
V19
()
V20
()
V21
()
V22
() )
M2
(
K6
(
REAL
: ( ( ) (
V16
()
V17
()
V18
()
V22
() )
set
) ) : ( ( ) ( )
set
) )) ))
*
a
: ( (
ext-real
) (
ext-real
)
set
)
)
: ( ( ) ( )
set
)
*
c
: ( ( ) ( )
set
)
)
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ;
end;
registration
let
a
,
b
,
c
be ( (
complex
) (
complex
)
number
) ;
cluster
delta
(
a
: ( (
complex
) (
complex
)
set
) ,
b
: ( (
complex
) (
complex
)
set
) ,
c
: ( (
complex
) (
complex
)
set
) ) : ( ( ) ( )
set
)
->
complex
;
end;
registration
let
a
,
b
,
c
be ( (
real
) (
complex
ext-real
real
)
number
) ;
cluster
delta
(
a
: ( (
real
) (
complex
ext-real
real
)
set
) ,
b
: ( (
real
) (
complex
ext-real
real
)
set
) ,
c
: ( (
real
) (
complex
ext-real
real
)
set
) ) : ( ( ) (
complex
)
set
)
->
real
;
end;
definition
let
a
,
b
,
c
be ( ( ) (
complex
ext-real
real
)
Real
) ;
:: original:
delta
redefine
func
delta
(
a
,
b
,
c
)
->
( ( ) (
complex
ext-real
real
)
Real
) ;
end;
theorem
:: QUIN_1:1
for
a
,
b
,
c
,
x
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
natural
complex
ext-real
real
V16
()
V17
()
V18
()
V19
()
V20
()
V21
() )
M3
(
REAL
: ( ( ) (
V16
()
V17
()
V18
()
V22
() )
set
) ,
NAT
: ( ( ) (
V16
()
V17
()
V18
()
V19
()
V20
()
V21
()
V22
() )
M2
(
K6
(
REAL
: ( ( ) (
V16
()
V17
()
V18
()
V22
() )
set
) ) : ( ( ) ( )
set
) )) )) holds
(
(
a
: ( (
complex
) (
complex
)
number
)
*
(
x
: ( (
complex
) (
complex
)
number
)
^2
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
+
(
b
: ( (
complex
) (
complex
)
number
)
*
x
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
+
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
(
a
: ( (
complex
) (
complex
)
number
)
*
(
(
x
: ( (
complex
) (
complex
)
number
)
+
(
b
: ( (
complex
) (
complex
)
number
)
/
(
2 : ( ( ) ( non
zero
natural
complex
ext-real
positive
real
V16
()
V17
()
V18
()
V19
()
V20
()
V21
() )
M3
(
REAL
: ( ( ) (
V16
()
V17
()
V18
()
V22
() )
set
) ,
NAT
: ( ( ) (
V16
()
V17
()
V18
()
V19
()
V20
()
V21
()
V22
() )
M2
(
K6
(
REAL
: ( ( ) (
V16
()
V17
()
V18
()
V22
() )
set
) ) : ( ( ) ( )
set
) )) ))
*
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
^2
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
-
(
(
delta
(
a
: ( (
complex
) (
complex
)
number
) ,
b
: ( (
complex
) (
complex
)
number
) ,
c
: ( (
complex
) (
complex
)
number
) )
)
: ( ( ) (
complex
)
set
)
/
(
4 : ( ( ) ( non
zero
natural
complex
ext-real
positive
real
V16
()
V17
()
V18
()
V19
()
V20
()
V21
() )
M3
(
REAL
: ( ( ) (
V16
()
V17
()
V18
()
V22
() )
set
) ,
NAT
: ( ( ) (
V16
()
V17
()
V18
()
V19
()
V20
()
V21
()
V22
() )
M2
(
K6
(
REAL
: ( ( ) (
V16
()
V17
()
V18
()
V22
() )
set
) ) : ( ( ) ( )
set
) )) ))
*
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: QUIN_1:2
errorfrm ;
theorem
:: QUIN_1:3
errorfrm ;
theorem
:: QUIN_1:4
errorfrm ;
theorem
:: QUIN_1:5
errorfrm ;
theorem
:: QUIN_1:6
errorfrm ;
theorem
:: QUIN_1:7
errorfrm ;
theorem
:: QUIN_1:8
errorfrm ;
theorem
:: QUIN_1:9
errorfrm ;
theorem
:: QUIN_1:10
errorfrm ;
theorem
:: QUIN_1:11
errorfrm ;
theorem
:: QUIN_1:12
errorfrm ;
theorem
:: QUIN_1:13
errorfrm ;
theorem
:: QUIN_1:14
for
a
,
b
,
c
,
x
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
natural
complex
ext-real
real
V16
()
V17
()
V18
()
V19
()
V20
()
V21
() )
M3
(
REAL
: ( ( ) (
V16
()
V17
()
V18
()
V22
() )
set
) ,
NAT
: ( ( ) (
V16
()
V17
()
V18
()
V19
()
V20
()
V21
()
V22
() )
M2
(
K6
(
REAL
: ( ( ) (
V16
()
V17
()
V18
()
V22
() )
set
) ) : ( ( ) ( )
set
) )) )) &
(
(
a
: ( (
complex
) (
complex
)
number
)
*
(
x
: ( (
complex
) (
complex
)
number
)
^2
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
+
(
b
: ( (
complex
) (
complex
)
number
)
*
x
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
+
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
0
: ( ( ) (
natural
complex
ext-real
real
V16
()
V17
()
V18
()
V19
()
V20
()
V21
() )
M3
(
REAL
: ( ( ) (
V16
()
V17
()
V18
()
V22
() )
set
) ,
NAT
: ( ( ) (
V16
()
V17
()
V18
()
V19
()
V20
()
V21
()
V22
() )
M2
(
K6
(
REAL
: ( ( ) (
V16
()
V17
()
V18
()
V22
() )
set
) ) : ( ( ) ( )
set
) )) )) holds
(
(
(
(
2 : ( ( ) ( non
zero
natural
complex
ext-real
positive
real
V16
()
V17
()
V18
()
V19
()
V20
()
V21
() )
M3
(
REAL
: ( ( ) (
V16
()
V17
()
V18
()
V22
() )
set
) ,
NAT
: ( ( ) (
V16
()
V17
()
V18
()
V19
()
V20
()
V21
()
V22
() )
M2
(
K6
(
REAL
: ( ( ) (
V16
()
V17
()
V18
()
V22
() )
set
) ) : ( ( ) ( )
set
) )) ))
*
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
*
x
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
+
b
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
^2
)
: ( ( ) (
complex
)
set
)
-
(
delta
(
a
: ( (
complex
) (
complex
)
number
) ,
b
: ( (
complex
) (
complex
)
number
) ,
c
: ( (
complex
) (
complex
)
number
) )
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
)
=
0
: ( ( ) (
natural
complex
ext-real
real
V16
()
V17
()
V18
()
V19
()
V20
()
V21
() )
M3
(
REAL
: ( ( ) (
V16
()
V17
()
V18
()
V22
() )
set
) ,
NAT
: ( ( ) (
V16
()
V17
()
V18
()
V19
()
V20
()
V21
()
V22
() )
M2
(
K6
(
REAL
: ( ( ) (
V16
()
V17
()
V18
()
V22
() )
set
) ) : ( ( ) ( )
set
) )) )) ;
theorem
:: QUIN_1:15
errorfrm ;
theorem
:: QUIN_1:16
errorfrm ;
theorem
:: QUIN_1:17
errorfrm ;
theorem
:: QUIN_1:18
errorfrm ;
theorem
:: QUIN_1:19
errorfrm ;
theorem
:: QUIN_1:20
for
a
,
b
,
c
,
x
being ( (
complex
) (
complex
)
number
) st
a
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
natural
complex
ext-real
real
V16
()
V17
()
V18
()
V19
()
V20
()
V21
() )
M3
(
REAL
: ( ( ) (
V16
()
V17
()
V18
()
V22
() )
set
) ,
NAT
: ( ( ) (
V16
()
V17
()
V18
()
V19
()
V20
()
V21
()
V22
() )
M2
(
K6
(
REAL
: ( ( ) (
V16
()
V17
()
V18
()
V22
() )
set
) ) : ( ( ) ( )
set
) )) )) &
delta
(
a
: ( (
complex
) (
complex
)
number
) ,
b
: ( (
complex
) (
complex
)
number
) ,
c
: ( (
complex
) (
complex
)
number
) ) : ( ( ) (
complex
)
set
)
=
0
: ( ( ) (
natural
complex
ext-real
real
V16
()
V17
()
V18
()
V19
()
V20
()
V21
() )
M3
(
REAL
: ( ( ) (
V16
()
V17
()
V18
()
V22
() )
set
) ,
NAT
: ( ( ) (
V16
()
V17
()
V18
()
V19
()
V20
()
V21
()
V22
() )
M2
(
K6
(
REAL
: ( ( ) (
V16
()
V17
()
V18
()
V22
() )
set
) ) : ( ( ) ( )
set
) )) )) &
(
(
a
: ( (
complex
) (
complex
)
number
)
*
(
x
: ( (
complex
) (
complex
)
number
)
^2
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
+
(
b
: ( (
complex
) (
complex
)
number
)
*
x
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
+
c
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
)
set
)
=
0
: ( ( ) (
natural
complex
ext-real
real
V16
()
V17
()
V18
()
V19
()
V20
()
V21
() )
M3
(
REAL
: ( ( ) (
V16
()
V17
()
V18
()
V22
() )
set
) ,
NAT
: ( ( ) (
V16
()
V17
()
V18
()
V19
()
V20
()
V21
()
V22
() )
M2
(
K6
(
REAL
: ( ( ) (
V16
()
V17
()
V18
()
V22
() )
set
) ) : ( ( ) ( )
set
) )) )) holds
x
: ( (
complex
) (
complex
)
number
)
=
-
(
b
: ( (
complex
) (
complex
)
number
)
/
(
2 : ( ( ) ( non
zero
natural
complex
ext-real
positive
real
V16
()
V17
()
V18
()
V19
()
V20
()
V21
() )
M3
(
REAL
: ( ( ) (
V16
()
V17
()
V18
()
V22
() )
set
) ,
NAT
: ( ( ) (
V16
()
V17
()
V18
()
V19
()
V20
()
V21
()
V22
() )
M2
(
K6
(
REAL
: ( ( ) (
V16
()
V17
()
V18
()
V22
() )
set
) ) : ( ( ) ( )
set
) )) ))
*
a
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
) : ( (
complex
) (
complex
)
set
) ;
theorem
:: QUIN_1:21
errorfrm ;
theorem
:: QUIN_1:22
errorfrm ;
theorem
:: QUIN_1:23
errorfrm ;
theorem
:: QUIN_1:24
errorfrm ;
theorem
:: QUIN_1:25
errorfrm ;
theorem
:: QUIN_1:26
errorfrm ;
theorem
:: QUIN_1:27
errorfrm ;