let A be non empty set ; :: thesis:
let x, y be bound_QC-variable; :: thesis:
let p, q be Element of CQC-WFF ; :: thesis:
let J be interpretation of A; :: thesis:
let s9 be QC-formula; :: thesis:
defpred S₁[ Element of QC-WFF ] means for x, y being bound_QC-variable
for p, q being Element of CQC-WFF st x <> y & p = $1 . x & q = $1 . y holds
for v being Element of Valuations_in A st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v;

A1: now

let s be Element of QC-WFF ; :: thesis:
thus ( s is atomic implies S₁[s] ) :: thesis:

proof

assume A2: s is atomic ; :: thesis:
thus for x, y being bound_QC-variable
for p, q being Element of CQC-WFF st x <> y & p = s . x & q = s . y holds
for v being Element of Valuations_in A st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v :: thesis:

proof

consider k being Element of NAT , P being QC-pred_symbol of k, l being QC-variable_list of k such that
A3: s = P ! l by A2, QC_LANG1:def 17;
let x, y be bound_QC-variable; :: thesis:
let p, q be Element of CQC-WFF ; :: thesis:
assume that
x <> y and
A4: p = s . x and
A5: q = s . y ; :: thesis:
set lx = Subst (l,((a. 0) .--> x));
set ly = Subst (l,((a. 0) .--> y));
let v be Element of Valuations_in A; :: thesis:
assume A6: v . x = v . y ; :: thesis:
A7: p = P ! (Subst (l,((a. 0) .--> x))) by A4, A3, CQC_LANG:30;
then A8: { ((Subst (l,((a. 0) .--> x))) . i) where i is Element of NAT : ( 1 <= i & i <= len (Subst (l,((a. 0) .--> x))) & (Subst (l,((a. 0) .--> x))) . i in free_QC-variables ) } = {} by CQC_LANG:17;
A9: q = P ! (Subst (l,((a. 0) .--> y))) by A5, A3, CQC_LANG:30;
then A10: { ((Subst (l,((a. 0) .--> y))) . i) where i is Element of NAT : ( 1 <= i & i <= len (Subst (l,((a. 0) .--> y))) & (Subst (l,((a. 0) .--> y))) . i in free_QC-variables ) } = {} by CQC_LANG:17;
A11: { ((Subst (l,((a. 0) .--> y))) . j) where j is Element of NAT : ( 1 <= j & j <= len (Subst (l,((a. 0) .--> y))) & (Subst (l,((a. 0) .--> y))) . j in fixed_QC-variables ) } = {} by A9, CQC_LANG:17;
{ ((Subst (l,((a. 0) .--> x))) . j) where j is Element of NAT : ( 1 <= j & j <= len (Subst (l,((a. 0) .--> x))) & (Subst (l,((a. 0) .--> x))) . j in fixed_QC-variables ) } = {} by A7, CQC_LANG:17;
then reconsider lx = Subst (l,((a. 0) .--> x)), ly = Subst (l,((a. 0) .--> y)) as CQC-variable_list of k by A8, A10, A11, CQC_LANG:15;
A12: len (v *' lx) = k by Def8;

A13: now

let i be Nat; :: thesis:
assume that
A14: 1 <= i and
A15: i <= len (v *' lx) ; :: thesis:
A16: i in NAT by ORDINAL1:def 13;
A17: i <= len l by A12, A15, FINSEQ_1:def 18;

A18: now

assume l . i <> a. 0 ; :: thesis:
then A19: ( lx . i = l . i & ly . i = l . i ) by A14, A17, A16, CQC_LANG:11;
v . (lx . i) = (v *' lx) . i by A12, A14, A15, Def8;
hence (v *' lx) . i = (v *' ly) . i by A12, A14, A15, A19, Def8; :: thesis:

end;

now

assume l . i = a. 0 ; :: thesis:
then A20: ( lx . i = x & ly . i = y ) by A14, A17, A16, CQC_LANG:11;
v . (lx . i) = (v *' lx) . i by A12, A14, A15, Def8;
hence (v *' lx) . i = (v *' ly) . i by A6, A12, A14, A15, A20, Def8; :: thesis:

end;

hence (v *' lx) . i = (v *' ly) . i by A18; :: thesis:

end;

len (v *' ly) = k by Def8;
then A21: v *' lx = v *' ly by A12, A13, FINSEQ_1:18;

A22: now

assume (Valid (p,J)) . v = FALSE ; :: thesis:
then not v *' lx in J . P by A7, Th17;
hence (Valid (q,J)) . v = FALSE by A9, A21, Th17; :: thesis:

end;

now

assume (Valid (p,J)) . v = TRUE ; :: thesis:
then v *' lx in J . P by A7, Th16;
hence (Valid (q,J)) . v = TRUE by A9, A21, Th16; :: thesis:

end;

hence (Valid (p,J)) . v = (Valid (q,J)) . v by A22, XBOOLEAN:def 3; :: thesis:

end;

thus S₁[ VERUM ] :: thesis:

proof

let x, y be bound_QC-variable; :: thesis:
let p, q be Element of CQC-WFF ; :: thesis:
assume that
x <> y and
A23: p = VERUM . x and
A24: q = VERUM . y ; :: thesis:
let v be Element of Valuations_in A; :: thesis:
assume v . x = v . y ; :: thesis:
p = VERUM by A23, CQC_LANG:28;
hence (Valid (p,J)) . v = (Valid (q,J)) . v by A24, CQC_LANG:28; :: thesis:

end;

thus ( s is negative & S₁[ the_argument_of s] implies S₁[s] ) :: thesis:

proof

assume that
A25: s is negative and
A26: for x, y being bound_QC-variable
for p, q being Element of CQC-WFF st x <> y & p = (the_argument_of s) . x & q = (the_argument_of s) . y holds
for v being Element of Valuations_in A st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v ; :: thesis:
thus for x, y being bound_QC-variable
for p, q being Element of CQC-WFF st x <> y & p = s . x & q = s . y holds
for v being Element of Valuations_in A st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v :: thesis:

proof

let x, y be bound_QC-variable; :: thesis:
let p, q be Element of CQC-WFF ; :: thesis:
assume that
x <> y and
A27: p = s . x and
A28: q = s . y ; :: thesis:
A29: s . y = 'not' ((the_argument_of s) . y) by A25, CQC_LANG:31;
then reconsider qa = (the_argument_of s) . y as Element of CQC-WFF by A28, CQC_LANG:18;
A30: s . x = 'not' ((the_argument_of s) . x) by A25, CQC_LANG:31;
then reconsider pa = (the_argument_of s) . x as Element of CQC-WFF by A27, CQC_LANG:18;
let v be Element of Valuations_in A; :: thesis:
assume A31: v . x = v . y ; :: thesis:

A32: now

assume (Valid (p,J)) . v = FALSE ; :: thesis:
then 'not' ((Valid (pa,J)) . v) = FALSE by A27, A30, Th20;
then (Valid (pa,J)) . v = TRUE by MARGREL1:41;
then (Valid (qa,J)) . v = TRUE by A26, A31;
then 'not' ((Valid (qa,J)) . v) = FALSE by MARGREL1:41;
hence (Valid (q,J)) . v = FALSE by A28, A29, Th20; :: thesis:

end;

now

assume (Valid (p,J)) . v = TRUE ; :: thesis:
then 'not' ((Valid (pa,J)) . v) = TRUE by A27, A30, Th20;
then (Valid (pa,J)) . v = FALSE by MARGREL1:41;
then (Valid (qa,J)) . v = FALSE by A26, A31;
then 'not' ((Valid (qa,J)) . v) = TRUE by MARGREL1:41;
hence (Valid (q,J)) . v = TRUE by A28, A29, Th20; :: thesis:

end;

hence (Valid (p,J)) . v = (Valid (q,J)) . v by A32, XBOOLEAN:def 3; :: thesis:

end;

thus ( s is conjunctive & S₁[ the_left_argument_of s] & S₁[ the_right_argument_of s] implies S₁[s] ) :: thesis:

proof

assume that
A33: s is conjunctive and
A34: for x, y being bound_QC-variable
for p, q being Element of CQC-WFF st x <> y & p = (the_left_argument_of s) . x & q = (the_left_argument_of s) . y holds
for v being Element of Valuations_in A st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v and
A35: for x, y being bound_QC-variable
for p, q being Element of CQC-WFF st x <> y & p = (the_right_argument_of s) . x & q = (the_right_argument_of s) . y holds
for v being Element of Valuations_in A st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v ; :: thesis:
thus for x, y being bound_QC-variable
for p, q being Element of CQC-WFF st x <> y & p = s . x & q = s . y holds
for v being Element of Valuations_in A st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v :: thesis:

proof

let x, y be bound_QC-variable; :: thesis:
let p, q be Element of CQC-WFF ; :: thesis:
assume that
x <> y and
A36: p = s . x and
A37: q = s . y ; :: thesis:
A38: s . x = ((the_left_argument_of s) . x) '&' ((the_right_argument_of s) . x) by A33, CQC_LANG:33;
then reconsider pla = (the_left_argument_of s) . x, pra = (the_right_argument_of s) . x as Element of CQC-WFF by A36, CQC_LANG:19;
A39: s . y = ((the_left_argument_of s) . y) '&' ((the_right_argument_of s) . y) by A33, CQC_LANG:33;
then reconsider qla = (the_left_argument_of s) . y, qra = (the_right_argument_of s) . y as Element of CQC-WFF by A37, CQC_LANG:19;
let v be Element of Valuations_in A; :: thesis:
assume A40: v . x = v . y ; :: thesis:

A41: now

assume A42: (Valid (p,J)) . v = FALSE ; :: thesis:

A43: now

assume (Valid (pla,J)) . v = FALSE ; :: thesis:
then (Valid (qla,J)) . v = FALSE by A34, A40;
then ((Valid (qla,J)) . v) '&' ((Valid (qra,J)) . v) = FALSE by MARGREL1:45;
hence (Valid (p,J)) . v = (Valid (q,J)) . v by A37, A39, A42, Th22; :: thesis:

end;

A44: now

assume (Valid (pra,J)) . v = FALSE ; :: thesis:
then (Valid (qra,J)) . v = FALSE by A35, A40;
then ((Valid (qla,J)) . v) '&' ((Valid (qra,J)) . v) = FALSE by MARGREL1:45;
hence (Valid (p,J)) . v = (Valid (q,J)) . v by A37, A39, A42, Th22; :: thesis:

end;

((Valid (pla,J)) . v) '&' ((Valid (pra,J)) . v) = FALSE by A36, A38, A42, Th22;
hence (Valid (p,J)) . v = (Valid (q,J)) . v by A43, A44, MARGREL1:45; :: thesis:

end;

now

assume (Valid (p,J)) . v = TRUE ; :: thesis:
then A45: ((Valid (pla,J)) . v) '&' ((Valid (pra,J)) . v) = TRUE by A36, A38, Th22;
then (Valid (pra,J)) . v = TRUE by MARGREL1:45;
then A46: (Valid (qra,J)) . v = TRUE by A35, A40;
(Valid (pla,J)) . v = TRUE by A45, MARGREL1:45;
then (Valid (qla,J)) . v = TRUE by A34, A40;
then ((Valid (qla,J)) . v) '&' ((Valid (qra,J)) . v) = TRUE by A46;
hence (Valid (q,J)) . v = TRUE by A37, A39, Th22; :: thesis:

end;

hence (Valid (p,J)) . v = (Valid (q,J)) . v by A41, XBOOLEAN:def 3; :: thesis:

end;

thus ( s is universal & S₁[ the_scope_of s] implies S₁[s] ) :: thesis:

proof

assume that
A47: s is universal and
A48: for x, y being bound_QC-variable
for p, q being Element of CQC-WFF st x <> y & p = (the_scope_of s) . x & q = (the_scope_of s) . y holds
for v being Element of Valuations_in A st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v ; :: thesis:
consider xx being bound_QC-variable, pp being Element of QC-WFF such that
A49: s = All (xx,pp) by A47, QC_LANG1:def 20;
A50: xx = bound_in s by A47, A49, QC_LANG1:def 26;
thus for x, y being bound_QC-variable
for p, q being Element of CQC-WFF st x <> y & p = s . x & q = s . y holds
for v being Element of Valuations_in A st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v :: thesis:

proof

let x, y be bound_QC-variable; :: thesis:
let p, q be Element of CQC-WFF ; :: thesis:
assume that
x <> y and
A51: p = s . x and
A52: q = s . y ; :: thesis:
let v be Element of Valuations_in A; :: thesis:
assume A53: v . x = v . y ; :: thesis:

A54: now

assume A55: x <> bound_in s ; :: thesis:
then s . x = All ((bound_in s),((the_scope_of s) . x)) by A47, CQC_LANG:36;
then reconsider ps = (the_scope_of s) . x as Element of CQC-WFF by A51, CQC_LANG:23;
A56: All ((bound_in s),ps) = p by A47, A51, A55, CQC_LANG:36;

A57: now

assume A58: y <> bound_in s ; :: thesis:
then s . y = All ((bound_in s),((the_scope_of s) . y)) by A47, CQC_LANG:36;
then reconsider qs = (the_scope_of s) . y as Element of CQC-WFF by A52, CQC_LANG:23;
A59: Valid ((All ((bound_in s),qs)),J) = FOR_ALL ((bound_in s),(Valid (qs,J))) by Lm1;
A60: Valid ((All ((bound_in s),ps)),J) = FOR_ALL ((bound_in s),(Valid (ps,J))) by Lm1;
A61: All ((bound_in s),qs) = q by A47, A52, A58, CQC_LANG:36;

A62: now

assume A63: (Valid (p,J)) . v = TRUE ; :: thesis:
for v1 being Element of Valuations_in A st ( for y being bound_QC-variable st bound_in s <> y holds
v1 . y = v . y ) holds
(Valid (qs,J)) . v1 = TRUE

proof

let v1 be Element of Valuations_in A; :: thesis:
assume A64: for y being bound_QC-variable st bound_in s <> y holds
v1 . y = v . y ; :: thesis:
then A65: ( v1 . x = v . x & v1 . y = v . y ) by A55, A58;
(Valid (ps,J)) . v1 = TRUE by A56, A60, A63, A64, Th8;
hence (Valid (qs,J)) . v1 = TRUE by A48, A53, A65; :: thesis:

end;

hence (Valid (q,J)) . v = TRUE by A61, A59, Th8; :: thesis:

end;

now

assume A66: (Valid (p,J)) . v = FALSE ; :: thesis:
ex v1 being Element of Valuations_in A st
( (Valid (qs,J)) . v1 = FALSE & ( for y being bound_QC-variable st bound_in s <> y holds
v1 . y = v . y ) )

proof

consider v1 being Element of Valuations_in A such that
A67: (Valid (ps,J)) . v1 = FALSE and
A68: for y being bound_QC-variable st bound_in s <> y holds
v1 . y = v . y by A56, A60, A66, Th7;
( v1 . x = v . x & v1 . y = v . y ) by A55, A58, A68;
then (Valid (qs,J)) . v1 = FALSE by A48, A53, A67;
hence ex v1 being Element of Valuations_in A st
( (Valid (qs,J)) . v1 = FALSE & ( for y being bound_QC-variable st bound_in s <> y holds
v1 . y = v . y ) ) by A68; :: thesis:

end;

hence (Valid (q,J)) . v = FALSE by A61, A59, Th7; :: thesis:

end;

hence (Valid (p,J)) . v = (Valid (q,J)) . v by A62, XBOOLEAN:def 3; :: thesis:

end;

now

assume A69: y = bound_in s ; :: thesis:
then q = All (y,pp) by A49, A50, A52, CQC_LANG:37;
hence (Valid (p,J)) . v = (Valid (q,J)) . v by A49, A50, A51, A69, CQC_LANG:40; :: thesis:

end;

hence (Valid (p,J)) . v = (Valid (q,J)) . v by A57; :: thesis:

end;

now

assume A70: x = bound_in s ; :: thesis:
then p = All (x,pp) by A49, A50, A51, CQC_LANG:37;
hence (Valid (p,J)) . v = (Valid (q,J)) . v by A49, A50, A52, A70, CQC_LANG:40; :: thesis:

end;

hence (Valid (p,J)) . v = (Valid (q,J)) . v by A54; :: thesis:

end;

for s being Element of QC-WFF holds S₁[s] from QC_LANG1:sch 2(A1);
hence ( x <> y & p = s9 . x & q = s9 . y implies for v being Element of Valuations_in A st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v ) ; :: thesis: