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

A1: now :: thesis:

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

proof

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

proof

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

A13: now :: thesis:

let i be Nat; :: thesis:
assume that
A14: 1 <= i and
A15: i <= len (v *' lx) ; :: thesis:
A16: i <= len l by A12, A15, CARD_1:def 7;

A17: now :: thesis:

assume l . i <> Al a. 0 ; :: thesis:
then A18: ( lx . i = l . i & ly . i = l . i ) by A14, A16, CQC_LANG:3;
v . (lx . i) = (v *' lx) . i by A12, A14, A15, Def3;
hence (v *' lx) . i = (v *' ly) . i by A12, A14, A15, A18, Def3; :: thesis:

end;

now :: thesis:

assume l . i = Al a. 0 ; :: thesis:
then A19: ( lx . i = x & ly . i = y ) by A14, A16, CQC_LANG:3;
v . (lx . i) = (v *' lx) . i by A12, A14, A15, Def3;
hence (v *' lx) . i = (v *' ly) . i by A6, A12, A14, A15, A19, Def3; :: thesis:

end;

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

end;

len (v *' ly) = k by Def3;
then A20: v *' lx = v *' ly by A12, A13, FINSEQ_1:14;

A21: now :: thesis:

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

end;

now :: thesis:

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

end;

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

end;

thus S₁[ VERUM Al] :: thesis:

proof

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

end;

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

proof

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

proof

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

A31: now :: thesis:

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

end;

now :: thesis:

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

end;

hence (Valid (p,J)) . v = (Valid (q,J)) . v by A31, 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
A32: s is conjunctive and
A33: for x, y being bound_QC-variable of Al
for p, q being Element of CQC-WFF Al 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 (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v and
A34: for x, y being bound_QC-variable of Al
for p, q being Element of CQC-WFF Al 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 (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v ; :: thesis:
thus for x, y being bound_QC-variable of Al
for p, q being Element of CQC-WFF Al st x <> y & p = s . x & q = s . y holds
for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v :: thesis:

proof

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

A40: now :: thesis:

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

A42: now :: thesis:

assume (Valid (pla,J)) . v = FALSE ; :: thesis:
then (Valid (qla,J)) . v = FALSE by A33, A39;
then ((Valid (qla,J)) . v) '&' ((Valid (qra,J)) . v) = FALSE by MARGREL1:12;
hence (Valid (p,J)) . v = (Valid (q,J)) . v by A36, A38, A41, Th12; :: thesis:

end;

A43: now :: thesis:

assume (Valid (pra,J)) . v = FALSE ; :: thesis:
then (Valid (qra,J)) . v = FALSE by A34, A39;
then ((Valid (qla,J)) . v) '&' ((Valid (qra,J)) . v) = FALSE by MARGREL1:12;
hence (Valid (p,J)) . v = (Valid (q,J)) . v by A36, A38, A41, Th12; :: thesis:

end;

((Valid (pla,J)) . v) '&' ((Valid (pra,J)) . v) = FALSE by A35, A37, A41, Th12;
hence (Valid (p,J)) . v = (Valid (q,J)) . v by A42, A43, MARGREL1:12; :: thesis:

end;

now :: thesis:

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

end;

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

end;

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

proof

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

proof

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

A53: now :: thesis:

assume A54: x <> bound_in s ; :: thesis:
then s . x = All ((bound_in s),((the_scope_of s) . x)) by A46, CQC_LANG:23;
then reconsider ps = (the_scope_of s) . x as Element of CQC-WFF Al by A50, CQC_LANG:13;
A55: All ((bound_in s),ps) = p by A46, A50, A54, CQC_LANG:23;

A56: now :: thesis:

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

A61: now :: thesis:

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

proof

let v1 be Element of Valuations_in (Al,A); :: thesis:
assume A63: for y being bound_QC-variable of Al st bound_in s <> y holds
v1 . y = v . y ; :: thesis:
then A64: ( v1 . x = v . x & v1 . y = v . y ) by A54, A57;
(Valid (ps,J)) . v1 = TRUE by A55, A59, A62, A63, Th3;
hence (Valid (qs,J)) . v1 = TRUE by A47, A52, A64; :: thesis:

end;

hence (Valid (q,J)) . v = TRUE by A60, A58, Th3; :: thesis:

end;

now :: thesis:

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

proof

consider v1 being Element of Valuations_in (Al,A) such that
A66: (Valid (ps,J)) . v1 = FALSE and
A67: for y being bound_QC-variable of Al st bound_in s <> y holds
v1 . y = v . y by A55, A59, A65, Th2;
( v1 . x = v . x & v1 . y = v . y ) by A54, A57, A67;
then (Valid (qs,J)) . v1 = FALSE by A47, A52, A66;
hence ex v1 being Element of Valuations_in (Al,A) st
( (Valid (qs,J)) . v1 = FALSE & ( for y being bound_QC-variable of Al st bound_in s <> y holds
v1 . y = v . y ) ) by A67; :: thesis:

end;

hence (Valid (q,J)) . v = FALSE by A60, A58, Th2; :: thesis:

end;

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

end;

now :: thesis:

assume A68: y = bound_in s ; :: thesis:
then q = All (y,pp) by A48, A49, A51, CQC_LANG:24;
hence (Valid (p,J)) . v = (Valid (q,J)) . v by A48, A49, A50, A68, CQC_LANG:27; :: thesis:

end;

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

end;

now :: thesis:

assume A69: x = bound_in s ; :: thesis:
then p = All (x,pp) by A48, A49, A50, CQC_LANG:24;
hence (Valid (p,J)) . v = (Valid (q,J)) . v by A48, A49, A51, A69, CQC_LANG:27; :: thesis:

end;

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

end;

for s being Element of QC-WFF Al 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 (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v ) ; :: thesis: