let A be non empty set ; :: thesis: for x being bound_QC-variable
for p being Element of CQC-WFF
for J being interpretation of A st not x in still_not-bound_in p holds
for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid p,J) . v = (Valid p,J) . w
let x be bound_QC-variable; :: thesis: for p being Element of CQC-WFF
for J being interpretation of A st not x in still_not-bound_in p holds
for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid p,J) . v = (Valid p,J) . w
let p be Element of CQC-WFF ; :: thesis: for J being interpretation of A st not x in still_not-bound_in p holds
for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid p,J) . v = (Valid p,J) . w
let J be interpretation of A; :: thesis: ( not x in still_not-bound_in p implies for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid p,J) . v = (Valid p,J) . w )
defpred S₁[ Element of CQC-WFF ] means ( not x in still_not-bound_in $1 implies for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid $1,J) . v = (Valid $1,J) . w );

A1: now

let s, t be Element of CQC-WFF ; :: thesis: for y being bound_QC-variable
for k being Element of NAT
for ll being CQC-variable_list of k
for P being QC-pred_symbol of k holds
( S₁[ VERUM ] & S₁[P ! ll] & ( S₁[s] implies S₁[ 'not' s] ) & ( S₁[s] & S₁[t] implies S₁[s '&' t] ) & ( S₁[s] implies S₁[ All y,s] ) )
let y be bound_QC-variable; :: thesis: for k being Element of NAT
for ll being CQC-variable_list of k
for P being QC-pred_symbol of k holds
( S₁[ VERUM ] & S₁[P ! ll] & ( S₁[s] implies S₁[ 'not' s] ) & ( S₁[s] & S₁[t] implies S₁[s '&' t] ) & ( S₁[s] implies S₁[ All y,s] ) )
let k be Element of NAT ; :: thesis: for ll being CQC-variable_list of k
for P being QC-pred_symbol of k holds
( S₁[ VERUM ] & S₁[P ! ll] & ( S₁[s] implies S₁[ 'not' s] ) & ( S₁[s] & S₁[t] implies S₁[s '&' t] ) & ( S₁[s] implies S₁[ All y,s] ) )
let ll be CQC-variable_list of k; :: thesis: for P being QC-pred_symbol of k holds
( S₁[ VERUM ] & S₁[P ! ll] & ( S₁[s] implies S₁[ 'not' s] ) & ( S₁[s] & S₁[t] implies S₁[s '&' t] ) & ( S₁[s] implies S₁[ All y,s] ) )
let P be QC-pred_symbol of k; :: thesis: ( S₁[ VERUM ] & S₁[P ! ll] & ( S₁[s] implies S₁[ 'not' s] ) & ( S₁[s] & S₁[t] implies S₁[s '&' t] ) & ( S₁[s] implies S₁[ All y,s] ) )
thus S₁[ VERUM ] :: thesis: ( S₁[P ! ll] & ( S₁[s] implies S₁[ 'not' s] ) & ( S₁[s] & S₁[t] implies S₁[s '&' t] ) & ( S₁[s] implies S₁[ All y,s] ) )

proof

assume not x in still_not-bound_in VERUM ; :: thesis: for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid VERUM ,J) . v = (Valid VERUM ,J) . w
thus for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid VERUM ,J) . v = (Valid VERUM ,J) . w :: thesis: verum

proof

let v, w be Element of Valuations_in A; :: thesis: ( ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) implies (Valid VERUM ,J) . v = (Valid VERUM ,J) . w )
assume for y being bound_QC-variable st x <> y holds
w . y = v . y ; :: thesis: (Valid VERUM ,J) . v = (Valid VERUM ,J) . w
(Valid VERUM ,J) . v = TRUE by Th14;
hence (Valid VERUM ,J) . v = (Valid VERUM ,J) . w by Th14; :: thesis: verum

end;

end;

A2: rng ll c= bound_QC-variables by RELAT_1:def 19;
thus S₁[P ! ll] :: thesis: ( ( S₁[s] implies S₁[ 'not' s] ) & ( S₁[s] & S₁[t] implies S₁[s '&' t] ) & ( S₁[s] implies S₁[ All y,s] ) )

proof

assume A3: not x in still_not-bound_in (P ! ll) ; :: thesis: for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid (P ! ll),J) . v = (Valid (P ! ll),J) . w
thus for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid (P ! ll),J) . v = (Valid (P ! ll),J) . w :: thesis: verum

proof

let v, w be Element of Valuations_in A; :: thesis: ( ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) implies (Valid (P ! ll),J) . v = (Valid (P ! ll),J) . w )
assume A4: for y being bound_QC-variable st x <> y holds
w . y = v . y ; :: thesis: (Valid (P ! ll),J) . v = (Valid (P ! ll),J) . w

A5: now

A6: len (v *' ll) = k by Def8;

A7: now

let i be Nat; :: thesis: ( 1 <= i & i <= len (v *' ll) implies (v *' ll) . i = (w *' ll) . i )
assume A8: ( 1 <= i & i <= len (v *' ll) ) ; :: thesis: (v *' ll) . i = (w *' ll) . i
A9: len (v *' ll) = len ll by A6, FINSEQ_1:def 18;
then i in dom ll by A8, FINSEQ_3:27;
then ll . i in rng ll by FUNCT_1:def 5;
then reconsider z = ll . i as bound_QC-variable by A2;
A10: i in NAT by ORDINAL1:def 13;
ll . i <> x

proof

reconsider M = still_not-bound_in ll as set ;
not x in M by A3, QC_LANG3:9;
then not x in variables_in ll,bound_QC-variables by QC_LANG3:6;
then not x in { (ll . i2) where i2 is Element of NAT : ( 1 <= i2 & i2 <= len ll & ll . i2 in bound_QC-variables ) } by QC_LANG3:def 2;
hence ll . i <> x by A8, A10, A9; :: thesis: verum

end;

then A11: w . z = v . z by A4;
(v *' ll) . i = v . (ll . i) by A6, A8, Def8;
hence (v *' ll) . i = (w *' ll) . i by A6, A8, A11, Def8; :: thesis: verum

end;

assume A12: (Valid (P ! ll),J) . v = TRUE ; :: thesis: (Valid (P ! ll),J) . v = (Valid (P ! ll),J) . w
then (ll 'in' (J . P)) . v = TRUE by Lm1;
then A13: v *' ll in J . P by Def9;
len (w *' ll) = k by Def8;
then w *' ll in J . P by A13, A6, A7, FINSEQ_1:18;
then (ll 'in' (J . P)) . w = TRUE by Def9;
hence (Valid (P ! ll),J) . v = (Valid (P ! ll),J) . w by A12, Lm1; :: thesis: verum

end;

now

A14: len (v *' ll) = k by Def8;

A15: now

let i be Nat; :: thesis: ( 1 <= i & i <= len (v *' ll) implies (v *' ll) . i = (w *' ll) . i )
assume A16: ( 1 <= i & i <= len (v *' ll) ) ; :: thesis: (v *' ll) . i = (w *' ll) . i
A17: len (v *' ll) = len ll by A14, FINSEQ_1:def 18;
then i in dom ll by A16, FINSEQ_3:27;
then ll . i in rng ll by FUNCT_1:def 5;
then reconsider z = ll . i as bound_QC-variable by A2;
ll . i <> x

proof

reconsider M = still_not-bound_in ll as set ;
not x in M by A3, QC_LANG3:9;
then not x in variables_in ll,bound_QC-variables by QC_LANG3:6;
then ( i in NAT & not x in { (ll . i2) where i2 is Element of NAT : ( 1 <= i2 & i2 <= len ll & ll . i2 in bound_QC-variables ) } ) by ORDINAL1:def 13, QC_LANG3:def 2;
hence ll . i <> x by A16, A17; :: thesis: verum

end;

then A18: w . z = v . z by A4;
(v *' ll) . i = v . (ll . i) by A14, A16, Def8;
hence (v *' ll) . i = (w *' ll) . i by A14, A16, A18, Def8; :: thesis: verum

end;

assume A19: (Valid (P ! ll),J) . v = FALSE ; :: thesis: (Valid (P ! ll),J) . v = (Valid (P ! ll),J) . w
then (ll 'in' (J . P)) . v = FALSE by Lm1;
then A20: not v *' ll in J . P by Def9;
len (w *' ll) = k by Def8;
then not w *' ll in J . P by A20, A14, A15, FINSEQ_1:18;
then (ll 'in' (J . P)) . w = FALSE by Def9;
hence (Valid (P ! ll),J) . v = (Valid (P ! ll),J) . w by A19, Lm1; :: thesis: verum

end;

hence (Valid (P ! ll),J) . v = (Valid (P ! ll),J) . w by A5, XBOOLEAN:def 3; :: thesis: verum

end;

end;

thus ( S₁[s] implies S₁[ 'not' s] ) :: thesis: ( ( S₁[s] & S₁[t] implies S₁[s '&' t] ) & ( S₁[s] implies S₁[ All y,s] ) )

proof

assume A21: ( ( not x in still_not-bound_in s implies for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid s,J) . v = (Valid s,J) . w ) & not x in still_not-bound_in ('not' s) ) ; :: thesis: for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid ('not' s),J) . v = (Valid ('not' s),J) . w
thus for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid ('not' s),J) . v = (Valid ('not' s),J) . w :: thesis: verum

proof

let v, w be Element of Valuations_in A; :: thesis: ( ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) implies (Valid ('not' s),J) . v = (Valid ('not' s),J) . w )
assume A22: for y being bound_QC-variable st x <> y holds
w . y = v . y ; :: thesis: (Valid ('not' s),J) . v = (Valid ('not' s),J) . w

A23: now

assume A24: (Valid ('not' s),J) . v = FALSE ; :: thesis: (Valid ('not' s),J) . v = (Valid ('not' s),J) . w
then 'not' ((Valid s,J) . v) = FALSE by Th20;
then (Valid s,J) . v = TRUE by MARGREL1:41;
then (Valid s,J) . w = TRUE by A21, A22, QC_LANG3:11;
then 'not' ((Valid s,J) . w) = FALSE by MARGREL1:41;
hence (Valid ('not' s),J) . v = (Valid ('not' s),J) . w by A24, Th20; :: thesis: verum

end;

now

assume A25: (Valid ('not' s),J) . v = TRUE ; :: thesis: (Valid ('not' s),J) . v = (Valid ('not' s),J) . w
then 'not' ((Valid s,J) . v) = TRUE by Th20;
then (Valid s,J) . v = FALSE by MARGREL1:41;
then (Valid s,J) . w = FALSE by A21, A22, QC_LANG3:11;
then 'not' ((Valid s,J) . w) = TRUE by MARGREL1:41;
hence (Valid ('not' s),J) . v = (Valid ('not' s),J) . w by A25, Th20; :: thesis: verum

end;

hence (Valid ('not' s),J) . v = (Valid ('not' s),J) . w by A23, XBOOLEAN:def 3; :: thesis: verum

end;

end;

thus ( S₁[s] & S₁[t] implies S₁[s '&' t] ) :: thesis: ( S₁[s] implies S₁[ All y,s] )

proof

assume that
A26: ( not x in still_not-bound_in s implies for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid s,J) . v = (Valid s,J) . w ) and
A27: ( not x in still_not-bound_in t implies for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid t,J) . v = (Valid t,J) . w ) and
A28: not x in still_not-bound_in (s '&' t) ; :: thesis: for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid (s '&' t),J) . v = (Valid (s '&' t),J) . w
A29: not x in (still_not-bound_in s) \/ (still_not-bound_in t) by A28, QC_LANG3:14;
thus for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid (s '&' t),J) . v = (Valid (s '&' t),J) . w :: thesis: verum

proof

let v, w be Element of Valuations_in A; :: thesis: ( ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) implies (Valid (s '&' t),J) . v = (Valid (s '&' t),J) . w )
assume A30: for y being bound_QC-variable st x <> y holds
w . y = v . y ; :: thesis: (Valid (s '&' t),J) . v = (Valid (s '&' t),J) . w

A31: now

assume A32: (Valid (s '&' t),J) . v = FALSE ; :: thesis: (Valid (s '&' t),J) . v = (Valid (s '&' t),J) . w

A33: now

assume (Valid s,J) . v = FALSE ; :: thesis: (Valid (s '&' t),J) . v = (Valid (s '&' t),J) . w
then (Valid s,J) . w = FALSE by A26, A29, A30, XBOOLE_0:def 3;
then ((Valid s,J) . w) '&' ((Valid t,J) . w) = FALSE by MARGREL1:45;
hence (Valid (s '&' t),J) . v = (Valid (s '&' t),J) . w by A32, Th22; :: thesis: verum

end;

A34: now

assume (Valid t,J) . v = FALSE ; :: thesis: (Valid (s '&' t),J) . v = (Valid (s '&' t),J) . w
then (Valid t,J) . w = FALSE by A27, A29, A30, XBOOLE_0:def 3;
then ((Valid s,J) . w) '&' ((Valid t,J) . w) = FALSE by MARGREL1:45;
hence (Valid (s '&' t),J) . v = (Valid (s '&' t),J) . w by A32, Th22; :: thesis: verum

end;

((Valid s,J) . v) '&' ((Valid t,J) . v) = FALSE by A32, Th22;
hence (Valid (s '&' t),J) . v = (Valid (s '&' t),J) . w by A33, A34, MARGREL1:45; :: thesis: verum

end;

now

assume A35: (Valid (s '&' t),J) . v = TRUE ; :: thesis: (Valid (s '&' t),J) . v = (Valid (s '&' t),J) . w
then A36: ((Valid s,J) . v) '&' ((Valid t,J) . v) = TRUE by Th22;
then (Valid t,J) . v = TRUE by MARGREL1:45;
then A37: (Valid t,J) . w = TRUE by A27, A29, A30, XBOOLE_0:def 3;
(Valid s,J) . v = TRUE by A36, MARGREL1:45;
then (Valid s,J) . w = TRUE by A26, A29, A30, XBOOLE_0:def 3;
then ((Valid s,J) . w) '&' ((Valid t,J) . w) = TRUE by A37;
hence (Valid (s '&' t),J) . v = (Valid (s '&' t),J) . w by A35, Th22; :: thesis: verum

end;

hence (Valid (s '&' t),J) . v = (Valid (s '&' t),J) . w by A31, XBOOLEAN:def 3; :: thesis: verum

end;

end;

thus ( S₁[s] implies S₁[ All y,s] ) :: thesis: verum

proof

assume that
A38: ( not x in still_not-bound_in s implies for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid s,J) . v = (Valid s,J) . w ) and
A39: not x in still_not-bound_in (All y,s) ; :: thesis: for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid (All y,s),J) . v = (Valid (All y,s),J) . w
A40: not x in (still_not-bound_in s) \ {y} by A39, QC_LANG3:16;
thus for v, w being Element of Valuations_in A st ( for z being bound_QC-variable st x <> z holds
w . z = v . z ) holds
(Valid (All y,s),J) . v = (Valid (All y,s),J) . w :: thesis: verum

proof

let v, w be Element of Valuations_in A; :: thesis: ( ( for z being bound_QC-variable st x <> z holds
w . z = v . z ) implies (Valid (All y,s),J) . v = (Valid (All y,s),J) . w )
assume A41: for z being bound_QC-variable st x <> z holds
w . z = v . z ; :: thesis: (Valid (All y,s),J) . v = (Valid (All y,s),J) . w

A42: now

assume A43: (Valid (All y,s),J) . v = FALSE ; :: thesis: (Valid (All y,s),J) . v = (Valid (All y,s),J) . w
then (FOR_ALL y,(Valid s,J)) . v = FALSE by Lm1;
then consider v1 being Element of Valuations_in A such that
A44: (Valid s,J) . v1 = FALSE and
A45: for z being bound_QC-variable st y <> z holds
v1 . z = v . z by Th7;

A46: now

assume A47: not x in still_not-bound_in s ; :: thesis: ex v2 being Element of Valuations_in A st
( (Valid s,J) . v2 = FALSE & ( for z being bound_QC-variable st y <> z holds
v2 . z = w . z ) )
consider v2 being Element of Valuations_in A such that
A48: ( ( for z being bound_QC-variable st z <> y holds
v2 . z = w . z ) & v2 . y = v1 . y ) from VALUAT_1:sch 1();
take v2 = v2; :: thesis: ( (Valid s,J) . v2 = FALSE & ( for z being bound_QC-variable st y <> z holds
v2 . z = w . z ) )
for z being bound_QC-variable st x <> z holds
v2 . z = v1 . z

proof

let z be bound_QC-variable; :: thesis: ( x <> z implies v2 . z = v1 . z )
assume A49: x <> z ; :: thesis: v2 . z = v1 . z

now

assume A50: z <> y ; :: thesis: v2 . z = v1 . z
hence v2 . z = w . z by A48
.= v . z by A41, A49
.= v1 . z by A45, A50 ;
:: thesis: verum

end;

hence v2 . z = v1 . z by A48; :: thesis: verum

end;

hence (Valid s,J) . v2 = FALSE by A38, A44, A47; :: thesis: for z being bound_QC-variable st y <> z holds
v2 . z = w . z
thus for z being bound_QC-variable st y <> z holds
v2 . z = w . z by A48; :: thesis: verum

end;

now

assume A51: x in {y} ; :: thesis: ex v2 being Element of Valuations_in A st
( (Valid s,J) . v2 = FALSE & ( for z being bound_QC-variable st y <> z holds
v2 . z = w . z ) )
take v2 = v1; :: thesis: ( (Valid s,J) . v2 = FALSE & ( for z being bound_QC-variable st y <> z holds
v2 . z = w . z ) )
thus (Valid s,J) . v2 = FALSE by A44; :: thesis: for z being bound_QC-variable st y <> z holds
v2 . z = w . z
for z being bound_QC-variable st y <> z holds
v1 . z = w . z

proof

let z be bound_QC-variable; :: thesis: ( y <> z implies v1 . z = w . z )
assume A52: y <> z ; :: thesis: v1 . z = w . z
then A53: x <> z by A51, TARSKI:def 1;
thus v1 . z = v . z by A45, A52
.= w . z by A41, A53 ; :: thesis: verum

end;

hence for z being bound_QC-variable st y <> z holds
v2 . z = w . z ; :: thesis: verum

end;

then (FOR_ALL y,(Valid s,J)) . w = FALSE by A40, A46, Th7, XBOOLE_0:def 5;
hence (Valid (All y,s),J) . v = (Valid (All y,s),J) . w by A43, Lm1; :: thesis: verum

end;

now

assume A54: (Valid (All y,s),J) . v = TRUE ; :: thesis: (Valid (All y,s),J) . v = (Valid (All y,s),J) . w
then A55: (FOR_ALL y,(Valid s,J)) . v = TRUE by Lm1;
for v1 being Element of Valuations_in A st ( for z being bound_QC-variable st y <> z holds
v1 . z = w . z ) holds
(Valid s,J) . v1 = TRUE

proof

let v1 be Element of Valuations_in A; :: thesis: ( ( for z being bound_QC-variable st y <> z holds
v1 . z = w . z ) implies (Valid s,J) . v1 = TRUE )
assume A56: for z being bound_QC-variable st y <> z holds
v1 . z = w . z ; :: thesis: (Valid s,J) . v1 = TRUE

A57: now

assume A58: not x in still_not-bound_in s ; :: thesis: (Valid s,J) . v1 = TRUE
consider v2 being Element of Valuations_in A such that
A59: ( ( for z being bound_QC-variable st z <> y holds
v2 . z = v . z ) & v2 . y = v1 . y ) from VALUAT_1:sch 1();
A60: for z being bound_QC-variable st x <> z holds
v2 . z = v1 . z

proof

let z be bound_QC-variable; :: thesis: ( x <> z implies v2 . z = v1 . z )
assume A61: x <> z ; :: thesis: v2 . z = v1 . z

now

assume A62: z <> y ; :: thesis: v2 . z = v1 . z
hence v2 . z = v . z by A59
.= w . z by A41, A61
.= v1 . z by A56, A62 ;
:: thesis: verum

end;

hence v2 . z = v1 . z by A59; :: thesis: verum

end;

(Valid s,J) . v2 = TRUE by A55, A59, Th8;
hence (Valid s,J) . v1 = TRUE by A38, A58, A60; :: thesis: verum

end;

now

assume x in {y} ; :: thesis: (Valid s,J) . v1 = TRUE
then A63: x = y by TARSKI:def 1;
for z being bound_QC-variable st y <> z holds
v1 . z = v . z

proof

let z be bound_QC-variable; :: thesis: ( y <> z implies v1 . z = v . z )
assume A64: y <> z ; :: thesis: v1 . z = v . z
hence v . z = w . z by A41, A63
.= v1 . z by A56, A64 ;
:: thesis: verum

end;

hence (Valid s,J) . v1 = TRUE by A55, Th8; :: thesis: verum

end;

hence (Valid s,J) . v1 = TRUE by A40, A57, XBOOLE_0:def 5; :: thesis: verum

end;

then (FOR_ALL y,(Valid s,J)) . w = TRUE by Th8;
hence (Valid (All y,s),J) . v = (Valid (All y,s),J) . w by A54, Lm1; :: thesis: verum

end;

hence (Valid (All y,s),J) . v = (Valid (All y,s),J) . w by A42, XBOOLEAN:def 3; :: thesis: verum

end;

end;

end;

for s being Element of CQC-WFF holds S₁[s] from CQC_LANG:sch 1(A1);
hence ( not x in still_not-bound_in p implies for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid p,J) . v = (Valid p,J) . w ) ; :: thesis: verum