:: PROCAL_1 semantic presentation
begin
theorem
:: PROCAL_1:1
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
'not'
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
(
'not'
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:2
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
(
'not'
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:3
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:4
for
A
being ( ( ) ( )
QC-alphabet
)
for
q
,
p
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:5
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
(
'not'
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:6
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
'not'
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
(
'not'
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
(
'not'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:7
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
(
'not'
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
(
'not'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
'not'
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:8
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:9
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
'not'
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:10
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
'not'
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
'not'
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:11
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:12
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:13
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
(
'not'
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:14
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
(
'not'
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:15
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
'not'
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
'not'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:16
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
'not'
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
'not'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:17
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
'not'
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
(
'not'
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
(
'not'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:18
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
(
'not'
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
(
'not'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
'not'
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:19
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:20
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:21
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:22
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:23
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
<=>
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:24
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
<=>
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:25
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
,
r
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
(
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:26
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
,
r
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
(
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:27
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
,
r
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
(
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:28
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:29
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
(
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
<=>
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:30
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
<=>
(
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:31
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
,
r
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:32
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
,
r
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:33
for
A
being ( ( ) ( )
QC-alphabet
)
for
r
,
p
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
(
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:34
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
,
r
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
(
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:35
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
r
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
(
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:36
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
r
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
(
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:37
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
(
'not'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
'not'
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:38
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
,
r
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
(
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:39
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
,
r
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
(
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:40
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
r
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
(
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:41
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
,
r
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
(
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:42
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) st
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) holds
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:43
for
A
being ( ( ) ( )
QC-alphabet
)
for
q
,
p
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) st
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) holds
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:44
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) st
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) holds
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:45
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) st
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) holds
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:46
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) st
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) holds
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:47
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) st
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) &
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) holds
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:48
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
,
r
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) st
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) holds
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:49
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
,
r
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) st
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) holds
(
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:50
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
,
r
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) st
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) holds
(
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:51
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
,
r
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) st
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) holds
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:52
for
A
being ( ( ) ( )
QC-alphabet
)
for
r
,
p
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) st
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) &
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) holds
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:53
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
r
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) st
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) &
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) holds
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:54
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) st
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) &
'not'
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) holds
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:55
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) st
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) &
'not'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) holds
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:56
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
,
r
,
s
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) st
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) &
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
s
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) holds
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
s
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:57
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
,
r
,
s
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) st
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) &
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
s
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) holds
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
r
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'or'
s
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: PROCAL_1:58
for
A
being ( ( ) ( )
QC-alphabet
)
for
p
,
q
being ( ( ) ( )
Element
of
CQC-WFF
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) st
(
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
'&'
(
'not'
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
(
'not'
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) holds
p
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
=>
q
: ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
) : ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) )
in
TAUT
A
: ( ( ) ( )
QC-alphabet
) : ( ( ) ( )
Element
of
K6
(
(
CQC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( ( ) (
V1
() )
Element
of
K6
(
(
QC-WFF
b
1
: ( ( ) ( )
QC-alphabet
)
)
: ( (
V1
() ) (
V1
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;