begin
theorem
for
A being
QC-alphabet for
x,
y,
z being
bound_QC-variable of
A for
p being
Element of
QC-WFF A holds
(
All (
x,
y,
z,
p)
= All (
x,
(All (y,z,p))) &
Ex (
x,
y,
z,
p)
= Ex (
x,
(Ex (y,z,p))) ) ;
theorem
for
A being
QC-alphabet for
p1,
p2 being
Element of
QC-WFF A for
x1,
x2,
y1,
y2,
z1,
z2 being
bound_QC-variable of
A st
All (
x1,
y1,
z1,
p1)
= All (
x2,
y2,
z2,
p2) holds
(
x1 = x2 &
y1 = y2 &
z1 = z2 &
p1 = p2 )
theorem
for
A being
QC-alphabet for
x,
y,
z being
bound_QC-variable of
A for
p,
q being
Element of
QC-WFF A for
t,
s being
bound_QC-variable of
A st
All (
x,
y,
z,
p)
= All (
t,
s,
q) holds
(
x = t &
y = s &
All (
z,
p)
= q )
theorem
for
A being
QC-alphabet for
p1,
p2 being
Element of
QC-WFF A for
x1,
x2,
y1,
y2,
z1,
z2 being
bound_QC-variable of
A st
Ex (
x1,
y1,
z1,
p1)
= Ex (
x2,
y2,
z2,
p2) holds
(
x1 = x2 &
y1 = y2 &
z1 = z2 &
p1 = p2 )
theorem
for
A being
QC-alphabet for
x,
y,
z being
bound_QC-variable of
A for
p,
q being
Element of
QC-WFF A for
t,
s being
bound_QC-variable of
A st
Ex (
x,
y,
z,
p)
= Ex (
t,
s,
q) holds
(
x = t &
y = s &
Ex (
z,
p)
= q )
theorem
for
A being
QC-alphabet for
x,
y,
z being
bound_QC-variable of
A for
p being
Element of
QC-WFF A holds
(
All (
x,
y,
z,
p) is
universal &
bound_in (All (x,y,z,p)) = x &
the_scope_of (All (x,y,z,p)) = All (
y,
z,
p) )
by Th7, QC_LANG1:def 21;
:: Immediate constituents of QC-formulae
::