cqc_sim1.miz
begin
reserve A for
QC-alphabet;
definition
let A;
let b be
bound_QC-variable of A;
::
CQC_SIM1:def1
func
x. b ->
QC-symbol of A means
:
Def1: (
x. it )
= b;
existence by
QC_LANG3: 30;
uniqueness by
XTUPLE_0: 1;
end
theorem ::
CQC_SIM1:1
Th1: for x,y be
set, f be
Function holds (
Im ((f
+* (x
.--> y)),x))
=
{y}
proof
let x,y be
set, f be
Function;
now
let u be
object;
thus u
in ((f
+* (x
.--> y))
.:
{x}) implies u
= y
proof
assume u
in ((f
+* (x
.--> y))
.:
{x});
then
consider z be
object such that z
in (
dom (f
+* (x
.--> y))) and
A1: z
in
{x} and
A2: u
= ((f
+* (x
.--> y))
. z) by
FUNCT_1:def 6;
z
in (
dom (x
.--> y)) by
A1;
then u
= ((x
.--> y)
. z) by
A2,
FUNCT_4: 13;
hence thesis by
A1,
FUNCOP_1: 7;
end;
A3: x
in
{x} by
TARSKI:def 1;
then
A4: x
in (
dom (x
.--> y));
then
A5: x
in (
dom (f
+* (x
.--> y))) by
FUNCT_4: 12;
((x
.--> y)
. x)
= y by
A3,
FUNCOP_1: 7;
then y
= ((f
+* (x
.--> y))
. x) by
A4,
FUNCT_4: 13;
hence u
= y implies u
in ((f
+* (x
.--> y))
.:
{x}) by
A3,
A5,
FUNCT_1:def 6;
end;
hence thesis by
TARSKI:def 1;
end;
theorem ::
CQC_SIM1:2
Th2: for K,L be
set holds for x,y be
set, f be
Function holds ((f
+* (L
--> y))
.: K)
c= ((f
.: K)
\/
{y})
proof
let K,L be
set, x,y be
set, f be
Function, z be
object;
assume z
in ((f
+* (L
--> y))
.: K);
then
consider u be
object such that
A1: u
in (
dom (f
+* (L
--> y))) and
A2: u
in K and
A3: z
= ((f
+* (L
--> y))
. u) by
FUNCT_1:def 6;
A4: (
dom (L
--> y))
= L;
now
per cases ;
case
A5: u
in L;
then z
= ((L
--> y)
. u) by
A3,
A4,
FUNCT_4: 13;
then z
= y by
A5,
FUNCOP_1: 7;
hence z
in
{y} by
TARSKI:def 1;
end;
case
A6: not u
in L;
then
A7: z
= (f
. u) by
A3,
A4,
FUNCT_4: 11;
u
in (
dom f) by
A1,
A4,
A6,
FUNCT_4: 12;
hence z
in (f
.: K) by
A2,
A7,
FUNCT_1:def 6;
end;
end;
hence thesis by
XBOOLE_0:def 3;
end;
theorem ::
CQC_SIM1:3
Th3: for x,y be
set, g be
Function, A be
set holds ((g
+* (x
.--> y))
.: (A
\
{x}))
= (g
.: (A
\
{x}))
proof
let x,y be
set, g be
Function, A be
set;
thus ((g
+* (x
.--> y))
.: (A
\
{x}))
c= (g
.: (A
\
{x}))
proof
let u be
object;
A1: (
dom (x
.--> y))
=
{x};
assume u
in ((g
+* (x
.--> y))
.: (A
\
{x}));
then
consider z be
object such that
A2: z
in (
dom (g
+* (x
.--> y))) and
A3: z
in (A
\
{x}) and
A4: u
= ((g
+* (x
.--> y))
. z) by
FUNCT_1:def 6;
A5: not z
in
{x} by
A3,
XBOOLE_0:def 5;
then
A6: z
in (
dom g) by
A2,
A1,
FUNCT_4: 12;
u
= (g
. z) by
A4,
A5,
A1,
FUNCT_4: 11;
hence thesis by
A3,
A6,
FUNCT_1:def 6;
end;
let u be
object;
assume u
in (g
.: (A
\
{x}));
then
consider z be
object such that
A7: z
in (
dom g) and
A8: z
in (A
\
{x}) and
A9: u
= (g
. z) by
FUNCT_1:def 6;
not z
in
{x} by
A8,
XBOOLE_0:def 5;
then not z
in (
dom (x
.--> y));
then
A10: u
= ((g
+* (x
.--> y))
. z) by
A9,
FUNCT_4: 11;
z
in (
dom (g
+* (x
.--> y))) by
A7,
FUNCT_4: 12;
hence thesis by
A8,
A10,
FUNCT_1:def 6;
end;
theorem ::
CQC_SIM1:4
Th4: for x,y be
set holds for g be
Function holds for A be
set st not y
in (g
.: (A
\
{x})) holds ((g
+* (x
.--> y))
.: (A
\
{x}))
= (((g
+* (x
.--> y))
.: A)
\
{y})
proof
let x,y be
set, g be
Function, A be
set;
assume
A1: not y
in (g
.: (A
\
{x}));
thus ((g
+* (x
.--> y))
.: (A
\
{x}))
c= (((g
+* (x
.--> y))
.: A)
\
{y})
proof
let u be
object;
A2: (
dom (x
.--> y))
=
{x};
assume
A3: u
in ((g
+* (x
.--> y))
.: (A
\
{x}));
then
consider z be
object such that
A4: z
in (
dom (g
+* (x
.--> y))) and
A5: z
in (A
\
{x}) and
A6: u
= ((g
+* (x
.--> y))
. z) by
FUNCT_1:def 6;
A7: not z
in
{x} by
A5,
XBOOLE_0:def 5;
then
A8: z
in (
dom g) by
A4,
A2,
FUNCT_4: 12;
u
= (g
. z) by
A6,
A7,
A2,
FUNCT_4: 11;
then u
<> y by
A1,
A5,
A8,
FUNCT_1:def 6;
then
A9: not u
in
{y} by
TARSKI:def 1;
((g
+* (x
.--> y))
.: (A
\
{x}))
c= ((g
+* (x
.--> y))
.: A) by
RELAT_1: 123;
hence thesis by
A3,
A9,
XBOOLE_0:def 5;
end;
let u be
object;
assume
A10: u
in (((g
+* (x
.--> y))
.: A)
\
{y});
then
consider z be
object such that
A11: z
in (
dom (g
+* (x
.--> y))) and
A12: z
in A and
A13: u
= ((g
+* (x
.--> y))
. z) by
FUNCT_1:def 6;
now
assume
A14: z
in
{x};
then z
in (
dom (x
.--> y));
then u
= ((x
.--> y)
. z) by
A13,
FUNCT_4: 13;
then u
= y by
A14,
FUNCOP_1: 7;
then u
in
{y} by
TARSKI:def 1;
hence contradiction by
A10,
XBOOLE_0:def 5;
end;
then z
in (A
\
{x}) by
A12,
XBOOLE_0:def 5;
hence thesis by
A11,
A13,
FUNCT_1:def 6;
end;
reserve i,j,k,l,m,n for
Nat;
reserve a,b,e for
set;
reserve t,u,v,w,z for
QC-symbol of A;
reserve p,q,r,s for
Element of (
CQC-WFF A);
reserve x for
Element of (
bound_QC-variables A);
reserve ll for
CQC-variable_list of k, A;
reserve P for
QC-pred_symbol of k, A;
theorem ::
CQC_SIM1:5
Th5: p is
atomic implies ex k, P, ll st p
= (P
! ll)
proof
assume p is
atomic;
then
consider k be
Nat, P be
QC-pred_symbol of k, A, ll be
QC-variable_list of k, A such that
A1: p
= (P
! ll) by
QC_LANG1:def 18;
reconsider k as
Element of
NAT by
ORDINAL1:def 12;
reconsider ll as
QC-variable_list of k, A;
A2: { (ll
. m) where m be
Nat : 1
<= m & m
<= (
len ll) & (ll
. m)
in (
fixed_QC-variables A) }
=
{} by
A1,
CQC_LANG: 7;
{ (ll
. i) where i be
Nat : 1
<= i & i
<= (
len ll) & (ll
. i)
in (
free_QC-variables A) }
=
{} by
A1,
CQC_LANG: 7;
then ll is
CQC-variable_list of k, A by
A2,
CQC_LANG: 5;
hence thesis by
A1;
end;
theorem ::
CQC_SIM1:6
p is
negative implies ex q st p
= (
'not' q)
proof
assume p is
negative;
then
consider r be
Element of (
QC-WFF A) such that
A1: p
= (
'not' r) by
QC_LANG1:def 19;
r is
Element of (
CQC-WFF A) by
A1,
CQC_LANG: 8;
hence thesis by
A1;
end;
theorem ::
CQC_SIM1:7
p is
conjunctive implies ex q, r st p
= (q
'&' r)
proof
assume p is
conjunctive;
then
consider q,r be
Element of (
QC-WFF A) such that
A1: p
= (q
'&' r) by
QC_LANG1:def 20;
A2: r is
Element of (
CQC-WFF A) by
A1,
CQC_LANG: 9;
q is
Element of (
CQC-WFF A) by
A1,
CQC_LANG: 9;
hence thesis by
A1,
A2;
end;
theorem ::
CQC_SIM1:8
p is
universal implies ex x, q st p
= (
All (x,q))
proof
assume p is
universal;
then
consider x be
bound_QC-variable of A, q be
Element of (
QC-WFF A) such that
A1: p
= (
All (x,q)) by
QC_LANG1:def 21;
q is
Element of (
CQC-WFF A) by
A1,
CQC_LANG: 13;
hence thesis by
A1;
end;
theorem ::
CQC_SIM1:9
Th9: for l be
FinSequence holds (
rng l)
= { (l
. i) : 1
<= i & i
<= (
len l) }
proof
let l be
FinSequence;
thus (
rng l)
c= { (l
. i) : 1
<= i & i
<= (
len l) }
proof
let a be
object;
assume a
in (
rng l);
then
consider x be
object such that
A1: x
in (
dom l) and
A2: a
= (l
. x) by
FUNCT_1:def 3;
reconsider k = x as
Element of
NAT by
A1;
A3: k
<= (
len l) by
A1,
FINSEQ_3: 25;
1
<= k by
A1,
FINSEQ_3: 25;
hence thesis by
A2,
A3;
end;
thus { (l
. i) : 1
<= i & i
<= (
len l) }
c= (
rng l)
proof
let a be
object;
assume a
in { (l
. i) : 1
<= i & i
<= (
len l) };
then
consider k be
Nat such that
A4: a
= (l
. k) and
A5: 1
<= k and
A6: k
<= (
len l);
k
in (
dom l) by
A5,
A6,
FINSEQ_3: 25;
hence thesis by
A4,
FUNCT_1:def 3;
end;
end;
scheme ::
CQC_SIM1:sch1
QCFuncExN { Al() ->
QC-alphabet , D() -> non
empty
set , V() ->
Element of D() , A(
object) ->
Element of D() , N(
object,
object) ->
Element of D() , C(
object,
object,
object) ->
Element of D() , Q(
object,
object) ->
Element of D() } :
ex F be
Function of (
QC-WFF Al()), D() st (F
. (
VERUM Al()))
= V() & for p be
Element of (
QC-WFF Al()) holds (p is
atomic implies (F
. p)
= A(p)) & (p is
negative implies (F
. p)
= N(.,p)) & (p is
conjunctive implies (F
. p)
= C(.,.,p)) & (p is
universal implies (F
. p)
= Q(.,p));
defpred
Pfn[
Function of (
QC-WFF Al()), D(),
Nat] means for p be
Element of (
QC-WFF Al()) st (
len (
@ p))
<= $2 holds (p
= (
VERUM Al()) implies ($1
. p)
= V()) & (p is
atomic implies ($1
. p)
= A(p)) & (p is
negative implies ($1
. p)
= N(.,p)) & (p is
conjunctive implies ($1
. p)
= C(.,.,p)) & (p is
universal implies ($1
. p)
= Q(.,p));
defpred
Pfgp[
Element of D(),
Function of (
QC-WFF Al()), D(),
Element of (
QC-WFF Al())] means ($3
= (
VERUM Al()) implies $1
= V()) & ($3 is
atomic implies $1
= A($3)) & ($3 is
negative implies $1
= N(.,$3)) & ($3 is
conjunctive implies $1
= C(.,.,$3)) & ($3 is
universal implies $1
= Q(.,$3));
defpred
S[
Nat] means ex F be
Function of (
QC-WFF Al()), D() st
Pfn[F, $1];
A1: for n be
Nat st
S[n] holds
S[(n
+ 1)]
proof
let n be
Nat;
given F be
Function of (
QC-WFF Al()), D() such that
A2:
Pfn[F, n];
defpred
P[
Element of (
QC-WFF Al()),
Element of D()] means ((
len (
@ $1))
<> (n
+ 1) implies $2
= (F
. $1)) & ((
len (
@ $1))
= (n
+ 1) implies
Pfgp[$2, F, $1]);
A3: for x be
Element of (
QC-WFF Al()) holds ex y be
Element of D() st
P[x, y]
proof
let p be
Element of (
QC-WFF Al());
now
per cases by
QC_LANG1: 9;
case (
len (
@ p))
<> (n
+ 1);
take y = (F
. p);
thus y
= (F
. p);
end;
case
A4: (
len (
@ p))
= (n
+ 1) & p
= (
VERUM Al());
take y = V();
thus
Pfgp[y, F, p] by
A4,
QC_LANG1: 20;
end;
case
A5: (
len (
@ p))
= (n
+ 1) & p is
atomic;
take y = A(p);
thus
Pfgp[y, F, p] by
A5,
QC_LANG1: 20;
end;
case
A6: (
len (
@ p))
= (n
+ 1) & p is
negative;
take y = N(.,p);
thus
Pfgp[y, F, p] by
A6,
QC_LANG1: 20;
end;
case
A7: (
len (
@ p))
= (n
+ 1) & p is
conjunctive;
take y = C(.,.,p);
thus
Pfgp[y, F, p] by
A7,
QC_LANG1: 20;
end;
case
A8: (
len (
@ p))
= (n
+ 1) & p is
universal;
take y = Q(.,p);
thus
Pfgp[y, F, p] by
A8,
QC_LANG1: 20;
end;
end;
hence thesis;
end;
consider G be
Function of (
QC-WFF Al()), D() such that
A9: for p be
Element of (
QC-WFF Al()) holds
P[p, (G
. p)] from
FUNCT_2:sch 3(
A3);
take H = G;
thus
Pfn[H, (n
+ 1)]
proof
let p be
Element of (
QC-WFF Al()) such that
A10: (
len (
@ p))
<= (n
+ 1);
thus p
= (
VERUM Al()) implies (H
. p)
= V()
proof
now
per cases ;
suppose
A11: (
len (
@ p))
<> (n
+ 1);
then
A12: (H
. p)
= (F
. p) by
A9;
(
len (
@ p))
<= n by
A10,
A11,
NAT_1: 8;
hence thesis by
A2,
A12;
end;
suppose (
len (
@ p))
= (n
+ 1);
hence thesis by
A9;
end;
end;
hence thesis;
end;
thus p is
atomic implies (H
. p)
= A(p)
proof
now
per cases ;
suppose
A13: (
len (
@ p))
<> (n
+ 1);
then
A14: (H
. p)
= (F
. p) by
A9;
(
len (
@ p))
<= n by
A10,
A13,
NAT_1: 8;
hence thesis by
A2,
A14;
end;
suppose (
len (
@ p))
= (n
+ 1);
hence thesis by
A9;
end;
end;
hence thesis;
end;
thus p is
negative implies (H
. p)
= N(.,p)
proof
assume
A15: p is
negative;
then (
len (
@ (
the_argument_of p)))
<> (n
+ 1) by
A10,
QC_LANG1: 14;
then
A16: (H
. (
the_argument_of p))
= (F
. (
the_argument_of p)) by
A9;
now
per cases ;
suppose
A17: (
len (
@ p))
<> (n
+ 1);
then
A18: (H
. p)
= (F
. p) by
A9;
(
len (
@ p))
<= n by
A10,
A17,
NAT_1: 8;
hence thesis by
A2,
A15,
A16,
A18;
end;
suppose (
len (
@ p))
= (n
+ 1);
hence thesis by
A9,
A15,
A16;
end;
end;
hence thesis;
end;
thus p is
conjunctive implies (H
. p)
= C(.,.,p)
proof
assume
A19: p is
conjunctive;
then (
len (
@ (
the_right_argument_of p)))
<> (n
+ 1) by
A10,
QC_LANG1: 15;
then
A20: (H
. (
the_right_argument_of p))
= (F
. (
the_right_argument_of p)) by
A9;
(
len (
@ (
the_left_argument_of p)))
<> (n
+ 1) by
A10,
A19,
QC_LANG1: 15;
then
A21: (H
. (
the_left_argument_of p))
= (F
. (
the_left_argument_of p)) by
A9;
now
per cases ;
suppose
A22: (
len (
@ p))
<> (n
+ 1);
then
A23: (H
. p)
= (F
. p) by
A9;
(
len (
@ p))
<= n by
A10,
A22,
NAT_1: 8;
hence thesis by
A2,
A19,
A21,
A20,
A23;
end;
suppose (
len (
@ p))
= (n
+ 1);
hence thesis by
A9,
A19,
A21,
A20;
end;
end;
hence thesis;
end;
thus p is
universal implies (H
. p)
= Q(.,p)
proof
assume
A24: p is
universal;
then (
len (
@ (
the_scope_of p)))
<> (n
+ 1) by
A10,
QC_LANG1: 16;
then
A25: (H
. (
the_scope_of p))
= (F
. (
the_scope_of p)) by
A9;
now
per cases ;
suppose
A26: (
len (
@ p))
<> (n
+ 1);
then
A27: (H
. p)
= (F
. p) by
A9;
(
len (
@ p))
<= n by
A10,
A26,
NAT_1: 8;
hence thesis by
A2,
A24,
A25,
A27;
end;
suppose (
len (
@ p))
= (n
+ 1);
hence thesis by
A9,
A24,
A25;
end;
end;
hence thesis;
end;
end;
end;
defpred
Qfn[
object,
object] means ex p be
Element of (
QC-WFF Al()) st p
= $1 & for g be
Function of (
QC-WFF Al()), D() st
Pfn[g, (
len (
@ p))] holds $2
= (g
. p);
A28:
S[
0 ]
proof
set F = the
Function of (
QC-WFF Al()), D();
take F;
thus thesis by
QC_LANG1: 10;
end;
A29: for n be
Nat holds
S[n] from
NAT_1:sch 2(
A28,
A1);
A30: for x be
object st x
in (
QC-WFF Al()) holds ex y be
object st
Qfn[x, y]
proof
let x be
object;
assume x
in (
QC-WFF Al());
then
reconsider x9 = x as
Element of (
QC-WFF Al());
consider F be
Function of (
QC-WFF Al()), D() such that
A31:
Pfn[F, (
len (
@ x9))] by
A29;
take (F
. x), x9;
thus x
= x9;
let G be
Function of (
QC-WFF Al()), D() such that
A32:
Pfn[G, (
len (
@ x9))];
defpred
Prop[
Element of (
QC-WFF Al())] means (
len (
@ $1))
<= (
len (
@ x9)) implies (F
. $1)
= (G
. $1);
A33:
now
let p be
Element of (
QC-WFF Al());
thus p is
atomic implies
Prop[p]
proof
assume that
A34: p is
atomic and
A35: (
len (
@ p))
<= (
len (
@ x9));
thus (F
. p)
= A(p) by
A31,
A34,
A35
.= (G
. p) by
A32,
A34,
A35;
end;
thus
Prop[(
VERUM Al())]
proof
assume
A36: (
len (
@ (
VERUM Al())))
<= (
len (
@ x9));
hence (F
. (
VERUM Al()))
= V() by
A31
.= (G
. (
VERUM Al())) by
A32,
A36;
end;
thus p is
negative &
Prop[(
the_argument_of p)] implies
Prop[p]
proof
assume that
A37: p is
negative and
A38:
Prop[(
the_argument_of p)] and
A39: (
len (
@ p))
<= (
len (
@ x9));
(
len (
@ (
the_argument_of p)))
< (
len (
@ p)) by
A37,
QC_LANG1: 14;
hence (F
. p)
= N(.,p) by
A31,
A37,
A38,
A39,
XXREAL_0: 2
.= (G
. p) by
A32,
A37,
A39;
end;
thus p is
conjunctive &
Prop[(
the_left_argument_of p)] &
Prop[(
the_right_argument_of p)] implies
Prop[p]
proof
assume that
A40: p is
conjunctive and
A41:
Prop[(
the_left_argument_of p)] and
A42:
Prop[(
the_right_argument_of p)] and
A43: (
len (
@ p))
<= (
len (
@ x9));
A44: (
len (
@ (
the_right_argument_of p)))
< (
len (
@ p)) by
A40,
QC_LANG1: 15;
(
len (
@ (
the_left_argument_of p)))
< (
len (
@ p)) by
A40,
QC_LANG1: 15;
hence (F
. p)
= C(.,.,p) by
A31,
A40,
A41,
A42,
A43,
A44,
XXREAL_0: 2
.= (G
. p) by
A32,
A40,
A43;
end;
thus p is
universal &
Prop[(
the_scope_of p)] implies
Prop[p]
proof
assume that
A45: p is
universal and
A46:
Prop[(
the_scope_of p)] and
A47: (
len (
@ p))
<= (
len (
@ x9));
(
len (
@ (
the_scope_of p)))
< (
len (
@ p)) by
A45,
QC_LANG1: 16;
hence (F
. p)
= Q(.,p) by
A31,
A45,
A46,
A47,
XXREAL_0: 2
.= (G
. p) by
A32,
A45,
A47;
end;
end;
for p be
Element of (
QC-WFF Al()) holds
Prop[p] from
QC_LANG1:sch 2(
A33);
hence thesis;
end;
consider F be
Function such that
A48: (
dom F)
= (
QC-WFF Al()) and
A49: for x be
object st x
in (
QC-WFF Al()) holds
Qfn[x, (F
. x)] from
CLASSES1:sch 1(
A30);
(
rng F)
c= D()
proof
let y be
object;
assume y
in (
rng F);
then
consider x be
object such that
A50: x
in (
QC-WFF Al()) and
A51: y
= (F
. x) by
A48,
FUNCT_1:def 3;
consider p be
Element of (
QC-WFF Al()) such that p
= x and
A52: for g be
Function of (
QC-WFF Al()), D() st
Pfn[g, (
len (
@ p))] holds y
= (g
. p) by
A49,
A50,
A51;
consider G be
Function of (
QC-WFF Al()), D() such that
A53:
Pfn[G, (
len (
@ p))] by
A29;
y
= (G
. p) by
A52,
A53;
hence thesis;
end;
then
reconsider F as
Function of (
QC-WFF Al()), D() by
A48,
FUNCT_2:def 1,
RELSET_1: 4;
consider p1 be
Element of (
QC-WFF Al()) such that
A54: p1
= (
VERUM Al()) and
A55: for g be
Function of (
QC-WFF Al()), D() st
Pfn[g, (
len (
@ p1))] holds (F
. (
VERUM Al()))
= (g
. p1) by
A49;
take F;
consider G be
Function of (
QC-WFF Al()), D() such that
A56:
Pfn[G, (
len (
@ p1))] by
A29;
(F
. (
VERUM Al()))
= (G
. (
VERUM Al())) by
A54,
A55,
A56;
hence (F
. (
VERUM Al()))
= V() by
A54,
A56;
let p be
Element of (
QC-WFF Al());
consider p1 be
Element of (
QC-WFF Al()) such that
A57: p1
= p and
A58: for g be
Function of (
QC-WFF Al()), D() st
Pfn[g, (
len (
@ p1))] holds (F
. p)
= (g
. p1) by
A49;
consider G be
Function of (
QC-WFF Al()), D() such that
A59:
Pfn[G, (
len (
@ p1))] by
A29;
set p9 = (
the_scope_of p);
A60: ex p1 be
Element of (
QC-WFF Al()) st p1
= p9 & for g be
Function of (
QC-WFF Al()), D() st
Pfn[g, (
len (
@ p1))] holds (F
. p9)
= (g
. p1) by
A49;
A61: (F
. p)
= (G
. p) by
A57,
A58,
A59;
hence p is
atomic implies (F
. p)
= A(p) by
A57,
A59;
A62: for k be
Element of
NAT st k
< (
len (
@ p)) holds
Pfn[G, k]
proof
let k be
Element of
NAT ;
assume
A63: k
< (
len (
@ p));
let p9 be
Element of (
QC-WFF Al());
assume (
len (
@ p9))
<= k;
then (
len (
@ p9))
<= (
len (
@ p)) by
A63,
XXREAL_0: 2;
hence thesis by
A57,
A59;
end;
thus p is
negative implies (F
. p)
= N(.,p)
proof
set p9 = (
the_argument_of p);
set k = (
len (
@ p9));
A64: ex p1 be
Element of (
QC-WFF Al()) st p1
= p9 & for g be
Function of (
QC-WFF Al()), D() st
Pfn[g, (
len (
@ p1))] holds (F
. p9)
= (g
. p1) by
A49;
assume
A65: p is
negative;
then k
< (
len (
@ p)) by
QC_LANG1: 14;
then
Pfn[G, k] by
A62;
then (F
. p9)
= (G
. p9) by
A64;
hence thesis by
A57,
A59,
A61,
A65;
end;
thus p is
conjunctive implies (F
. p)
= C(.,.,p)
proof
set p99 = (
the_right_argument_of p);
set p9 = (
the_left_argument_of p);
set k9 = (
len (
@ p9));
set k99 = (
len (
@ p99));
A66: ex p2 be
Element of (
QC-WFF Al()) st p2
= p99 & for g be
Function of (
QC-WFF Al()), D() st
Pfn[g, (
len (
@ p2))] holds (F
. p99)
= (g
. p2) by
A49;
assume
A67: p is
conjunctive;
then k9
< (
len (
@ p)) by
QC_LANG1: 15;
then
A68:
Pfn[G, k9] by
A62;
k99
< (
len (
@ p)) by
A67,
QC_LANG1: 15;
then
Pfn[G, k99] by
A62;
then
A69: (F
. p99)
= (G
. p99) by
A66;
ex p1 be
Element of (
QC-WFF Al()) st p1
= p9 & for g be
Function of (
QC-WFF Al()), D() st
Pfn[g, (
len (
@ p1))] holds (F
. p9)
= (g
. p1) by
A49;
then (F
. p9)
= (G
. p9) by
A68;
hence thesis by
A57,
A59,
A61,
A67,
A69;
end;
set k = (
len (
@ p9));
assume
A70: p is
universal;
then k
< (
len (
@ p)) by
QC_LANG1: 16;
then
Pfn[G, k] by
A62;
then (F
. p9)
= (G
. p9) by
A60;
hence thesis by
A57,
A59,
A61,
A70;
end;
scheme ::
CQC_SIM1:sch2
CQCF2FuncEx { Al() ->
QC-alphabet , D,E() -> non
empty
set , V() ->
Element of (
Funcs (D(),E())) , A(
object,
object,
object) ->
Element of (
Funcs (D(),E())) , N(
object,
object) ->
Element of (
Funcs (D(),E())) , C(
object,
object,
object,
object) ->
Element of (
Funcs (D(),E())) , Q(
object,
object,
object) ->
Element of (
Funcs (D(),E())) } :
ex F be
Function of (
CQC-WFF Al()), (
Funcs (D(),E())) st (F
. (
VERUM Al()))
= V() & (for k holds for l be
CQC-variable_list of k, Al() holds for P be
QC-pred_symbol of k, Al() holds (F
. (P
! l))
= A(k,P,l)) & for r,s be
Element of (
CQC-WFF Al()) holds for x be
Element of (
bound_QC-variables Al()) holds (F
. (
'not' r))
= N(.,r) & (F
. (r
'&' s))
= C(.,.,r,s) & (F
. (
All (x,r)))
= Q(x,.,r);
deffunc
q(
set,
Element of (
QC-WFF Al())) = Q(bound_in,$1,the_scope_of);
deffunc
c(
set,
set,
Element of (
QC-WFF Al())) = C($1,$2,the_left_argument_of,the_right_argument_of);
deffunc
n(
set,
Element of (
QC-WFF Al())) = N($1,the_argument_of);
deffunc
a(
Element of (
QC-WFF Al())) = A(the_arity_of,the_pred_symbol_of,the_arguments_of);
consider F be
Function of (
QC-WFF Al()), (
Funcs (D(),E())) such that
A1: (F
. (
VERUM Al()))
= V() & for p be
Element of (
QC-WFF Al()) holds (p is
atomic implies (F
. p)
=
a(p)) & (p is
negative implies (F
. p)
=
n(.,p)) & (p is
conjunctive implies (F
. p)
=
c(.,.,p)) & (p is
universal implies (F
. p)
=
q(.,p)) from
QCFuncExN;
reconsider G = (F
| (
CQC-WFF Al())) as
Function of (
CQC-WFF Al()), (
Funcs (D(),E())) by
FUNCT_2: 32;
take G;
thus (G
. (
VERUM Al()))
= V() by
A1,
FUNCT_1: 49;
thus for k holds for l be
CQC-variable_list of k, Al() holds for P be
QC-pred_symbol of k, Al() holds (G
. (P
! l))
= A(k,P,l)
proof
let k;
let l be
CQC-variable_list of k, Al();
let P be
QC-pred_symbol of k, Al();
A2: (
the_arity_of P)
= k by
QC_LANG1: 11;
A3: (P
! l) is
atomic by
QC_LANG1:def 18;
then
A4: (
the_arguments_of (P
! l))
= l by
QC_LANG1:def 23;
A5: (
the_pred_symbol_of (P
! l))
= P by
A3,
QC_LANG1:def 22;
thus (G
. (P
! l))
= (F
. (P
! l)) by
FUNCT_1: 49
.= A(k,P,l) by
A1,
A3,
A4,
A5,
A2;
end;
let r,s be
Element of (
CQC-WFF Al()), x be
Element of (
bound_QC-variables Al());
set r9 = (G
. r), s9 = (G
. s);
A6: r9
= (F
. r) by
FUNCT_1: 49;
A7: (
'not' r) is
negative by
QC_LANG1:def 19;
then
A8: (
the_argument_of (
'not' r))
= r by
QC_LANG1:def 24;
thus (G
. (
'not' r))
= (F
. (
'not' r)) by
FUNCT_1: 49
.= N(r9,r) by
A1,
A6,
A7,
A8;
A9: s9
= (F
. s) by
FUNCT_1: 49;
A10: (r
'&' s) is
conjunctive by
QC_LANG1:def 20;
then
A11: (
the_left_argument_of (r
'&' s))
= r by
QC_LANG1:def 25;
A12: (
the_right_argument_of (r
'&' s))
= s by
A10,
QC_LANG1:def 26;
thus (G
. (r
'&' s))
= (F
. (r
'&' s)) by
FUNCT_1: 49
.= C(r9,s9,r,s) by
A1,
A6,
A9,
A10,
A11,
A12;
A13: (
All (x,r)) is
universal by
QC_LANG1:def 21;
then
A14: (
bound_in (
All (x,r)))
= x by
QC_LANG1:def 27;
A15: (
the_scope_of (
All (x,r)))
= r by
A13,
QC_LANG1:def 28;
thus (G
. (
All (x,r)))
= (F
. (
All (x,r))) by
FUNCT_1: 49
.= Q(x,r9,r) by
A1,
A6,
A13,
A14,
A15;
end;
scheme ::
CQC_SIM1:sch3
CQCF2FUniq { Al() ->
QC-alphabet , D,E() -> non
empty
set , F1,F2() ->
Function of (
CQC-WFF Al()), (
Funcs (D(),E())) , V() ->
Function of D(), E() , A(
object,
object,
object) ->
Function of D(), E() , N(
object,
object) ->
Function of D(), E() , C(
object,
object,
object,
object) ->
Function of D(), E() , Q(
object,
object,
object) ->
Function of D(), E() } :
F1()
= F2()
provided
A1: (F1()
. (
VERUM Al()))
= V()
and
A2: for k holds for ll be
CQC-variable_list of k, Al() holds for P be
QC-pred_symbol of k, Al() holds (F1()
. (P
! ll))
= A(k,P,ll)
and
A3: for r,s be
Element of (
CQC-WFF Al()) holds for x be
Element of (
bound_QC-variables Al()) holds (F1()
. (
'not' r))
= N(.,r) & (F1()
. (r
'&' s))
= C(.,.,r,s) & (F1()
. (
All (x,r)))
= Q(x,.,r)
and
A4: (F2()
. (
VERUM Al()))
= V()
and
A5: for k holds for ll be
CQC-variable_list of k, Al() holds for P be
QC-pred_symbol of k, Al() holds (F2()
. (P
! ll))
= A(k,P,ll)
and
A6: for r,s be
Element of (
CQC-WFF Al()) holds for x be
Element of (
bound_QC-variables Al()) holds (F2()
. (
'not' r))
= N(.,r) & (F2()
. (r
'&' s))
= C(.,.,r,s) & (F2()
. (
All (x,r)))
= Q(x,.,r);
defpred
P[
set] means (F1()
. $1)
= (F2()
. $1);
A7: for r,s be
Element of (
CQC-WFF Al()) holds for x be
bound_QC-variable of Al() holds for k be
Nat holds for ll be
CQC-variable_list of k, Al() holds for P be
QC-pred_symbol of k, Al() holds
P[(
VERUM Al())] &
P[(P
! ll)] & (
P[r] implies
P[(
'not' r)]) & (
P[r] &
P[s] implies
P[(r
'&' s)]) & (
P[r] implies
P[(
All (x,r))])
proof
let r,s be
Element of (
CQC-WFF Al());
let x be
Element of (
bound_QC-variables Al());
let k be
Nat;
let ll be
CQC-variable_list of k, Al();
let P be
QC-pred_symbol of k, Al();
thus (F1()
. (
VERUM Al()))
= (F2()
. (
VERUM Al())) by
A1,
A4;
reconsider k as
Element of
NAT by
ORDINAL1:def 12;
reconsider l1 = ll as
CQC-variable_list of k, Al();
(F1()
. (P
! l1))
= A(k,P,l1) by
A2;
hence (F1()
. (P
! ll))
= (F2()
. (P
! ll)) by
A5;
(F1()
. (
'not' r))
= N(.,r) by
A3;
hence (F1()
. r)
= (F2()
. r) implies (F1()
. (
'not' r))
= (F2()
. (
'not' r)) by
A6;
(F1()
. (r
'&' s))
= C(.,.,r,s) by
A3;
hence (F1()
. r)
= (F2()
. r) & (F1()
. s)
= (F2()
. s) implies (F1()
. (r
'&' s))
= (F2()
. (r
'&' s)) by
A6;
(F1()
. (
All (x,r)))
= Q(x,.,r) by
A3;
hence thesis by
A6;
end;
for r be
Element of (
CQC-WFF Al()) holds
P[r] from
CQC_LANG:sch 1(
A7);
hence thesis by
FUNCT_2: 63;
end;
theorem ::
CQC_SIM1:10
Th10: p
is_subformula_of (
'not' p)
proof
p
is_proper_subformula_of (
'not' p) by
QC_LANG2: 66;
hence thesis by
QC_LANG2:def 21;
end;
theorem ::
CQC_SIM1:11
Th11: p
is_subformula_of (p
'&' q) & q
is_subformula_of (p
'&' q)
proof
A1: q
is_proper_subformula_of (p
'&' q) by
QC_LANG2: 69;
p
is_proper_subformula_of (p
'&' q) by
QC_LANG2: 69;
hence thesis by
A1,
QC_LANG2:def 21;
end;
theorem ::
CQC_SIM1:12
Th12: p
is_subformula_of (
All (x,p))
proof
p
is_proper_subformula_of (
All (x,p)) by
QC_LANG2: 71;
hence thesis by
QC_LANG2:def 21;
end;
theorem ::
CQC_SIM1:13
Th13: for l be
CQC-variable_list of k, A, i st 1
<= i & i
<= (
len l) holds (l
. i)
in (
bound_QC-variables A)
proof
let l be
CQC-variable_list of k, A, i;
assume that
A1: 1
<= i and
A2: i
<= (
len l);
i
in (
dom l) by
A1,
A2,
FINSEQ_3: 25;
then
A3: (l
. i)
in (
rng l) by
FUNCT_1:def 3;
(
rng l)
c= (
bound_QC-variables A) by
RELAT_1:def 19;
hence thesis by
A3;
end;
definition
let A;
let D be non
empty
set, f be
Function of D, (
CQC-WFF A);
::
CQC_SIM1:def2
func
NEGATIVE f ->
Element of (
Funcs (D,(
CQC-WFF A))) means
:
Def2: for a be
Element of D holds for p be
Element of (
CQC-WFF A) st p
= (f
. a) holds (it
. a)
= (
'not' p);
existence
proof
defpred
P[
set,
set] means for p be
Element of (
CQC-WFF A) st p
= (f
. $1) holds $2
= (
'not' p);
A1: for e be
Element of D holds ex u be
Element of (
CQC-WFF A) st
P[e, u]
proof
let e be
Element of D;
reconsider p = (f
. e) as
Element of (
CQC-WFF A);
take (
'not' p);
thus thesis;
end;
consider F be
Function of D, (
CQC-WFF A) such that
A2: for e be
Element of D holds
P[e, (F
. e)] from
FUNCT_2:sch 3(
A1);
F is
Element of (
Funcs (D,(
CQC-WFF A))) by
FUNCT_2: 8;
hence thesis by
A2;
end;
uniqueness
proof
let F,G be
Element of (
Funcs (D,(
CQC-WFF A)));
assume
A3: for a be
Element of D holds for p be
Element of (
CQC-WFF A) st p
= (f
. a) holds (F
. a)
= (
'not' p);
assume
A4: for a be
Element of D holds for p be
Element of (
CQC-WFF A) st p
= (f
. a) holds (G
. a)
= (
'not' p);
for a be
Element of D holds (F
. a)
= (G
. a)
proof
let a be
Element of D;
consider p such that
A5: p
= (f
. a);
thus (F
. a)
= (
'not' p) by
A3,
A5
.= (G
. a) by
A4,
A5;
end;
hence F
= G by
FUNCT_2: 63;
end;
end
reserve f,h for
Element of (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))),
K,L for
Element of (
Fin (
bound_QC-variables A));
definition
let A;
let f,g be
Function of
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):], (
CQC-WFF A), n be
Nat;
::
CQC_SIM1:def3
func
CON (f,g,n) ->
Element of (
Funcs (
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):],(
CQC-WFF A))) means
:
Def3: for t, h, p, q st p
= (f
. (t,h)) & q
= (g
. ((t
+ n),h)) holds (it
. (t,h))
= (p
'&' q);
existence
proof
defpred
P[
Element of (
QC-symbols A),
set,
set] means for p, q st p
= (f
.
[$1, $2]) & q
= (g
.
[($1
+ n), $2]) holds $3
= (p
'&' q);
A1: for t, h holds ex u be
Element of (
CQC-WFF A) st
P[t, h, u]
proof
let t, h;
reconsider p = (f
.
[t, h]) as
Element of (
CQC-WFF A);
reconsider q = (g
.
[(t
+ n), h]) as
Element of (
CQC-WFF A);
take (p
'&' q);
let p1,q1 be
Element of (
CQC-WFF A);
assume that
A2: p1
= (f
.
[t, h]) and
A3: q1
= (g
.
[(t
+ n), h]);
thus thesis by
A2,
A3;
end;
consider F be
Function of
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):], (
CQC-WFF A) such that
A4: for t, h holds
P[t, h, (F
. (t,h))] from
BINOP_1:sch 3(
A1);
reconsider F as
Element of (
Funcs (
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):],(
CQC-WFF A))) by
FUNCT_2: 8;
take F;
let t, h, p, q;
assume that
A5: p
= (f
. (t,h)) and
A6: q
= (g
. ((t
+ n),h));
thus thesis by
A4,
A5,
A6;
end;
uniqueness
proof
let F,G be
Element of (
Funcs (
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):],(
CQC-WFF A)));
assume
A7: for t, h, p, q holds p
= (f
. (t,h)) & q
= (g
. ((t
+ n),h)) implies (F
. (t,h))
= (p
'&' q);
assume
A8: for t, h, p, q holds p
= (f
. (t,h)) & q
= (g
. ((t
+ n),h)) implies (G
. (t,h))
= (p
'&' q);
for a be
Element of
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):] holds (F
. a)
= (G
. a)
proof
let a be
Element of
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):];
consider k be
Element of (
QC-symbols A), h be
Element of (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))) such that
A9: a
=
[k, h] by
DOMAIN_1: 1;
reconsider q = (g
. ((k
+ n),h)) as
Element of (
CQC-WFF A);
reconsider p = (f
. (k,h)) as
Element of (
CQC-WFF A);
(F
. (k,h))
= (p
'&' q) by
A7
.= (G
. (k,h)) by
A8;
hence thesis by
A9;
end;
hence F
= G by
FUNCT_2: 63;
end;
end
Lm1: (h
+* (x
.--> (
x. t))) is
Function of (
bound_QC-variables A), (
bound_QC-variables A)
proof
A1: (
rng (h
+* (x
.--> (
x. t))))
c= ((
rng h)
\/ (
rng (x
.--> (
x. t)))) by
FUNCT_4: 17;
A2: (
rng (x
.--> (
x. t)))
c= (
bound_QC-variables A) by
RELAT_1:def 19;
(
rng h)
c= (
bound_QC-variables A) by
RELAT_1:def 19;
then
A3: ((
rng h)
\/ (
rng (x
.--> (
x. t))))
c= (
bound_QC-variables A) by
A2,
XBOOLE_1: 8;
(
dom (h
+* (x
.--> (
x. t))))
= ((
dom h)
\/ (
dom (
{x}
--> (
x. t)))) by
FUNCT_4:def 1
.= ((
dom h)
\/
{x})
.= ((
bound_QC-variables A)
\/
{x}) by
FUNCT_2: 52
.= (
bound_QC-variables A) by
ZFMISC_1: 40;
hence thesis by
A1,
A3,
FUNCT_2: 2,
XBOOLE_1: 1;
end;
definition
let A;
let f be
Function of
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):], (
CQC-WFF A), x be
bound_QC-variable of A;
::
CQC_SIM1:def4
func
UNIVERSAL (x,f) ->
Element of (
Funcs (
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):],(
CQC-WFF A))) means
:
Def4: for t, h, p st p
= (f
. ((t
++ ),(h
+* (x
.--> (
x. t))))) holds (it
. (t,h))
= (
All ((
x. t),p));
existence
proof
defpred
P[
Element of (
QC-symbols A),
Element of (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))),
set] means for p st p
= (f
.
[($1
++ ), ($2
+* (
{x}
--> (
x. $1)))]) holds $3
= (
All ((
x. $1),p));
A1: for t, h holds ex u be
Element of (
CQC-WFF A) st
P[t, h, u]
proof
let t, h;
reconsider h2 = (h
+* (x
.--> (
x. t))) as
Function of (
bound_QC-variables A), (
bound_QC-variables A) by
Lm1;
reconsider h2 as
Element of (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))) by
FUNCT_2: 8;
reconsider q = (f
.
[(t
++ ), h2]) as
Element of (
CQC-WFF A);
take (
All ((
x. t),q));
thus thesis;
end;
consider F be
Function of
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):], (
CQC-WFF A) such that
A2: for t, h holds
P[t, h, (F
. (t,h))] from
BINOP_1:sch 3(
A1);
reconsider F as
Element of (
Funcs (
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):],(
CQC-WFF A))) by
FUNCT_2: 8;
take F;
let t, h, p;
assume p
= (f
. ((t
++ ),(h
+* (x
.--> (
x. t)))));
hence thesis by
A2;
end;
uniqueness
proof
let F,G be
Element of (
Funcs (
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):],(
CQC-WFF A)));
assume
A3: for t, h, p st p
= (f
. ((t
++ ),(h
+* (x
.--> (
x. t))))) holds (F
. (t,h))
= (
All ((
x. t),p));
assume
A4: for t, h, p st p
= (f
. ((t
++ ),(h
+* (x
.--> (
x. t))))) holds (G
. (t,h))
= (
All ((
x. t),p));
for a be
Element of
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):] holds (F
. a)
= (G
. a)
proof
let a be
Element of
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):];
consider k be
Element of (
QC-symbols A), h be
Element of (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))) such that
A5: a
=
[k, h] by
DOMAIN_1: 1;
reconsider h2 = (h
+* (x
.--> (
x. k))) as
Function of (
bound_QC-variables A), (
bound_QC-variables A) by
Lm1;
reconsider h2 as
Element of (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))) by
FUNCT_2: 8;
reconsider p = (f
. ((k
++ ),h2)) as
Element of (
CQC-WFF A);
(F
. (k,h))
= (
All ((
x. k),p)) by
A3
.= (G
. (k,h)) by
A4;
hence thesis by
A5;
end;
hence F
= G by
FUNCT_2: 63;
end;
end
Lm2: for f be
CQC-variable_list of k, A holds f is
FinSequence of (
bound_QC-variables A)
proof
let f be
CQC-variable_list of k, A;
(
rng f)
c= (
bound_QC-variables A) by
RELAT_1:def 19;
hence thesis by
FINSEQ_1:def 4;
end;
definition
let A;
let k;
let l be
CQC-variable_list of k, A;
let f be
Element of (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A)));
:: original:
*
redefine
func f
* l ->
CQC-variable_list of k, A ;
coherence
proof
reconsider l9 = l as
FinSequence of (
bound_QC-variables A) by
Lm2;
reconsider h = (f
* l9) as
FinSequence of (
bound_QC-variables A) by
FINSEQ_2: 32;
(
len h)
= (
len l9) by
FINSEQ_2: 33
.= k by
CARD_1:def 7;
hence thesis by
CARD_1:def 7,
FINSEQ_2: 24;
end;
end
definition
let A;
let k;
let P be
QC-pred_symbol of k, A, l be
CQC-variable_list of k, A;
::
CQC_SIM1:def5
func
ATOMIC (P,l) ->
Element of (
Funcs (
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):],(
CQC-WFF A))) means
:
Def5: for t, h holds (it
. (t,h))
= (P
! (h
* l));
existence
proof
deffunc
f(
set,
Element of (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A)))) = (P
! ($2
* l));
consider f be
Function of
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):], (
CQC-WFF A) such that
A1: for t, h holds (f
. (t,h))
=
f(t,h) from
BINOP_1:sch 4;
f is
Element of (
Funcs (
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):],(
CQC-WFF A))) by
FUNCT_2: 8;
hence thesis by
A1;
end;
uniqueness
proof
let F,G be
Element of (
Funcs (
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):],(
CQC-WFF A)));
assume
A2: for t, h holds (F
. (t,h))
= (P
! (h
* l));
assume
A3: for t, h holds (G
. (t,h))
= (P
! (h
* l));
for a be
Element of
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):] holds (F
. a)
= (G
. a)
proof
let a be
Element of
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):];
consider k be
Element of (
QC-symbols A), f be
Element of (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))) such that
A4: a
=
[k, f] by
DOMAIN_1: 1;
(F
. (k,f))
= (P
! (f
* l)) by
A2
.= (G
. (k,f)) by
A3;
hence thesis by
A4;
end;
hence F
= G by
FUNCT_2: 63;
end;
end
deffunc
A(
set,
set,
set) =
0 ;
deffunc
N(
Element of
NAT ) = $1;
deffunc
C(
Element of
NAT ,
Element of
NAT ) = ($1
+ $2);
deffunc
Q(
set,
Element of
NAT ) = ($2
+ 1);
definition
let A;
let p;
::
CQC_SIM1:def6
func
QuantNbr (p) ->
Element of
NAT means
:
Def6: ex F be
Function of (
CQC-WFF A),
NAT st it
= (F
. p) & (F
. (
VERUM A))
=
0 & for r, s, x, k holds for l be
CQC-variable_list of k, A holds for P be
QC-pred_symbol of k, A holds (F
. (P
! l))
=
0 & (F
. (
'not' r))
= (F
. r) & (F
. (r
'&' s))
= ((F
. r)
+ (F
. s)) & (F
. (
All (x,r)))
= ((F
. r)
+ 1);
correctness
proof
thus (ex d be
Element of
NAT st ex F be
Function of (
CQC-WFF A),
NAT st d
= (F
. p) & (F
. (
VERUM A))
=
0 & for r,s be
Element of (
CQC-WFF A) holds for x be
bound_QC-variable of A holds for k holds for l be
CQC-variable_list of k, A holds for P be
QC-pred_symbol of k, A holds (F
. (P
! l))
=
A(k,P,l) & (F
. (
'not' r))
=
N(.) & (F
. (r
'&' s))
=
C(.,.) & (F
. (
All (x,r)))
=
Q(x,.)) & for d1,d2 be
Element of
NAT st (ex F be
Function of (
CQC-WFF A),
NAT st d1
= (F
. p) & (F
. (
VERUM A))
=
0 & for r,s be
Element of (
CQC-WFF A) holds for x be
bound_QC-variable of A holds for k holds for l be
CQC-variable_list of k, A holds for P be
QC-pred_symbol of k, A holds (F
. (P
! l))
=
A(k,P,l) & (F
. (
'not' r))
=
N(.) & (F
. (r
'&' s))
=
C(.,.) & (F
. (
All (x,r)))
=
Q(x,.)) & (ex F be
Function of (
CQC-WFF A),
NAT st d2
= (F
. p) & (F
. (
VERUM A))
=
0 & for r,s be
Element of (
CQC-WFF A) holds for x be
bound_QC-variable of A holds for k holds for l be
CQC-variable_list of k, A holds for P be
QC-pred_symbol of k, A holds (F
. (P
! l))
=
A(k,P,l) & (F
. (
'not' r))
=
N(.) & (F
. (r
'&' s))
=
C(.,.) & (F
. (
All (x,r)))
=
Q(x,.)) holds d1
= d2 from
CQC_LANG:sch 4;
end;
end
definition
let A;
let f be
Function of (
CQC-WFF A), (
Funcs (
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):],(
CQC-WFF A))), x be
Element of (
CQC-WFF A);
:: original:
.
redefine
func f
. x ->
Element of (
Funcs (
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):],(
CQC-WFF A))) ;
coherence
proof
thus (f
. x) is
Element of (
Funcs (
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):],(
CQC-WFF A)));
end;
end
definition
let A;
::
CQC_SIM1:def7
func
SepFunc (A) ->
Function of (
CQC-WFF A), (
Funcs (
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):],(
CQC-WFF A))) means
:
Def7: (it
. (
VERUM A))
= (
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):]
--> (
VERUM A)) & (for k holds for l be
CQC-variable_list of k, A holds for P be
QC-pred_symbol of k, A holds (it
. (P
! l))
= (
ATOMIC (P,l))) & for r, s, x holds (it
. (
'not' r))
= (
NEGATIVE (it
. r)) & (it
. (r
'&' s))
= (
CON ((it
. r),(it
. s),(
QuantNbr r))) & (it
. (
All (x,r)))
= (
UNIVERSAL (x,(it
. r)));
existence
proof
deffunc
A(
Nat,
QC-pred_symbol of $1, A,
CQC-variable_list of $1, A) = (
ATOMIC ($2,$3));
set D =
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):];
deffunc
N(
Function of D, (
CQC-WFF A),
set) = (
NEGATIVE $1);
deffunc
C(
Function of D, (
CQC-WFF A),
Function of D, (
CQC-WFF A),
Element of (
CQC-WFF A),
set) = (
CON ($1,$2,(
QuantNbr $3)));
deffunc
Q(
Element of (
bound_QC-variables A),
Function of D, (
CQC-WFF A),
set) = (
UNIVERSAL ($1,$2));
reconsider V = (D
--> (
VERUM A)) as
Function of D, (
CQC-WFF A);
reconsider V as
Element of (
Funcs (D,(
CQC-WFF A))) by
FUNCT_2: 8;
consider F be
Function of (
CQC-WFF A), (
Funcs (D,(
CQC-WFF A))) such that
A1: (F
. (
VERUM A))
= V and
A2: for k holds for l be
CQC-variable_list of k, A holds for P be
QC-pred_symbol of k, A holds (F
. (P
! l))
=
A(k,P,l) and
A3: for r, s, x holds (F
. (
'not' r))
=
N(.,r) & (F
. (r
'&' s))
=
C(.,.,r,s) & (F
. (
All (x,r)))
=
Q(x,.,r) from
CQCF2FuncEx;
take F;
thus thesis by
A1,
A2,
A3;
end;
uniqueness
proof
deffunc
A(
Nat,
QC-pred_symbol of $1, A,
CQC-variable_list of $1, A) = (
ATOMIC ($2,$3));
set D =
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):];
deffunc
N(
Function of D, (
CQC-WFF A),
set) = (
NEGATIVE $1);
deffunc
C(
Function of D, (
CQC-WFF A),
Function of D, (
CQC-WFF A),
Element of (
CQC-WFF A),
set) = (
CON ($1,$2,(
QuantNbr $3)));
deffunc
Q(
Element of (
bound_QC-variables A),
Function of D, (
CQC-WFF A),
set) = (
UNIVERSAL ($1,$2));
reconsider V = (D
--> (
VERUM A)) as
Function of D, (
CQC-WFF A);
let F,G be
Function of (
CQC-WFF A), (
Funcs (D,(
CQC-WFF A))) such that
A4: (F
. (
VERUM A))
= (D
--> (
VERUM A)) and
A5: for k, ll, P holds (F
. (P
! ll))
=
A(k,P,ll) and
A6: for r, s, x holds (F
. (
'not' r))
=
N(.,r) & (F
. (r
'&' s))
=
C(.,.,r,s) & (F
. (
All (x,r)))
=
Q(x,.,r) and
A7: (G
. (
VERUM A))
= (D
--> (
VERUM A)) and
A8: for k, ll, P holds (G
. (P
! ll))
=
A(k,P,ll) and
A9: for r, s, x holds (G
. (
'not' r))
=
N(.,r) & (G
. (r
'&' s))
=
C(.,.,r,s) & (G
. (
All (x,r)))
=
Q(x,.,r);
A10: (G
. (
VERUM A))
= V by
A7;
A11: (F
. (
VERUM A))
= V by
A4;
thus F
= G from
CQCF2FUniq(
A11,
A5,
A6,
A10,
A8,
A9);
end;
end
definition
let A;
let p, t, f;
::
CQC_SIM1:def8
func
SepFunc (p,t,f) ->
Element of (
CQC-WFF A) equals (((
SepFunc A)
. p)
.
[t, f]);
correctness ;
end
theorem ::
CQC_SIM1:14
(
QuantNbr (
VERUM A))
=
0
proof
deffunc
F(
Element of (
CQC-WFF A)) = (
QuantNbr $1);
A1: for d be
Element of
NAT holds d
=
F(p) iff ex F be
Function of (
CQC-WFF A),
NAT st d
= (F
. p) & (F
. (
VERUM A))
=
0 & for r, s, x, k holds for l be
CQC-variable_list of k, A holds for P be
QC-pred_symbol of k, A holds (F
. (P
! l))
=
A(k,P,l) & (F
. (
'not' r))
=
N(.) & (F
. (r
'&' s))
=
C(.,.) & (F
. (
All (x,r)))
=
Q(x,.) by
Def6;
thus
F(VERUM)
=
0 from
CQC_LANG:sch 5(
A1);
end;
theorem ::
CQC_SIM1:15
(
QuantNbr (P
! ll))
=
0
proof
deffunc
F(
Element of (
CQC-WFF A)) = (
QuantNbr $1);
A1: for d be
Element of
NAT holds d
=
F(p) iff ex F be
Function of (
CQC-WFF A),
NAT st d
= (F
. p) & (F
. (
VERUM A))
=
0 & for r, s, x, k holds for l be
CQC-variable_list of k, A holds for P be
QC-pred_symbol of k, A holds (F
. (P
! l))
=
A(k,P,l) & (F
. (
'not' r))
=
N(.) & (F
. (r
'&' s))
=
C(.,.) & (F
. (
All (x,r)))
=
Q(x,.) by
Def6;
thus
F(!)
=
A(k,P,ll) from
CQC_LANG:sch 6(
A1);
end;
theorem ::
CQC_SIM1:16
(
QuantNbr (
'not' p))
= (
QuantNbr p)
proof
deffunc
F(
Element of (
CQC-WFF A)) = (
QuantNbr $1);
A1: for p be
Element of (
CQC-WFF A), d be
Element of
NAT holds d
=
F(p) iff ex F be
Function of (
CQC-WFF A),
NAT st d
= (F
. p) & (F
. (
VERUM A))
=
0 & for r, s, x, k holds for l be
CQC-variable_list of k, A holds for P be
QC-pred_symbol of k, A holds (F
. (P
! l))
=
A(k,P,l) & (F
. (
'not' r))
=
N(.) & (F
. (r
'&' s))
=
C(.,.) & (F
. (
All (x,r)))
=
Q(x,.) by
Def6;
thus
F('not')
=
N(F) from
CQC_LANG:sch 7(
A1);
end;
theorem ::
CQC_SIM1:17
(
QuantNbr (p
'&' q))
= ((
QuantNbr p)
+ (
QuantNbr q))
proof
deffunc
F(
Element of (
CQC-WFF A)) = (
QuantNbr $1);
A1: for p be
Element of (
CQC-WFF A), d be
Element of
NAT holds d
=
F(p) iff ex F be
Function of (
CQC-WFF A),
NAT st d
= (F
. p) & (F
. (
VERUM A))
=
0 & for r, s, x, k holds for l be
CQC-variable_list of k, A holds for P be
QC-pred_symbol of k, A holds (F
. (P
! l))
=
A(k,P,l) & (F
. (
'not' r))
=
N(.) & (F
. (r
'&' s))
=
C(.,.) & (F
. (
All (x,r)))
=
Q(x,.) by
Def6;
thus
F('&')
=
C(F,F) from
CQC_LANG:sch 8(
A1);
end;
theorem ::
CQC_SIM1:18
(
QuantNbr (
All (x,p)))
= ((
QuantNbr p)
+ 1)
proof
deffunc
F(
Element of (
CQC-WFF A)) = (
QuantNbr $1);
A1: for p be
Element of (
CQC-WFF A), d be
Element of
NAT holds d
=
F(p) iff ex F be
Function of (
CQC-WFF A),
NAT st d
= (F
. p) & (F
. (
VERUM A))
=
0 & for r, s, x, k holds for l be
CQC-variable_list of k, A holds for P be
QC-pred_symbol of k, A holds (F
. (P
! l))
=
A(k,P,l) & (F
. (
'not' r))
=
N(.) & (F
. (r
'&' s))
=
C(.,.) & (F
. (
All (x,r)))
=
Q(x,.) by
Def6;
thus
F(All)
=
Q(x,F) from
CQC_LANG:sch 9(
A1);
end;
theorem ::
CQC_SIM1:19
Th19: for p be
Element of (
QC-WFF A) holds (
still_not-bound_in p) is
finite
proof
defpred
P[
Element of (
QC-WFF A)] means (
still_not-bound_in $1) is
finite;
A1: for p be
Element of (
QC-WFF A) holds (p is
atomic implies
P[p]) &
P[(
VERUM A)] & (p is
negative &
P[(
the_argument_of p)] implies
P[p]) & (p is
conjunctive &
P[(
the_left_argument_of p)] &
P[(
the_right_argument_of p)] implies
P[p]) & (p is
universal &
P[(
the_scope_of p)] implies
P[p])
proof
let p be
Element of (
QC-WFF A);
thus p is
atomic implies (
still_not-bound_in p) is
finite
proof
deffunc
F(
set) = ((
the_arguments_of p)
. $1);
defpred
B[
Nat] means 1
<= $1 & $1
<= (
len (
the_arguments_of p));
defpred
A[
Nat] means 1
<= $1 & $1
<= (
len (
the_arguments_of p)) & ((
the_arguments_of p)
. $1)
in (
bound_QC-variables A);
A2: {
F(k) :
A[k] }
c= {
F(n) :
B[n] }
proof
let e be
object;
assume e
in {
F(k) :
A[k] };
then ex k st e
=
F(k) &
A[k];
hence thesis;
end;
assume p is
atomic;
then (
still_not-bound_in p)
= (
still_not-bound_in (
the_arguments_of p)) by
QC_LANG3: 4
.= (
variables_in ((
the_arguments_of p),(
bound_QC-variables A))) by
QC_LANG3: 2
.= { ((
the_arguments_of p)
. k) : 1
<= k & k
<= (
len (
the_arguments_of p)) & ((
the_arguments_of p)
. k)
in (
bound_QC-variables A) };
then (
still_not-bound_in p)
c= (
rng (
the_arguments_of p)) by
A2,
Th9;
hence thesis;
end;
thus (
still_not-bound_in (
VERUM A)) is
finite by
QC_LANG3: 3;
thus p is
negative & (
still_not-bound_in (
the_argument_of p)) is
finite implies (
still_not-bound_in p) is
finite by
QC_LANG3: 6;
thus p is
conjunctive & (
still_not-bound_in (
the_left_argument_of p)) is
finite & (
still_not-bound_in (
the_right_argument_of p)) is
finite implies (
still_not-bound_in p) is
finite
proof
assume that
A3: p is
conjunctive and
A4: (
still_not-bound_in (
the_left_argument_of p)) is
finite and
A5: (
still_not-bound_in (
the_right_argument_of p)) is
finite;
(
still_not-bound_in p)
= ((
still_not-bound_in (
the_left_argument_of p))
\/ (
still_not-bound_in (
the_right_argument_of p))) by
A3,
QC_LANG3: 9;
hence thesis by
A4,
A5;
end;
assume that
A6: p is
universal and
A7: (
still_not-bound_in (
the_scope_of p)) is
finite;
(
still_not-bound_in p)
= ((
still_not-bound_in (
the_scope_of p))
\
{(
bound_in p)}) by
A6,
QC_LANG3: 11;
hence thesis by
A7;
end;
thus for p be
Element of (
QC-WFF A) holds
P[p] from
QC_LANG1:sch 2(
A1);
end;
scheme ::
CQC_SIM1:sch4
MaxFinDomElem { D() -> non
empty
set , X() ->
set , P[
object,
object] } :
ex x be
Element of D() st x
in X() & for y be
Element of D() st y
in X() holds P[x, y]
provided
A1: X() is
finite & X()
<>
{} & X()
c= D()
and
A2: for x,y be
Element of D() holds P[x, y] or P[y, x]
and
A3: for x,y,z be
Element of D() st P[x, y] & P[y, z] holds P[x, z];
reconsider X = X() as
finite
set by
A1;
A4: X
<>
{} by
A1;
defpred
R[
object,
object] means not $1
in X or ($2
in X & P[$1, $2]);
A5: for x,y,z be
object st
R[x, y] &
R[y, z] holds
R[x, z] by
A1,
A3;
A6: for x,y be
object holds
R[x, y] or
R[y, x] by
A1,
A2;
consider x be
object such that
A7: x
in X and
A8: for y be
object st y
in X holds
R[x, y] from
CARD_2:sch 2(
A4,
A6,
A5);
reconsider x as
Element of D() by
A1,
A7;
take x;
thus x
in X() by
A7;
let y be
Element of D();
assume y
in X();
hence thesis by
A7,
A8;
end;
definition
let X be
set;
:: original:
id
redefine
func
id X ->
Element of (
Funcs (X,X)) ;
coherence
proof
(
id X) is
Function of X, X;
hence thesis by
FUNCT_2: 9;
end;
end
definition
let A;
let p;
::
CQC_SIM1:def9
func
NBI p ->
Subset of (
QC-symbols A) equals { t : for u st t
<= u holds not (
x. u)
in (
still_not-bound_in p) };
coherence
proof
defpred
P[
QC-symbol of A] means for u st $1
<= u holds not (
x. u)
in (
still_not-bound_in p);
{ t :
P[t] }
c= (
QC-symbols A) from
FRAENKEL:sch 10;
hence thesis;
end;
end
registration
let A;
let p;
cluster (
NBI p) -> non
empty;
coherence
proof
set A2 = { t : for u st t
<= u holds not (
x. u)
in (
still_not-bound_in p) };
ex t st t
in A2
proof
now
per cases ;
suppose (
still_not-bound_in p)
=
{} ;
then (
0 A)
<= u implies not (
x. u)
in (
still_not-bound_in p);
then (
0 A)
in { t : for u st t
<= u holds not (
x. u)
in (
still_not-bound_in p) };
hence thesis;
end;
suppose
A1: (
still_not-bound_in p)
<>
{} ;
defpred
P[
QC-symbol of A] means (
x. $1)
in (
still_not-bound_in p);
defpred
R[
object,
object] means for t st t
= $2 holds (
x. t)
= $1;
A2: { t :
P[t] }
c= (
QC-symbols A) from
FRAENKEL:sch 10;
A3: for e be
object st e
in (
still_not-bound_in p) holds ex b be
object st b
in (
QC-symbols A) &
R[e, b]
proof
let e be
object;
assume e
in (
still_not-bound_in p);
then
reconsider e as
bound_QC-variable of A;
consider t such that
A4: (
x. t)
= e by
QC_LANG3: 30;
reconsider t as
set;
take t;
thus thesis by
A4;
end;
consider f be
Function such that
A5: (
dom f)
= (
still_not-bound_in p) & (
rng f)
c= (
QC-symbols A) and for e be
object st e
in (
still_not-bound_in p) holds
R[e, (f
. e)] from
FUNCT_1:sch 6(
A3);
reconsider f as
Function of (
still_not-bound_in p), (
QC-symbols A) by
A5,
FUNCT_2:def 1,
RELSET_1: 4;
set x = the
Element of (
still_not-bound_in p);
reconsider x as
bound_QC-variable of A by
A1,
TARSKI:def 3;
consider t such that
A6: (
x. t)
= x by
QC_LANG3: 30;
A7: ex a st a
in { z : (
x. z)
in (
still_not-bound_in p) }
proof
take t;
thus thesis by
A1,
A6;
end;
defpred
R[
QC-symbol of A,
QC-symbol of A] means $2
<= $1;
A8: for t, u holds
R[t, u] or
R[u, t] by
QC_LANG1: 24;
A9: for t, u, v st
R[t, u] &
R[u, v] holds
R[t, v] by
QC_LANG1: 21;
A10: (
still_not-bound_in p) is
finite by
Th19;
deffunc
Z(
bound_QC-variable of A) = (
x. $1);
A11: {
Z(b) where b be
Element of (
bound_QC-variables A) : b
in (
still_not-bound_in p) } is
finite from
FRAENKEL:sch 21(
A10);
{ (
x. b) where b be
Element of (
bound_QC-variables A) : b
in (
still_not-bound_in p) }
= { w : (
x. w)
in (
still_not-bound_in p) }
proof
set S1 = { (
x. b) where b be
Element of (
bound_QC-variables A) : b
in (
still_not-bound_in p) };
set S2 = { w : (
x. w)
in (
still_not-bound_in p) };
for s be
object holds s
in S1 implies s
in S2
proof
let s be
object;
assume s
in S1;
then
consider b be
Element of (
bound_QC-variables A) such that
A12: s
= (
x. b) & b
in (
still_not-bound_in p);
reconsider s1 = s as
QC-symbol of A by
A12;
(
x. s1)
= b by
A12,
Def1;
hence thesis by
A12;
end;
hence S1
c= S2;
for s be
object holds s
in S2 implies s
in S1
proof
let s be
object;
assume s
in S2;
then
consider w such that
A13: s
= w & (
x. w)
in (
still_not-bound_in p);
(
x. (
x. w))
= w by
Def1;
hence thesis by
A13;
end;
hence S2
c= S1;
end;
then
A14: { w : (
x. w)
in (
still_not-bound_in p) } is
finite & { z : (
x. z)
in (
still_not-bound_in p) }
<>
{} & { v : (
x. v)
in (
still_not-bound_in p) }
c= (
QC-symbols A) by
A11,
A2,
A7;
consider v such that v
in { w : (
x. w)
in (
still_not-bound_in p) } and
A15: for t st t
in { z : (
x. z)
in (
still_not-bound_in p) } holds
R[v, t] from
MaxFinDomElem(
A14,
A8,
A9);
now
take n = (v
++ );
thus n
= (v
++ );
let z;
assume that
A16: (v
++ )
<= z and
A17: (
x. z)
in (
still_not-bound_in p);
z
in { w : (
x. w)
in (
still_not-bound_in p) } by
A17;
then z
<= v by
A15;
then (v
++ )
<= v by
A16,
QC_LANG1: 21;
then not v
< (v
++ ) by
QC_LANG1: 25;
hence contradiction by
QC_LANG1: 27;
end;
then (v
++ )
in A2;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis;
end;
end
definition
let A;
let p;
::
CQC_SIM1:def10
func
index p ->
QC-symbol of A equals (
min (
NBI p));
coherence ;
end
theorem ::
CQC_SIM1:20
Th20: (
index p)
= (
0 A) iff p is
closed
proof
thus (
index p)
= (
0 A) implies p is
closed
proof
assume (
index p)
= (
0 A);
then (
0 A)
in (
NBI p) by
QC_LANG1:def 35;
then
consider t such that
A1: t
= (
0 A) & for u st t
<= u holds not (
x. u)
in (
still_not-bound_in p);
now
set a = the
Element of (
still_not-bound_in p);
assume
A2: (
still_not-bound_in p)
<>
{} ;
then
reconsider a as
bound_QC-variable of A by
TARSKI:def 3;
consider u such that
A3: (
x. u)
= a by
QC_LANG3: 30;
not t
<= u by
A1,
A2,
A3;
hence contradiction by
A1,
QC_LANG1:def 36;
end;
hence thesis by
QC_LANG1:def 31;
end;
assume p is
closed;
then (
0 A)
<= t implies not (
x. t)
in (
still_not-bound_in p) by
QC_LANG1:def 31;
then
A4: (
0 A)
in (
NBI p);
(
0 A)
= (
min (
NBI p))
proof
assume (
min (
NBI p))
<> (
0 A);
then
consider t such that
A5: (
0 A)
<> t & t
= (
min (
NBI p));
t
<= (
0 A) by
A4,
A5,
QC_LANG1:def 35;
then t
< (
0 A) by
A5,
QC_LANG1:def 34;
then not (
0 A)
<= t by
QC_LANG1: 25;
hence contradiction by
QC_LANG1:def 36;
end;
hence thesis;
end;
theorem ::
CQC_SIM1:21
Th21: (
x. t)
in (
still_not-bound_in p) implies t
< (
index p)
proof
assume
A1: (
x. t)
in (
still_not-bound_in p);
now
(
min (
NBI p))
in (
NBI p) by
QC_LANG1:def 35;
then
A2: ex u st u
= (
min (
NBI p)) & for t st u
<= t holds not (
x. t)
in (
still_not-bound_in p);
assume (
min (
NBI p))
<= t;
hence contradiction by
A1,
A2;
end;
hence thesis by
QC_LANG1: 25;
end;
theorem ::
CQC_SIM1:22
Th22: (
index (
VERUM A))
= (
0 A)
proof
(
VERUM A) is
closed by
QC_LANG3: 20;
hence thesis by
Th20;
end;
theorem ::
CQC_SIM1:23
Th23: (
index (
'not' p))
= (
index p)
proof
(
still_not-bound_in p)
= (
still_not-bound_in (
'not' p)) by
QC_LANG3: 7;
hence thesis;
end;
theorem ::
CQC_SIM1:24
(
index p)
<= (
index (p
'&' q)) & (
index q)
<= (
index (p
'&' q))
proof
A1: (
still_not-bound_in (p
'&' q))
= ((
still_not-bound_in p)
\/ (
still_not-bound_in q)) by
QC_LANG3: 10;
A2: (
NBI (p
'&' q))
c= (
NBI q)
proof
let e be
object;
assume e
in (
NBI (p
'&' q));
then
consider t such that
A3: t
= e and
A4: for u st t
<= u holds not (
x. u)
in (
still_not-bound_in (p
'&' q));
now
let u;
assume
A5: t
<= u;
(
still_not-bound_in q)
c= (
still_not-bound_in (p
'&' q)) by
A1,
XBOOLE_1: 7;
hence not (
x. u)
in (
still_not-bound_in q) by
A4,
A5;
end;
hence thesis by
A3;
end;
(
NBI (p
'&' q))
c= (
NBI p)
proof
let e be
object;
assume e
in (
NBI (p
'&' q));
then
consider t such that
A6: t
= e and
A7: for u st t
<= u holds not (
x. u)
in (
still_not-bound_in (p
'&' q));
now
let u;
assume
A8: t
<= u;
(
still_not-bound_in p)
c= (
still_not-bound_in (p
'&' q)) by
A1,
XBOOLE_1: 7;
hence not (
x. u)
in (
still_not-bound_in p) by
A7,
A8;
end;
hence thesis by
A6;
end;
hence thesis by
A2,
QC_LANG1: 28;
end;
definition
let A;
let p;
::
CQC_SIM1:def11
func
SepVar (p) ->
Element of (
CQC-WFF A) equals (
SepFunc (p,(
index p),(
id (
bound_QC-variables A))));
coherence ;
end
theorem ::
CQC_SIM1:25
(
SepVar (
VERUM A))
= (
VERUM A)
proof
(
index (
VERUM A))
= (
0 A) by
Th22;
hence (
SepVar (
VERUM A))
= ((
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):]
--> (
VERUM A))
.
[(
0 A), (
id (
bound_QC-variables A))]) by
Def7
.= (
VERUM A);
end;
scheme ::
CQC_SIM1:sch5
CQCInd { A() ->
QC-alphabet , P[
object] } :
for r be
Element of (
CQC-WFF A()) holds P[r]
provided
A1: P[(
VERUM A())]
and
A2: for k holds for l be
CQC-variable_list of k, A() holds for P be
QC-pred_symbol of k, A() holds P[(P
! l)]
and
A3: for r be
Element of (
CQC-WFF A()) st P[r] holds P[(
'not' r)]
and
A4: for r,s be
Element of (
CQC-WFF A()) st P[r] & P[s] holds P[(r
'&' s)]
and
A5: for r be
Element of (
CQC-WFF A()), x be
bound_QC-variable of A() st P[r] holds P[(
All (x,r))];
A6: for r,s be
Element of (
CQC-WFF A()), x be
bound_QC-variable of A(), k be
Nat holds for l be
CQC-variable_list of k, A() holds for P be
QC-pred_symbol of k, A() holds P[(
VERUM A())] & P[(P
! l)] & (P[r] implies P[(
'not' r)]) & (P[r] & P[s] implies P[(r
'&' s)]) & (P[r] implies P[(
All (x,r))]) by
A1,
A2,
A3,
A4,
A5;
thus for r be
Element of (
CQC-WFF A()) holds P[r] from
CQC_LANG:sch 1(
A6);
end;
theorem ::
CQC_SIM1:26
Th26: (
SepVar (P
! ll))
= (P
! ll)
proof
A1: (
dom ll)
= (
dom ll);
(
rng ll)
c= (
bound_QC-variables A) by
RELAT_1:def 19;
then
reconsider lf = ll as
PartFunc of
NAT , (
bound_QC-variables A) by
A1,
RELSET_1: 4;
A2: ((
id (
bound_QC-variables A))
* lf)
= ll by
PARTFUN1: 7;
thus (
SepVar (P
! ll))
= ((
ATOMIC (P,ll))
. ((
index (P
! ll)),(
id (
bound_QC-variables A)))) by
Def7
.= (P
! ll) by
A2,
Def5;
end;
theorem ::
CQC_SIM1:27
p is
atomic implies (
SepVar p)
= p
proof
assume p is
atomic;
then ex k, P, ll st p
= (P
! ll) by
Th5;
hence thesis by
Th26;
end;
theorem ::
CQC_SIM1:28
Th28: (
SepVar (
'not' p))
= (
'not' (
SepVar p))
proof
reconsider FP = ((
SepFunc A)
. p) as
Function of
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):], (
CQC-WFF A);
thus (
SepVar (
'not' p))
= ((
NEGATIVE FP)
.
[(
index (
'not' p)), (
id (
bound_QC-variables A))]) by
Def7
.= ((
NEGATIVE FP)
.
[(
index p), (
id (
bound_QC-variables A))]) by
Th23
.= (
'not' (
SepVar p)) by
Def2;
end;
theorem ::
CQC_SIM1:29
p is
negative & q
= (
the_argument_of p) implies (
SepVar p)
= (
'not' (
SepVar q))
proof
assume that
A1: p is
negative and
A2: q
= (
the_argument_of p);
p
= (
'not' q) by
A1,
A2,
QC_LANG1:def 24;
hence thesis by
Th28;
end;
definition
let A;
let p;
let X be
Subset of
[:(
CQC-WFF A), (
QC-symbols A), (
Fin (
bound_QC-variables A)), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):];
::
CQC_SIM1:def12
pred X
is_Sep-closed_on p means
[p, (
index p), (
{}. (
bound_QC-variables A)), (
id (
bound_QC-variables A))]
in X & (for q, t, K, f holds
[(
'not' q), t, K, f]
in X implies
[q, t, K, f]
in X) & (for q, r, t, K, f holds
[(q
'&' r), t, K, f]
in X implies
[q, t, K, f]
in X &
[r, (t
+ (
QuantNbr q)), K, f]
in X) & for q, x, t, K, f st
[(
All (x,q)), t, K, f]
in X holds
[q, (t
++ ), (K
\/
{x}), (f
+* (x
.--> (
x. t)))]
in X;
end
definition
let A;
let p;
::
CQC_SIM1:def13
func
SepQuadruples p ->
Subset of
[:(
CQC-WFF A), (
QC-symbols A), (
Fin (
bound_QC-variables A)), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):] means
:
Def13: it
is_Sep-closed_on p & for D be
Subset of
[:(
CQC-WFF A), (
QC-symbols A), (
Fin (
bound_QC-variables A)), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):] st D
is_Sep-closed_on p holds it
c= D;
existence
proof
set S =
[:(
CQC-WFF A), (
QC-symbols A), (
Fin (
bound_QC-variables A)), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):];
set A2 = { X where X be
Subset of S : X
is_Sep-closed_on p };
A2
c= (
bool S)
proof
let a be
object;
assume a
in A2;
then ex X be
Subset of S st X
= a & X
is_Sep-closed_on p;
hence thesis;
end;
then
reconsider A2 as
Subset-Family of S;
take X = (
meet A2);
set B = (
[#] S);
B
is_Sep-closed_on p
proof
thus
[p, (
index p), (
{}. (
bound_QC-variables A)), (
id (
bound_QC-variables A))]
in B;
thus for q, t, K, f holds
[(
'not' q), t, K, f]
in B implies
[q, t, K, f]
in B;
thus for q, r, t, K, f holds
[(q
'&' r), t, K, f]
in B implies
[q, t, K, f]
in B &
[r, (t
+ (
QuantNbr q)), K, f]
in B;
let q, x, t, K, f such that
[(
All (x,q)), t, K, f]
in B;
A1: (
rng (f
+* (x
.--> (
x. t))))
c= ((
rng f)
\/ (
rng (x
.--> (
x. t)))) by
FUNCT_4: 17;
A2: (
rng (x
.--> (
x. t)))
=
{(
x. t)} by
FUNCOP_1: 8;
A3: ((
bound_QC-variables A)
\/
{(
x. t)})
= (
bound_QC-variables A) by
ZFMISC_1: 40;
(
rng f)
c= (
bound_QC-variables A) by
RELAT_1:def 19;
then ((
rng f)
\/ (
rng (x
.--> (
x. t))))
c= (
bound_QC-variables A) by
A2,
A3,
XBOOLE_1: 9;
then
A4: (
rng (f
+* (x
.--> (
x. t))))
c= (
bound_QC-variables A) by
A1;
(
dom (f
+* (x
.--> (
x. t))))
= ((
dom f)
\/ (
dom (x
.--> (
x. t)))) by
FUNCT_4:def 1
.= ((
bound_QC-variables A)
\/ (
dom (x
.--> (
x. t)))) by
FUNCT_2:def 1
.= ((
bound_QC-variables A)
\/
{x})
.= (
bound_QC-variables A) by
ZFMISC_1: 40;
then (f
+* (x
.--> (
x. t))) is
Function of (
bound_QC-variables A), (
bound_QC-variables A) by
A4,
FUNCT_2:def 1,
RELSET_1: 4;
then
reconsider ff = (f
+* (x
.--> (
x. t))) as
Element of (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))) by
FUNCT_2: 8;
[q, (t
++ ), (K
\/
{.x.}), ff]
in B;
hence thesis;
end;
then
A5: B
in A2;
for Y be
set st Y
in A2 holds
[p, (
index p), (
{}. (
bound_QC-variables A)), (
id (
bound_QC-variables A))]
in Y
proof
let Y be
set;
assume Y
in A2;
then ex X be
Subset of S st X
= Y & X
is_Sep-closed_on p;
hence thesis;
end;
hence
[p, (
index p), (
{}. (
bound_QC-variables A)), (
id (
bound_QC-variables A))]
in X by
A5,
SETFAM_1:def 1;
thus for q, t, K, f holds
[(
'not' q), t, K, f]
in X implies
[q, t, K, f]
in X
proof
let q, t, K, f such that
A6:
[(
'not' q), t, K, f]
in X;
for Y be
set st Y
in A2 holds
[q, t, K, f]
in Y
proof
let Y be
set;
assume
A7: Y
in A2;
then
A8: ex X be
Subset of S st X
= Y & X
is_Sep-closed_on p;
[(
'not' q), t, K, f]
in Y by
A6,
A7,
SETFAM_1:def 1;
hence thesis by
A8;
end;
hence thesis by
A5,
SETFAM_1:def 1;
end;
thus for q, r, t, K, f holds
[(q
'&' r), t, K, f]
in X implies
[q, t, K, f]
in X &
[r, (t
+ (
QuantNbr q)), K, f]
in X
proof
let q, r, t, K, f such that
A9:
[(q
'&' r), t, K, f]
in X;
for Y be
set st Y
in A2 holds
[q, t, K, f]
in Y
proof
let Y be
set;
assume
A10: Y
in A2;
then
A11: ex X be
Subset of S st X
= Y & X
is_Sep-closed_on p;
[(q
'&' r), t, K, f]
in Y by
A9,
A10,
SETFAM_1:def 1;
hence thesis by
A11;
end;
hence
[q, t, K, f]
in X by
A5,
SETFAM_1:def 1;
for Y be
set st Y
in A2 holds
[r, (t
+ (
QuantNbr q)), K, f]
in Y
proof
let Y be
set;
assume
A12: Y
in A2;
then
A13: ex X be
Subset of S st X
= Y & X
is_Sep-closed_on p;
[(q
'&' r), t, K, f]
in Y by
A9,
A12,
SETFAM_1:def 1;
hence thesis by
A13;
end;
hence thesis by
A5,
SETFAM_1:def 1;
end;
thus for q, x, t, K, f st
[(
All (x,q)), t, K, f]
in X holds
[q, (t
++ ), (K
\/
{x}), (f
+* (x
.--> (
x. t)))]
in X
proof
let q, x, t, K, f such that
A14:
[(
All (x,q)), t, K, f]
in X;
for Y be
set st Y
in A2 holds
[q, (t
++ ), (K
\/
{x}), (f
+* (x
.--> (
x. t)))]
in Y
proof
let Y be
set;
assume
A15: Y
in A2;
then
A16: ex X be
Subset of S st X
= Y & X
is_Sep-closed_on p;
[(
All (x,q)), t, K, f]
in Y by
A14,
A15,
SETFAM_1:def 1;
hence thesis by
A16;
end;
hence thesis by
A5,
SETFAM_1:def 1;
end;
let D be
Subset of S;
assume D
is_Sep-closed_on p;
then D
in A2;
hence thesis by
SETFAM_1: 3;
end;
uniqueness ;
end
theorem ::
CQC_SIM1:30
Th30:
[p, (
index p), (
{}. (
bound_QC-variables A)), (
id (
bound_QC-variables A))]
in (
SepQuadruples p)
proof
(
SepQuadruples p)
is_Sep-closed_on p by
Def13;
hence thesis;
end;
theorem ::
CQC_SIM1:31
Th31: for q, t, K, f st
[(
'not' q), t, K, f]
in (
SepQuadruples p) holds
[q, t, K, f]
in (
SepQuadruples p)
proof
(
SepQuadruples p)
is_Sep-closed_on p by
Def13;
hence thesis;
end;
theorem ::
CQC_SIM1:32
Th32: for q, r, t, K, f st
[(q
'&' r), t, K, f]
in (
SepQuadruples p) holds
[q, t, K, f]
in (
SepQuadruples p) &
[r, (t
+ (
QuantNbr q)), K, f]
in (
SepQuadruples p)
proof
(
SepQuadruples p)
is_Sep-closed_on p by
Def13;
hence thesis;
end;
theorem ::
CQC_SIM1:33
Th33: for q, x, t, K, f st
[(
All (x,q)), t, K, f]
in (
SepQuadruples p) holds
[q, (t
++ ), (K
\/
{x}), (f
+* (x
.--> (
x. t)))]
in (
SepQuadruples p)
proof
(
SepQuadruples p)
is_Sep-closed_on p by
Def13;
hence thesis;
end;
theorem ::
CQC_SIM1:34
Th34:
[q, t, K, f]
in (
SepQuadruples p) implies
[q, t, K, f]
=
[p, (
index p), (
{}. (
bound_QC-variables A)), (
id (
bound_QC-variables A))] or
[(
'not' q), t, K, f]
in (
SepQuadruples p) or (ex r st
[(q
'&' r), t, K, f]
in (
SepQuadruples p)) or (ex r, u st t
= (u
+ (
QuantNbr r)) &
[(r
'&' q), u, K, f]
in (
SepQuadruples p)) or ex x, u, h st (u
++ )
= t & (h
+* (
{x}
--> (
x. u)))
= f & (
[(
All (x,q)), u, K, h]
in (
SepQuadruples p) or
[(
All (x,q)), u, (K
\
{x}), h]
in (
SepQuadruples p))
proof
assume that
A1:
[q, t, K, f]
in (
SepQuadruples p) and
A2:
[q, t, K, f]
<>
[p, (
index p), (
{}. (
bound_QC-variables A)), (
id (
bound_QC-variables A))] and
A3: not
[(
'not' q), t, K, f]
in (
SepQuadruples p) and
A4: not ex r st
[(q
'&' r), t, K, f]
in (
SepQuadruples p) and
A5: not ex r, u st t
= (u
+ (
QuantNbr r)) &
[(r
'&' q), u, K, f]
in (
SepQuadruples p) and
A6: not ex x, u, h st (u
++ )
= t & (h
+* (
{x}
--> (
x. u)))
= f & (
[(
All (x,q)), u, K, h]
in (
SepQuadruples p) or
[(
All (x,q)), u, (K
\
{x}), h]
in (
SepQuadruples p));
reconsider Y = ((
SepQuadruples p)
\
{
[q, t, K, f]}) as
Subset of
[:(
CQC-WFF A), (
QC-symbols A), (
Fin (
bound_QC-variables A)), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):];
A7: (
SepQuadruples p)
is_Sep-closed_on p by
Def13;
A8: for q, t, K, f holds
[(
'not' q), t, K, f]
in Y implies
[q, t, K, f]
in Y
proof
let s, u, L, h;
assume
A9:
[(
'not' s), u, L, h]
in Y;
then s
<> q or u
<> t or L
<> K or f
<> h by
A3,
XBOOLE_0:def 5;
then
A10:
[s, u, L, h]
<>
[q, t, K, f] by
XTUPLE_0: 5;
[(
'not' s), u, L, h]
in (
SepQuadruples p) by
A9,
XBOOLE_0:def 5;
then
[s, u, L, h]
in (
SepQuadruples p) by
A7;
hence thesis by
A10,
ZFMISC_1: 56;
end;
A11: for q, r, t, K, f holds
[(q
'&' r), t, K, f]
in Y implies
[q, t, K, f]
in Y &
[r, (t
+ (
QuantNbr q)), K, f]
in Y
proof
let s, r, u, L, h;
assume
[(s
'&' r), u, L, h]
in Y;
then
A12:
[(s
'&' r), u, L, h]
in (
SepQuadruples p) by
XBOOLE_0:def 5;
then s
<> q or u
<> t or L
<> K or f
<> h by
A4;
then
A13:
[s, u, L, h]
<>
[q, t, K, f] by
XTUPLE_0: 5;
[s, u, L, h]
in (
SepQuadruples p) by
A7,
A12;
hence
[s, u, L, h]
in Y by
A13,
ZFMISC_1: 56;
r
<> q or L
<> K or f
<> h or (u
+ (
QuantNbr s))
<> t by
A5,
A12;
then
A14:
[r, (u
+ (
QuantNbr s)), L, h]
<>
[q, t, K, f] by
XTUPLE_0: 5;
[r, (u
+ (
QuantNbr s)), L, h]
in (
SepQuadruples p) by
A7,
A12;
hence thesis by
A14,
ZFMISC_1: 56;
end;
A15: Y
c= (
SepQuadruples p) by
XBOOLE_1: 36;
A16: for q, x, t, K, f st
[(
All (x,q)), t, K, f]
in Y holds
[q, (t
++ ), (K
\/
{x}), (f
+* (x
.--> (
x. t)))]
in Y
proof
let s, x, u, L, h;
assume
A17:
[(
All (x,s)), u, L, h]
in Y;
now
assume that
A18: not
[(
All (x,q)), u, K, h]
in (
SepQuadruples p) and
A19: not
[(
All (x,q)), u, (K
\
{x}), h]
in (
SepQuadruples p);
A20: s
<> q or L
<> K & L
<> (K
\
{x}) by
A17,
A18,
A19,
XBOOLE_0:def 5;
assume
A21: s
= q;
assume
A22: (L
\/
{x})
= K;
then (K
\
{x})
= (L
\
{x}) by
XBOOLE_1: 40;
hence contradiction by
A20,
A21,
A22,
ZFMISC_1: 40,
ZFMISC_1: 57;
end;
then s
<> q or (u
++ )
<> t or (L
\/
{x})
<> K or f
<> (h
+* (
{x}
--> (
x. u))) by
A6;
then
A23:
[s, (u
++ ), (L
\/
{x}), (h
+* (x
.--> (
x. u)))]
<>
[q, t, K, f] by
XTUPLE_0: 5;
[(
All (x,s)), u, L, h]
in (
SepQuadruples p) by
A17,
XBOOLE_0:def 5;
then
[s, (u
++ ), (L
\/
{x}), (h
+* (x
.--> (
x. u)))]
in (
SepQuadruples p) by
A7;
hence thesis by
A23,
ZFMISC_1: 56;
end;
[p, (
index p), (
{}. (
bound_QC-variables A)), (
id (
bound_QC-variables A))]
in (
SepQuadruples p) by
A7;
then
[p, (
index p), (
{}. (
bound_QC-variables A)), (
id (
bound_QC-variables A))]
in Y by
A2,
ZFMISC_1: 56;
then Y
is_Sep-closed_on p by
A8,
A11,
A16;
then (
SepQuadruples p)
c= Y by
Def13;
then Y
= (
SepQuadruples p) by
A15;
hence contradiction by
A1,
ZFMISC_1: 57;
end;
scheme ::
CQC_SIM1:sch6
Sepregression { A() ->
QC-alphabet , p() ->
Element of (
CQC-WFF A()) , P[
object,
object,
object,
object] } :
for q be
Element of (
CQC-WFF A()), t be
QC-symbol of A(), K be
Element of (
Fin (
bound_QC-variables A())), f be
Element of (
Funcs ((
bound_QC-variables A()),(
bound_QC-variables A()))) st
[q, t, K, f]
in (
SepQuadruples p()) holds P[q, t, K, f]
provided
A1: P[p(), (
index p()), (
{}. (
bound_QC-variables A())), (
id (
bound_QC-variables A()))]
and
A2: for q be
Element of (
CQC-WFF A()), t be
QC-symbol of A(), K be
Element of (
Fin (
bound_QC-variables A())), f be
Element of (
Funcs ((
bound_QC-variables A()),(
bound_QC-variables A()))) st
[(
'not' q), t, K, f]
in (
SepQuadruples p()) & P[(
'not' q), t, K, f] holds P[q, t, K, f]
and
A3: for q,r be
Element of (
CQC-WFF A()), t be
QC-symbol of A(), K be
Element of (
Fin (
bound_QC-variables A())), f be
Element of (
Funcs ((
bound_QC-variables A()),(
bound_QC-variables A()))) st
[(q
'&' r), t, K, f]
in (
SepQuadruples p()) & P[(q
'&' r), t, K, f] holds P[q, t, K, f] & P[r, (t
+ (
QuantNbr q)), K, f]
and
A4: for q be
Element of (
CQC-WFF A()), x be
bound_QC-variable of A(), t be
QC-symbol of A(), K be
Element of (
Fin (
bound_QC-variables A())), f be
Element of (
Funcs ((
bound_QC-variables A()),(
bound_QC-variables A()))) st
[(
All (x,q)), t, K, f]
in (
SepQuadruples p()) & P[(
All (x,q)), t, K, f] holds P[q, (t
++ ), (K
\/
{x}), (f
+* (x
.--> (
x. t)))];
set Y = {
[s, v, M, g] where s be
Element of (
CQC-WFF A()), M be
Element of (
Fin (
bound_QC-variables A())), v be
QC-symbol of A(), g be
Element of (
Funcs ((
bound_QC-variables A()),(
bound_QC-variables A()))) : P[s, v, M, g] };
reconsider X = ((
SepQuadruples p())
/\ Y) as
Subset of
[:(
CQC-WFF A()), (
QC-symbols A()), (
Fin (
bound_QC-variables A())), (
Funcs ((
bound_QC-variables A()),(
bound_QC-variables A()))):];
A5: (
SepQuadruples p())
is_Sep-closed_on p() by
Def13;
X
is_Sep-closed_on p()
proof
A6:
[p(), (
index p()), (
{}. (
bound_QC-variables A())), (
id (
bound_QC-variables A()))]
in Y by
A1;
[p(), (
index p()), (
{}. (
bound_QC-variables A())), (
id (
bound_QC-variables A()))]
in (
SepQuadruples p()) by
Th30;
hence
[p(), (
index p()), (
{}. (
bound_QC-variables A())), (
id (
bound_QC-variables A()))]
in X by
A6,
XBOOLE_0:def 4;
thus for q be
Element of (
CQC-WFF A()), t be
QC-symbol of A(), K be
Element of (
Fin (
bound_QC-variables A())), f be
Element of (
Funcs ((
bound_QC-variables A()),(
bound_QC-variables A()))) holds
[(
'not' q), t, K, f]
in X implies
[q, t, K, f]
in X
proof
let q be
Element of (
CQC-WFF A()), t be
QC-symbol of A(), K be
Element of (
Fin (
bound_QC-variables A())), f be
Element of (
Funcs ((
bound_QC-variables A()),(
bound_QC-variables A())));
assume
A7:
[(
'not' q), t, K, f]
in X;
then
A8:
[(
'not' q), t, K, f]
in (
SepQuadruples p()) by
XBOOLE_0:def 4;
[(
'not' q), t, K, f]
in Y by
A7,
XBOOLE_0:def 4;
then
consider p be
Element of (
CQC-WFF A()), L be
Element of (
Fin (
bound_QC-variables A())), u be
QC-symbol of A(), h be
Element of (
Funcs ((
bound_QC-variables A()),(
bound_QC-variables A()))) such that
A9:
[(
'not' q), t, K, f]
=
[p, u, L, h] and
A10: P[p, u, L, h];
A11: t
= u by
A9,
XTUPLE_0: 5;
A12: f
= h by
A9,
XTUPLE_0: 5;
A13: K
= L by
A9,
XTUPLE_0: 5;
(
'not' q)
= p by
A9,
XTUPLE_0: 5;
then P[q, t, K, f] by
A2,
A8,
A10,
A11,
A13,
A12;
then
A14:
[q, t, K, f]
in Y;
[q, t, K, f]
in (
SepQuadruples p()) by
A5,
A8;
hence thesis by
A14,
XBOOLE_0:def 4;
end;
thus for q,r be
Element of (
CQC-WFF A()), t be
QC-symbol of A(), K be
Element of (
Fin (
bound_QC-variables A())), f be
Element of (
Funcs ((
bound_QC-variables A()),(
bound_QC-variables A()))) holds
[(q
'&' r), t, K, f]
in X implies
[q, t, K, f]
in X &
[r, (t
+ (
QuantNbr q)), K, f]
in X
proof
let q,r be
Element of (
CQC-WFF A()), t be
QC-symbol of A(), K be
Element of (
Fin (
bound_QC-variables A())), f be
Element of (
Funcs ((
bound_QC-variables A()),(
bound_QC-variables A())));
assume
A15:
[(q
'&' r), t, K, f]
in X;
then
A16:
[(q
'&' r), t, K, f]
in (
SepQuadruples p()) by
XBOOLE_0:def 4;
then
A17:
[r, (t
+ (
QuantNbr q)), K, f]
in (
SepQuadruples p()) by
A5;
[(q
'&' r), t, K, f]
in Y by
A15,
XBOOLE_0:def 4;
then
consider p be
Element of (
CQC-WFF A()), L be
Element of (
Fin (
bound_QC-variables A())), u be
QC-symbol of A(), h be
Element of (
Funcs ((
bound_QC-variables A()),(
bound_QC-variables A()))) such that
A18:
[(q
'&' r), t, K, f]
=
[p, u, L, h] and
A19: P[p, u, L, h];
A20: t
= u by
A18,
XTUPLE_0: 5;
A21: f
= h by
A18,
XTUPLE_0: 5;
A22: K
= L by
A18,
XTUPLE_0: 5;
A23: (q
'&' r)
= p by
A18,
XTUPLE_0: 5;
then P[q, t, K, f] by
A3,
A16,
A19,
A20,
A22,
A21;
then
A24:
[q, t, K, f]
in Y;
P[r, (t
+ (
QuantNbr q)), K, f] by
A3,
A16,
A19,
A23,
A20,
A22,
A21;
then
A25:
[r, (t
+ (
QuantNbr q)), K, f]
in Y;
[q, t, K, f]
in (
SepQuadruples p()) by
A5,
A16;
hence thesis by
A24,
A25,
A17,
XBOOLE_0:def 4;
end;
let q be
Element of (
CQC-WFF A()), x be
bound_QC-variable of A(), t be
QC-symbol of A(), K be
Element of (
Fin (
bound_QC-variables A())), f be
Element of (
Funcs ((
bound_QC-variables A()),(
bound_QC-variables A())));
assume
A26:
[(
All (x,q)), t, K, f]
in X;
then
A27:
[(
All (x,q)), t, K, f]
in (
SepQuadruples p()) by
XBOOLE_0:def 4;
(f
+* (x
.--> (
x. t))) is
Function of (
bound_QC-variables A()), (
bound_QC-variables A()) by
Lm1;
then
reconsider g = (f
+* (x
.--> (
x. t))) as
Element of (
Funcs ((
bound_QC-variables A()),(
bound_QC-variables A()))) by
FUNCT_2: 8;
[(
All (x,q)), t, K, f]
in Y by
A26,
XBOOLE_0:def 4;
then
consider p be
Element of (
CQC-WFF A()), L be
Element of (
Fin (
bound_QC-variables A())), u be
QC-symbol of A(), h be
Element of (
Funcs ((
bound_QC-variables A()),(
bound_QC-variables A()))) such that
A28:
[(
All (x,q)), t, K, f]
=
[p, u, L, h] and
A29: P[p, u, L, h];
A30: t
= u by
A28,
XTUPLE_0: 5;
A31: f
= h by
A28,
XTUPLE_0: 5;
A32: K
= L by
A28,
XTUPLE_0: 5;
(
All (x,q))
= p by
A28,
XTUPLE_0: 5;
then P[q, (t
++ ), (K
\/
{x}), g] by
A4,
A27,
A29,
A30,
A32,
A31;
then
A33:
[q, (t
++ ), (K
\/
{.x.}), (f
+* (x
.--> (
x. t)))]
in Y;
[q, (t
++ ), (K
\/
{x}), (f
+* (x
.--> (
x. t)))]
in (
SepQuadruples p()) by
A5,
A27;
hence thesis by
A33,
XBOOLE_0:def 4;
end;
then
A34: (
SepQuadruples p())
c= X by
Def13;
let q be
Element of (
CQC-WFF A()), t be
QC-symbol of A(), K be
Element of (
Fin (
bound_QC-variables A())), f be
Element of (
Funcs ((
bound_QC-variables A()),(
bound_QC-variables A())));
assume
[q, t, K, f]
in (
SepQuadruples p());
then
[q, t, K, f]
in Y by
A34,
XBOOLE_0:def 4;
then
consider p be
Element of (
CQC-WFF A()), L be
Element of (
Fin (
bound_QC-variables A())), u be
QC-symbol of A(), h be
Element of (
Funcs ((
bound_QC-variables A()),(
bound_QC-variables A()))) such that
A35:
[q, t, K, f]
=
[p, u, L, h] and
A36: P[p, u, L, h];
A37: t
= u by
A35,
XTUPLE_0: 5;
A38: K
= L by
A35,
XTUPLE_0: 5;
q
= p by
A35,
XTUPLE_0: 5;
hence thesis by
A35,
A36,
A37,
A38,
XTUPLE_0: 5;
end;
theorem ::
CQC_SIM1:35
Th35: for q, t, K, f holds
[q, t, K, f]
in (
SepQuadruples p) implies q
is_subformula_of p
proof
defpred
P[
Element of (
CQC-WFF A),
set,
set,
set] means $1
is_subformula_of p;
A1:
now
let q, t, K, f such that
[(
'not' q), t, K, f]
in (
SepQuadruples p);
q
is_subformula_of (
'not' q) by
Th10;
hence
P[(
'not' q), t, K, f] implies
P[q, t, K, f] by
QC_LANG2: 57;
end;
A2:
now
let q, x, t, K, f such that
[(
All (x,q)), t, K, f]
in (
SepQuadruples p);
q
is_subformula_of (
All (x,q)) by
Th12;
hence
P[(
All (x,q)), t, K, f] implies
P[q, (t
++ ), (K
\/
{x}), (f
+* (x
.--> (
x. t)))] by
QC_LANG2: 57;
end;
A3:
now
let q, r, t, K, f such that
[(q
'&' r), t, K, f]
in (
SepQuadruples p);
A4: r
is_subformula_of (q
'&' r) by
Th11;
q
is_subformula_of (q
'&' r) by
Th11;
hence
P[(q
'&' r), t, K, f] implies
P[q, t, K, f] &
P[r, (t
+ (
QuantNbr q)), K, f] by
A4,
QC_LANG2: 57;
end;
A5:
P[p, (
index p), (
{}. (
bound_QC-variables A)), (
id (
bound_QC-variables A))];
thus for q, t, K, f st
[q, t, K, f]
in (
SepQuadruples p) holds
P[q, t, K, f] from
Sepregression(
A5,
A1,
A3,
A2);
end;
theorem ::
CQC_SIM1:36
(
SepQuadruples (
VERUM A))
=
{
[(
VERUM A), (
0 A), (
{}. (
bound_QC-variables A)), (
id (
bound_QC-variables A))]}
proof
now
let x be
object;
thus x
in (
SepQuadruples (
VERUM A)) implies x
=
[(
VERUM A), (
0 A), (
{}. (
bound_QC-variables A)), (
id (
bound_QC-variables A))]
proof
assume
A1: x
in (
SepQuadruples (
VERUM A));
then
consider q, t, K, f such that
A2: x
=
[q, t, K, f] by
DOMAIN_1: 10;
A3:
now
given x, v, h such that (v
++ )
= t and (h
+* (
{x}
--> (
x. v)))
= f and
A4:
[(
All (x,q)), v, K, h]
in (
SepQuadruples (
VERUM A)) or
[(
All (x,q)), v, (K
\
{.x.}), h]
in (
SepQuadruples (
VERUM A));
(
All (x,q))
is_subformula_of (
VERUM A) by
A4,
Th35;
then (
All (x,q))
= (
VERUM A) by
QC_LANG2: 79;
then (
VERUM A) is
universal by
QC_LANG1:def 21;
hence contradiction by
QC_LANG1: 20;
end;
A5:
now
given r, v such that t
= (v
+ (
QuantNbr r)) and
A6:
[(r
'&' q), v, K, f]
in (
SepQuadruples (
VERUM A));
(r
'&' q)
is_subformula_of (
VERUM A) by
A6,
Th35;
then (r
'&' q)
= (
VERUM A) by
QC_LANG2: 79;
then (
VERUM A) is
conjunctive by
QC_LANG1:def 20;
hence contradiction by
QC_LANG1: 20;
end;
A7:
now
given r such that
A8:
[(q
'&' r), t, K, f]
in (
SepQuadruples (
VERUM A));
(q
'&' r)
is_subformula_of (
VERUM A) by
A8,
Th35;
then (q
'&' r)
= (
VERUM A) by
QC_LANG2: 79;
then (
VERUM A) is
conjunctive by
QC_LANG1:def 20;
hence contradiction by
QC_LANG1: 20;
end;
A9:
now
assume
[(
'not' q), t, K, f]
in (
SepQuadruples (
VERUM A));
then (
'not' q)
is_subformula_of (
VERUM A) by
Th35;
then (
'not' q)
= (
VERUM A) by
QC_LANG2: 79;
then (
VERUM A) is
negative by
QC_LANG1:def 19;
hence contradiction by
QC_LANG1: 20;
end;
A10: (
index (
VERUM A))
= (
0 A) by
Th22;
set p = (
VERUM A);
[q, t, K, f]
=
[p, (
index p), (
{}. (
bound_QC-variables A)), (
id (
bound_QC-variables A))] or
[(
'not' q), t, K, f]
in (
SepQuadruples p) or (ex r st
[(q
'&' r), t, K, f]
in (
SepQuadruples p)) or (ex r, u st t
= (u
+ (
QuantNbr r)) &
[(r
'&' q), u, K, f]
in (
SepQuadruples p)) or ex x, u, h st (u
++ )
= t & (h
+* (
{x}
--> (
x. u)))
= f & (
[(
All (x,q)), u, K, h]
in (
SepQuadruples p) or
[(
All (x,q)), u, (K
\
{x}), h]
in (
SepQuadruples p)) by
A1,
A2,
Th34;
hence x
=
[(
VERUM A), (
0 A), (
{}. (
bound_QC-variables A)), (
id (
bound_QC-variables A))] by
A2,
A7,
A5,
A3,
A9,
A10;
end;
(
index (
VERUM A))
= (
0 A) by
Th22;
hence x
=
[(
VERUM A), (
0 A), (
{}. (
bound_QC-variables A)), (
id (
bound_QC-variables A))] implies x
in (
SepQuadruples (
VERUM A)) by
Th30;
end;
hence thesis by
TARSKI:def 1;
end;
theorem ::
CQC_SIM1:37
for k holds for l be
CQC-variable_list of k, A holds for P be
QC-pred_symbol of k, A holds (
SepQuadruples (P
! l))
=
{
[(P
! l), (
index (P
! l)), (
{}. (
bound_QC-variables A)), (
id (
bound_QC-variables A))]}
proof
let k;
let l be
CQC-variable_list of k, A;
let P be
QC-pred_symbol of k, A;
A1: (P
! l) is
atomic by
QC_LANG1:def 18;
now
let x be
object;
thus x
in (
SepQuadruples (P
! l)) implies x
=
[(P
! l), (
index (P
! l)), (
{}. (
bound_QC-variables A)), (
id (
bound_QC-variables A))]
proof
assume
A2: x
in (
SepQuadruples (P
! l));
then
consider q, t, K, f such that
A3: x
=
[q, t, K, f] by
DOMAIN_1: 10;
A4:
now
given x, u, h such that (u
++ )
= t and (h
+* (
{x}
--> (
x. u)))
= f and
A5:
[(
All (x,q)), u, K, h]
in (
SepQuadruples (P
! l)) or
[(
All (x,q)), u, (K
\
{.x.}), h]
in (
SepQuadruples (P
! l));
(
All (x,q))
is_subformula_of (P
! l) by
A5,
Th35;
then (
All (x,q))
= (P
! l) by
QC_LANG2: 80;
then (P
! l) is
universal by
QC_LANG1:def 21;
hence contradiction by
A1,
QC_LANG1: 20;
end;
A6:
now
given r, u such that t
= (u
+ (
QuantNbr r)) and
A7:
[(r
'&' q), u, K, f]
in (
SepQuadruples (P
! l));
(r
'&' q)
is_subformula_of (P
! l) by
A7,
Th35;
then (r
'&' q)
= (P
! l) by
QC_LANG2: 80;
then (P
! l) is
conjunctive by
QC_LANG1:def 20;
hence contradiction by
A1,
QC_LANG1: 20;
end;
A8:
now
given r such that
A9:
[(q
'&' r), t, K, f]
in (
SepQuadruples (P
! l));
(q
'&' r)
is_subformula_of (P
! l) by
A9,
Th35;
then (q
'&' r)
= (P
! l) by
QC_LANG2: 80;
then (P
! l) is
conjunctive by
QC_LANG1:def 20;
hence contradiction by
A1,
QC_LANG1: 20;
end;
A10:
now
assume
[(
'not' q), t, K, f]
in (
SepQuadruples (P
! l));
then (
'not' q)
is_subformula_of (P
! l) by
Th35;
then (
'not' q)
= (P
! l) by
QC_LANG2: 80;
then (P
! l) is
negative by
QC_LANG1:def 19;
hence contradiction by
A1,
QC_LANG1: 20;
end;
set p = (P
! l);
[q, t, K, f]
=
[p, (
index p), (
{}. (
bound_QC-variables A)), (
id (
bound_QC-variables A))] or
[(
'not' q), t, K, f]
in (
SepQuadruples p) or (ex r st
[(q
'&' r), t, K, f]
in (
SepQuadruples p)) or (ex r, u st t
= (u
+ (
QuantNbr r)) &
[(r
'&' q), u, K, f]
in (
SepQuadruples p)) or ex x, u, h st (u
++ )
= t & (h
+* (
{x}
--> (
x. u)))
= f & (
[(
All (x,q)), u, K, h]
in (
SepQuadruples p) or
[(
All (x,q)), u, (K
\
{x}), h]
in (
SepQuadruples p)) by
A2,
Th34,
A3;
hence thesis by
A3,
A8,
A6,
A4,
A10;
end;
thus x
=
[(P
! l), (
index (P
! l)), (
{}. (
bound_QC-variables A)), (
id (
bound_QC-variables A))] implies x
in (
SepQuadruples (P
! l)) by
Th30;
end;
hence thesis by
TARSKI:def 1;
end;
theorem ::
CQC_SIM1:38
Th38: for q, t, K, f st
[q, t, K, f]
in (
SepQuadruples p) holds (
still_not-bound_in q)
c= ((
still_not-bound_in p)
\/ K)
proof
deffunc
f(
QC-formula of A) = (
still_not-bound_in $1);
defpred
P[
QC-formula of A,
set,
set,
set] means
f($1)
c= (
f(p)
\/ $3);
A1: for q, t, K, f st
[(
'not' q), t, K, f]
in (
SepQuadruples p) &
P[(
'not' q), t, K, f] holds
P[q, t, K, f] by
QC_LANG3: 7;
A2:
now
let q, r, t, K, f such that
[(q
'&' r), t, K, f]
in (
SepQuadruples p) and
A3:
P[(q
'&' r), t, K, f];
A4: (
still_not-bound_in (q
'&' r))
= ((
still_not-bound_in q)
\/ (
still_not-bound_in r)) by
QC_LANG3: 10;
then
A5: (
still_not-bound_in r)
c= (
still_not-bound_in (q
'&' r)) by
XBOOLE_1: 7;
(
still_not-bound_in q)
c= (
still_not-bound_in (q
'&' r)) by
A4,
XBOOLE_1: 7;
hence
P[q, t, K, f] &
P[r, (t
+ (
QuantNbr q)), K, f] by
A3,
A5,
XBOOLE_1: 1;
end;
A6:
now
let q, x, t, K, f such that
[(
All (x,q)), t, K, f]
in (
SepQuadruples p) and
A7:
P[(
All (x,q)), t, K, f];
(
still_not-bound_in (
All (x,q)))
= ((
still_not-bound_in q)
\
{x}) by
QC_LANG3: 12;
then (
still_not-bound_in q)
c= (((
still_not-bound_in p)
\/ K)
\/
{x}) by
A7,
XBOOLE_1: 44;
hence
P[q, (t
++ ), (K
\/
{x}), (f
+* (x
.--> (
x. t)))] by
XBOOLE_1: 4;
end;
A8:
P[p, (
index p), (
{}. (
bound_QC-variables A)), (
id (
bound_QC-variables A))];
thus for q, t, K, f st
[q, t, K, f]
in (
SepQuadruples p) holds
P[q, t, K, f] from
Sepregression(
A8,
A1,
A2,
A6);
end;
theorem ::
CQC_SIM1:39
Th39:
[q, t, K, f]
in (
SepQuadruples p) & (
x. u)
in (f
.: K) implies u
< t
proof
defpred
P[
Element of (
CQC-WFF A),
QC-symbol of A,
Element of (
Fin (
bound_QC-variables A)),
Function] means for u holds (
x. u)
in ($4
.: $3) implies u
< $2;
A1: for q, v, K, f st
[(
'not' q), v, K, f]
in (
SepQuadruples p) &
P[(
'not' q), v, K, f] holds
P[q, v, K, f];
A2:
now
let q, r, v, K, f;
assume
[(q
'&' r), v, K, f]
in (
SepQuadruples p);
assume
A3:
P[(q
'&' r), v, K, f];
hence
P[q, v, K, f];
thus
P[r, (v
+ (
QuantNbr q)), K, f]
proof
let u;
A4: v
<= (v
+ (
QuantNbr q)) by
QC_LANG1: 31;
assume (
x. u)
in (f
.: K);
hence thesis by
A3,
A4,
QC_LANG1: 30;
end;
end;
A5:
now
let q, x, v, K, f such that
[(
All (x,q)), v, K, f]
in (
SepQuadruples p);
assume
A6:
P[(
All (x,q)), v, K, f];
thus
P[q, (v
++ ), (K
\/
{.x.}), (f
+* (x
.--> (
x. v)))]
proof
let u;
assume (
x. u)
in ((f
+* (x
.--> (
x. v)))
.: (K
\/
{x}));
then (
x. u)
in (((f
+* (x
.--> (
x. v)))
.: K)
\/ ((f
+* (x
.--> (
x. v)))
.:
{x})) by
RELAT_1: 120;
then
A7: (
x. u)
in ((f
+* (x
.--> (
x. v)))
.: K) or (
x. u)
in (
Im ((f
+* (x
.--> (
x. v))),x)) by
XBOOLE_0:def 3;
((f
+* (x
.--> (
x. v)))
.: K)
c= ((f
.: K)
\/
{(
x. v)}) by
Th2;
then (
x. u)
in (f
.: K) or (
x. u)
in
{(
x. v)} by
A7,
Th1,
XBOOLE_0:def 3;
then u
< v or (
x. u)
= (
x. v) by
A6,
TARSKI:def 1;
then u
< v or u
= v by
XTUPLE_0: 1;
then u
<= v & v
< (v
++ ) by
QC_LANG1: 22,
QC_LANG1: 27,
QC_LANG1:def 34;
hence thesis by
QC_LANG1: 29;
end;
end;
A8:
P[p, (
index p), (
{}. (
bound_QC-variables A)), (
id (
bound_QC-variables A))];
for q, v, K, f st
[q, v, K, f]
in (
SepQuadruples p) holds
P[q, v, K, f] from
Sepregression(
A8,
A1,
A2,
A5);
hence thesis;
end;
theorem ::
CQC_SIM1:40
[q, t, K, f]
in (
SepQuadruples p) implies not (
x. t)
in (f
.: K)
proof
assume
A1:
[q, t, K, f]
in (
SepQuadruples p);
assume (
x. t)
in (f
.: K);
then t
< t & t
<= t by
A1,
Th39,
QC_LANG1: 22;
hence contradiction by
QC_LANG1: 25;
end;
theorem ::
CQC_SIM1:41
Th41:
[q, t, K, f]
in (
SepQuadruples p) & (
x. u)
in (f
.: (
still_not-bound_in p)) implies u
< t
proof
defpred
P[
Element of (
CQC-WFF A),
QC-symbol of A,
Element of (
Fin (
bound_QC-variables A)),
Function] means for u holds (
x. u)
in ($4
.: (
still_not-bound_in p)) implies u
< $2;
A1:
now
let q, r, v, K, f;
assume
[(q
'&' r), v, K, f]
in (
SepQuadruples p);
assume
A2:
P[(q
'&' r), v, K, f];
hence
P[q, v, K, f];
thus
P[r, (v
+ (
QuantNbr q)), K, f]
proof
let u;
A3: v
<= (v
+ (
QuantNbr q)) by
QC_LANG1: 31;
assume (
x. u)
in (f
.: (
still_not-bound_in p));
hence thesis by
A2,
A3,
QC_LANG1: 30;
end;
end;
A4:
P[p, (
index p), (
{}. (
bound_QC-variables A)), (
id (
bound_QC-variables A))]
proof
let u;
assume
A5: (
x. u)
in ((
id (
bound_QC-variables A))
.: (
still_not-bound_in p));
((
id (
bound_QC-variables A))
.: (
still_not-bound_in p))
= (
still_not-bound_in p) by
FUNCT_1: 92;
hence thesis by
A5,
Th21;
end;
A6:
now
let q, x, v, K, f such that
[(
All (x,q)), v, K, f]
in (
SepQuadruples p);
assume
A7:
P[(
All (x,q)), v, K, f];
thus
P[q, (v
++ ), (K
\/
{.x.}), (f
+* (x
.--> (
x. v)))]
proof
let u;
assume
A8: (
x. u)
in ((f
+* (x
.--> (
x. v)))
.: (
still_not-bound_in p));
((f
+* (x
.--> (
x. v)))
.: (
still_not-bound_in p))
c= ((f
.: (
still_not-bound_in p))
\/
{(
x. v)}) by
Th2;
then (
x. u)
in (f
.: (
still_not-bound_in p)) or (
x. u)
in
{(
x. v)} by
A8,
XBOOLE_0:def 3;
then u
< v or (
x. u)
= (
x. v) by
A7,
TARSKI:def 1;
then u
< v or u
= v by
XTUPLE_0: 1;
then u
<= v & v
< (v
++ ) by
QC_LANG1: 22,
QC_LANG1: 27,
QC_LANG1:def 34;
hence thesis by
QC_LANG1: 29;
end;
end;
A9: for q, v, K, f st
[(
'not' q), v, K, f]
in (
SepQuadruples p) &
P[(
'not' q), v, K, f] holds
P[q, v, K, f];
for q, v, K, f st
[q, v, K, f]
in (
SepQuadruples p) holds
P[q, v, K, f] from
Sepregression(
A4,
A9,
A1,
A6);
hence thesis;
end;
theorem ::
CQC_SIM1:42
Th42:
[q, t, K, f]
in (
SepQuadruples p) & (
x. u)
in (f
.: (
still_not-bound_in q)) implies u
< t
proof
assume that
A1:
[q, t, K, f]
in (
SepQuadruples p) and
A2: (
x. u)
in (f
.: (
still_not-bound_in q));
(f
.: (
still_not-bound_in q))
c= (f
.: ((
still_not-bound_in p)
\/ K)) by
A1,
Th38,
RELAT_1: 123;
then (
x. u)
in (f
.: ((
still_not-bound_in p)
\/ K)) by
A2;
then (
x. u)
in ((f
.: (
still_not-bound_in p))
\/ (f
.: K)) by
RELAT_1: 120;
then (
x. u)
in (f
.: (
still_not-bound_in p)) or (
x. u)
in (f
.: K) by
XBOOLE_0:def 3;
hence thesis by
A1,
Th39,
Th41;
end;
theorem ::
CQC_SIM1:43
Th43:
[q, t, K, f]
in (
SepQuadruples p) implies not (
x. t)
in (f
.: (
still_not-bound_in q))
proof
assume
A1:
[q, t, K, f]
in (
SepQuadruples p);
assume (
x. t)
in (f
.: (
still_not-bound_in q));
then t
< t & t
<= t by
A1,
Th42,
QC_LANG1: 22;
hence contradiction by
QC_LANG1: 25;
end;
theorem ::
CQC_SIM1:44
Th44: (
still_not-bound_in p)
= (
still_not-bound_in (
SepVar p))
proof
defpred
P[
Element of (
CQC-WFF A)] means for t, K, f st
[$1, t, K, f]
in (
SepQuadruples p) holds (f
.: (
still_not-bound_in $1))
= (
still_not-bound_in (((
SepFunc A)
. $1) qua
Element of (
Funcs (
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):],(
CQC-WFF A)))
.
[t, f] qua
Element of
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):]) qua
Element of (
CQC-WFF A));
A1:
[p, (
index p), (
{}. (
bound_QC-variables A)), (
id (
bound_QC-variables A))]
in (
SepQuadruples p) by
Th30;
A2:
now
let r;
reconsider g = ((
SepFunc A)
. r) as
Function of
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):], (
CQC-WFF A);
assume
A3:
P[r];
A4: ((
SepFunc A)
. (
'not' r))
= (
NEGATIVE g) by
Def7;
thus
P[(
'not' r)]
proof
let u, K, f;
assume
[(
'not' r), u, K, f]
in (
SepQuadruples p);
then
A5:
[r, u, K, f]
in (
SepQuadruples p) by
Th31;
set uf =
[u, f];
reconsider r9 = (g
. uf) as
Element of (
CQC-WFF A);
A6: (
still_not-bound_in r9)
= (
still_not-bound_in (
'not' r9)) by
QC_LANG3: 7;
A7: (
still_not-bound_in r)
= (
still_not-bound_in (
'not' r)) by
QC_LANG3: 7;
((
NEGATIVE g)
. uf)
= (
'not' r9) by
Def2;
hence thesis by
A4,
A3,
A7,
A6,
A5;
end;
end;
A8:
now
let k;
let l be
CQC-variable_list of k, A;
let P be
QC-pred_symbol of k, A;
thus
P[(P
! l)]
proof
let u, K, f such that
[(P
! l), u, K, f]
in (
SepQuadruples p);
set fl = (f
* l);
A9: (f
.: { (l
. i) : 1
<= i & i
<= (
len l) & (l
. i)
in (
bound_QC-variables A) })
= { (fl
. j) : 1
<= j & j
<= (
len fl) & (fl
. j)
in (
bound_QC-variables A) }
proof
A10: (
len fl)
= k by
CARD_1:def 7
.= (
len l) by
CARD_1:def 7;
thus (f
.: { (l
. i) : 1
<= i & i
<= (
len l) & (l
. i)
in (
bound_QC-variables A) })
c= { (fl
. j) : 1
<= j & j
<= (
len fl) & (fl
. j)
in (
bound_QC-variables A) }
proof
let x be
object;
assume x
in (f
.: { (l
. i) : 1
<= i & i
<= (
len l) & (l
. i)
in (
bound_QC-variables A) });
then
consider y be
object such that
A11: y
in (
dom f) & y
in { (l
. i) : 1
<= i & i
<= (
len l) & (l
. i)
in (
bound_QC-variables A) } & x
= (f
. y) by
FUNCT_1:def 6;
consider i such that
A12: y
= (l
. i) and
A13: 1
<= i and
A14: i
<= (
len l) and (l
. i)
in (
bound_QC-variables A) by
A11;
i
in (
dom l) by
A13,
A14,
FINSEQ_3: 25;
then
A15: (f
. (l
. i))
= (fl
. i) by
FUNCT_1: 13;
(fl
. i)
in (
bound_QC-variables A) by
A10,
A13,
A14,
Th13;
hence thesis by
A10,
A11,
A12,
A13,
A14,
A15;
end;
let x be
object;
assume x
in { (fl
. i) : 1
<= i & i
<= (
len fl) & (fl
. i)
in (
bound_QC-variables A) };
then
consider i such that
A16: x
= (fl
. i) and
A17: 1
<= i and
A18: i
<= (
len fl) and (fl
. i)
in (
bound_QC-variables A);
i
in (
dom l) by
A10,
A17,
A18,
FINSEQ_3: 25;
then
A19: (fl
. i)
= (f
. (l
. i)) by
FUNCT_1: 13;
A20: (l
. i)
in (
bound_QC-variables A) by
A10,
A17,
A18,
Th13;
then
A21: (l
. i)
in (
dom f) by
FUNCT_2:def 1;
(l
. i)
in { (l
. j) : 1
<= j & j
<= (
len l) & (l
. j)
in (
bound_QC-variables A) } by
A10,
A17,
A18,
A20;
hence thesis by
A16,
A21,
A19,
FUNCT_1:def 6;
end;
A22: (f
.: (
still_not-bound_in (P
! l)))
= (f
.: (
still_not-bound_in l)) by
QC_LANG3: 5
.= (f
.: (
variables_in (l,(
bound_QC-variables A)))) by
QC_LANG3: 2
.= (
variables_in (fl,(
bound_QC-variables A))) by
A9
.= (
still_not-bound_in fl) by
QC_LANG3: 2
.= (
still_not-bound_in (P
! fl)) by
QC_LANG3: 5;
((
ATOMIC (P,l))
. (u,f))
= (P
! (f
* l)) by
Def5;
hence thesis by
A22,
Def7;
end;
end;
A23:
now
let r, x such that
A24:
P[r];
thus
P[(
All (x,r))]
proof
reconsider g = ((
SepFunc A)
. r) as
Function of
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):], (
CQC-WFF A);
let u, K, f such that
A25:
[(
All (x,r)), u, K, f]
in (
SepQuadruples p);
A26:
[r, (u
++ ), (K
\/
{.x.}), (f
+* (x
.--> (
x. u)))]
in (
SepQuadruples p) by
A25,
Th33;
(f
+* (x
.--> (
x. u))) is
Function of (
bound_QC-variables A), (
bound_QC-variables A) by
Lm1;
then
reconsider fu = (f
+* (x
.--> (
x. u))) as
Element of (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))) by
FUNCT_2: 8;
reconsider r99 = (g
. ((u
++ ),fu)) as
Element of (
CQC-WFF A);
A27: ((
UNIVERSAL (x,g))
. (u,f))
= (
All ((
x. u),r99)) by
Def4;
A28: (
still_not-bound_in (
All (x,r)))
= ((
still_not-bound_in r)
\
{x}) by
QC_LANG3: 12;
then
A29: not (
x. u)
in (f
.: ((
still_not-bound_in r)
\
{x})) by
A25,
Th43;
thus (f
.: (
still_not-bound_in (
All (x,r))))
= (fu
.: ((
still_not-bound_in r)
\
{x})) by
A28,
Th3
.= ((fu
.: (
still_not-bound_in r))
\
{(
x. u)}) by
A29,
Th4
.= ((
still_not-bound_in r99)
\
{(
x. u)}) by
A24,
A26
.= (
still_not-bound_in (
All ((
x. u),r99))) by
QC_LANG3: 12
.= (
still_not-bound_in (((
SepFunc A)
. (
All (x,r))) qua
Element of (
Funcs (
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):],(
CQC-WFF A)))
.
[u, f] qua
Element of
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):]) qua
Element of (
CQC-WFF A)) by
A27,
Def7;
end;
end;
A30:
now
let r, s such that
A31:
P[r] and
A32:
P[s];
thus
P[(r
'&' s)]
proof
reconsider g = ((
SepFunc A)
. r), h = ((
SepFunc A)
. s) as
Function of
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):], (
CQC-WFF A);
let u, K, f such that
A33:
[(r
'&' s), u, K, f]
in (
SepQuadruples p);
reconsider r9 = (g
. (u,f)), s9 = (h
. ((u
+ (
QuantNbr r)),f)) as
Element of (
CQC-WFF A);
A34: ((
CON (g,h,(
QuantNbr r)))
. (u,f))
= (r9
'&' s9) by
Def3;
[r, u, K, f]
in (
SepQuadruples p) by
A33,
Th32;
then
A35: (f
.: (
still_not-bound_in r))
= (
still_not-bound_in r9) by
A31;
[s, (u
+ (
QuantNbr r)), K, f]
in (
SepQuadruples p) by
A33,
Th32;
then
A36: (f
.: (
still_not-bound_in s))
= (
still_not-bound_in s9) by
A32;
thus (f
.: (
still_not-bound_in (r
'&' s)))
= (f
.: ((
still_not-bound_in r)
\/ (
still_not-bound_in s))) by
QC_LANG3: 10
.= ((
still_not-bound_in r9)
\/ (
still_not-bound_in s9)) by
A35,
A36,
RELAT_1: 120
.= (
still_not-bound_in (r9
'&' s9)) by
QC_LANG3: 10
.= (
still_not-bound_in (((
SepFunc A)
. (r
'&' s)) qua
Element of (
Funcs (
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):],(
CQC-WFF A)))
.
[u, f] qua
Element of
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):]) qua
Element of (
CQC-WFF A)) by
A34,
Def7;
end;
end;
A37: ((
SepFunc A)
. (
VERUM A))
= (
[:(
QC-symbols A), (
Funcs ((
bound_QC-variables A),(
bound_QC-variables A))):]
--> (
VERUM A)) by
Def7;
A38:
P[(
VERUM A)]
proof
let v, K, f such that
[(
VERUM A), v, K, f]
in (
SepQuadruples p);
A39: (
still_not-bound_in (
VERUM A))
=
{} by
QC_LANG3: 3;
thus thesis by
A39,
A37;
end;
A40: for q holds
P[q] from
CQCInd(
A38,
A8,
A2,
A30,
A23);
thus (
still_not-bound_in p)
= ((
id (
bound_QC-variables A))
.: (
still_not-bound_in p)) by
FUNCT_1: 92
.= (
still_not-bound_in (
SepVar p)) by
A40,
A1;
end;
theorem ::
CQC_SIM1:45
(
index p)
= (
index (
SepVar p))
proof
(
still_not-bound_in p)
= (
still_not-bound_in (
SepVar p)) by
Th44;
hence thesis;
end;
definition
let A;
let p, q;
::
CQC_SIM1:def14
pred p,q
are_similar means (
SepVar p)
= (
SepVar q);
reflexivity ;
symmetry ;
end
theorem ::
CQC_SIM1:46
(p,q)
are_similar & (q,r)
are_similar implies (p,r)
are_similar ;