let A be non empty set ; :: thesis: for x, y being bound_QC-variable
for p, q being Element of CQC-WFF
for J being interpretation of A
for s9 being QC-formula st x <> y & p = s9 . x & q = s9 . y holds
for v being Element of Valuations_in A st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v
let x, y be bound_QC-variable; :: thesis: for p, q being Element of CQC-WFF
for J being interpretation of A
for s9 being QC-formula st x <> y & p = s9 . x & q = s9 . y holds
for v being Element of Valuations_in A st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v
let p, q be Element of CQC-WFF ; :: thesis: for J being interpretation of A
for s9 being QC-formula st x <> y & p = s9 . x & q = s9 . y holds
for v being Element of Valuations_in A st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v
let J be interpretation of A; :: thesis: for s9 being QC-formula st x <> y & p = s9 . x & q = s9 . y holds
for v being Element of Valuations_in A st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v
let s9 be QC-formula; :: thesis: ( 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 )
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: ( ( s is atomic implies S₁[s] ) & S₁[ VERUM ] & ( s is negative & S₁[ the_argument_of s] implies S₁[s] ) & ( s is conjunctive & S₁[ the_left_argument_of s] & S₁[ the_right_argument_of s] implies S₁[s] ) & ( s is universal & S₁[ the_scope_of s] implies S₁[s] ) )
thus ( s is atomic implies S₁[s] ) :: thesis: ( S₁[ VERUM ] & ( s is negative & S₁[ the_argument_of s] implies S₁[s] ) & ( s is conjunctive & S₁[ the_left_argument_of s] & S₁[ the_right_argument_of s] implies S₁[s] ) & ( s is universal & S₁[ the_scope_of s] implies S₁[s] ) )

proof

assume A2: s is atomic ; :: thesis: S₁[s]
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: verum

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 16;
let x, y be bound_QC-variable; :: thesis: 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
let p, q be Element of CQC-WFF ; :: thesis: ( x <> y & p = s . x & q = s . y implies for v being Element of Valuations_in A st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v )
assume that
x <> y and
A4: p = s . x and
A5: q = s . y ; :: thesis: for v being Element of Valuations_in A st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v
set lx = Subst (l,((a. 0) .--> x));
set ly = Subst (l,((a. 0) .--> y));
let v be Element of Valuations_in A; :: thesis: ( v . x = v . y implies (Valid (p,J)) . v = (Valid (q,J)) . v )
assume A6: v . x = v . y ; :: thesis: (Valid (p,J)) . v = (Valid (q,J)) . v
A7: p = P ! (Subst (l,((a. 0) .--> x))) by A4, A3, CQC_LANG:17;
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:7;
A9: q = P ! (Subst (l,((a. 0) .--> y))) by A5, A3, CQC_LANG:17;
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:7;
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:7;
{ ((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:7;
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:5;
A12: len (v *' lx) = k by Def8;

A13: now

let i be Nat; :: thesis: ( 1 <= i & i <= len (v *' lx) implies (v *' lx) . i = (v *' ly) . i )
assume that
A14: 1 <= i and
A15: i <= len (v *' lx) ; :: thesis: (v *' lx) . i = (v *' ly) . i
A16: i in NAT by ORDINAL1:def 12;
A17: i <= len l by A12, A15, CARD_1:def 7;

A18: now

assume l . i <> a. 0 ; :: thesis: (v *' lx) . i = (v *' ly) . i
then A19: ( lx . i = l . i & ly . i = l . i ) by A14, A17, A16, CQC_LANG:3;
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: verum

end;

now

assume l . i = a. 0 ; :: thesis: (v *' lx) . i = (v *' ly) . i
then A20: ( lx . i = x & ly . i = y ) by A14, A17, A16, CQC_LANG:3;
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: verum

end;

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

end;

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

A22: now

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

end;

now

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

end;

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

end;

end;

thus S₁[ VERUM ] :: thesis: ( ( s is negative & S₁[ the_argument_of s] implies S₁[s] ) & ( s is conjunctive & S₁[ the_left_argument_of s] & S₁[ the_right_argument_of s] implies S₁[s] ) & ( s is universal & S₁[ the_scope_of s] implies S₁[s] ) )

proof

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

end;

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

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: S₁[s]
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: verum

proof

let x, y be bound_QC-variable; :: thesis: 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
let p, q be Element of CQC-WFF ; :: thesis: ( x <> y & p = s . x & q = s . y implies for v being Element of Valuations_in A st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v )
assume that
x <> y and
A27: p = s . x and
A28: q = s . y ; :: thesis: for v being Element of Valuations_in A st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v
A29: s . y = 'not' ((the_argument_of s) . y) by A25, CQC_LANG:18;
then reconsider qa = (the_argument_of s) . y as Element of CQC-WFF by A28, CQC_LANG:8;
A30: s . x = 'not' ((the_argument_of s) . x) by A25, CQC_LANG:18;
then reconsider pa = (the_argument_of s) . x as Element of CQC-WFF by A27, CQC_LANG:8;
let v be Element of Valuations_in A; :: thesis: ( v . x = v . y implies (Valid (p,J)) . v = (Valid (q,J)) . v )
assume A31: v . x = v . y ; :: thesis: (Valid (p,J)) . v = (Valid (q,J)) . v

A32: now

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

end;

now

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

end;

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

end;

end;

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

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: S₁[s]
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: verum

proof

let x, y be bound_QC-variable; :: thesis: 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
let p, q be Element of CQC-WFF ; :: thesis: ( x <> y & p = s . x & q = s . y implies for v being Element of Valuations_in A st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v )
assume that
x <> y and
A36: p = s . x and
A37: q = s . y ; :: thesis: for v being Element of Valuations_in A st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v
A38: s . x = ((the_left_argument_of s) . x) '&' ((the_right_argument_of s) . x) by A33, CQC_LANG:20;
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:9;
A39: s . y = ((the_left_argument_of s) . y) '&' ((the_right_argument_of s) . y) by A33, CQC_LANG:20;
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:9;
let v be Element of Valuations_in A; :: thesis: ( v . x = v . y implies (Valid (p,J)) . v = (Valid (q,J)) . v )
assume A40: v . x = v . y ; :: thesis: (Valid (p,J)) . v = (Valid (q,J)) . v

A41: now

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

A43: now

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

end;

A44: now

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

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:12; :: thesis: verum

end;

now

assume (Valid (p,J)) . v = TRUE ; :: thesis: (Valid (q,J)) . v = TRUE
then A45: ((Valid (pla,J)) . v) '&' ((Valid (pra,J)) . v) = TRUE by A36, A38, Th22;
then (Valid (pra,J)) . v = TRUE by MARGREL1:12;
then A46: (Valid (qra,J)) . v = TRUE by A35, A40;
(Valid (pla,J)) . v = TRUE by A45, MARGREL1:12;
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: verum

end;

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

end;

end;

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

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: S₁[s]
consider xx being bound_QC-variable, pp being Element of QC-WFF such that
A49: s = All (xx,pp) by A47, QC_LANG1:def 19;
A50: xx = bound_in s by A47, A49, QC_LANG1:def 25;
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: verum

proof

let x, y be bound_QC-variable; :: thesis: 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
let p, q be Element of CQC-WFF ; :: thesis: ( x <> y & p = s . x & q = s . y implies for v being Element of Valuations_in A st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v )
assume that
x <> y and
A51: p = s . x and
A52: q = s . y ; :: thesis: for v being Element of Valuations_in A st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v
let v be Element of Valuations_in A; :: thesis: ( v . x = v . y implies (Valid (p,J)) . v = (Valid (q,J)) . v )
assume A53: v . x = v . y ; :: thesis: (Valid (p,J)) . v = (Valid (q,J)) . v

A54: now

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

A57: now

assume A58: y <> bound_in s ; :: thesis: (Valid (p,J)) . v = (Valid (q,J)) . v
then s . y = All ((bound_in s),((the_scope_of s) . y)) by A47, CQC_LANG:23;
then reconsider qs = (the_scope_of s) . y as Element of CQC-WFF by A52, CQC_LANG:13;
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:23;

A62: now

assume A63: (Valid (p,J)) . v = TRUE ; :: thesis: (Valid (q,J)) . v = TRUE
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: ( ( for y being bound_QC-variable st bound_in s <> y holds
v1 . y = v . y ) implies (Valid (qs,J)) . v1 = TRUE )
assume A64: for y being bound_QC-variable st bound_in s <> y holds
v1 . y = v . y ; :: thesis: (Valid (qs,J)) . v1 = TRUE
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: verum

end;

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

end;

now

assume A66: (Valid (p,J)) . v = FALSE ; :: thesis: (Valid (q,J)) . v = FALSE
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: verum

end;

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

end;

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

end;

now

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

end;

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

end;

now

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

end;

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

end;

end;

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: verum