let Al be QC-alphabet ; for A being non empty set
for x being bound_QC-variable of Al
for p being Element of CQC-WFF Al
for J being interpretation of Al,A st not x in still_not-bound_in p holds
for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid (p,J)) . v = (Valid (p,J)) . w
let A be non empty set ; for x being bound_QC-variable of Al
for p being Element of CQC-WFF Al
for J being interpretation of Al,A st not x in still_not-bound_in p holds
for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid (p,J)) . v = (Valid (p,J)) . w
let x be bound_QC-variable of Al; for p being Element of CQC-WFF Al
for J being interpretation of Al,A st not x in still_not-bound_in p holds
for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid (p,J)) . v = (Valid (p,J)) . w
let p be Element of CQC-WFF Al; for J being interpretation of Al,A st not x in still_not-bound_in p holds
for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid (p,J)) . v = (Valid (p,J)) . w
let J be interpretation of Al,A; ( not x in still_not-bound_in p implies for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid (p,J)) . v = (Valid (p,J)) . w )
defpred S1[ Element of CQC-WFF Al] means ( not x in still_not-bound_in $1 implies for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid ($1,J)) . v = (Valid ($1,J)) . w );
A1:
now for s, t being Element of CQC-WFF Al
for y being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( S1[ VERUM Al] & S1[P ! ll] & ( S1[s] implies S1[ 'not' s] ) & ( S1[s] & S1[t] implies S1[s '&' t] ) & ( S1[s] implies S1[ All (y,s)] ) )let s,
t be
Element of
CQC-WFF Al;
for y being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( S1[ VERUM Al] & S1[P ! ll] & ( S1[s] implies S1[ 'not' s] ) & ( S1[s] & S1[t] implies S1[s '&' t] ) & ( S1[s] implies S1[ All (y,s)] ) )let y be
bound_QC-variable of
Al;
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( S1[ VERUM Al] & S1[P ! ll] & ( S1[s] implies S1[ 'not' s] ) & ( S1[s] & S1[t] implies S1[s '&' t] ) & ( S1[s] implies S1[ All (y,s)] ) )let k be
Nat;
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( S1[ VERUM Al] & S1[P ! ll] & ( S1[s] implies S1[ 'not' s] ) & ( S1[s] & S1[t] implies S1[s '&' t] ) & ( S1[s] implies S1[ All (y,s)] ) )let ll be
CQC-variable_list of
k,
Al;
for P being QC-pred_symbol of k,Al holds
( S1[ VERUM Al] & S1[P ! ll] & ( S1[s] implies S1[ 'not' s] ) & ( S1[s] & S1[t] implies S1[s '&' t] ) & ( S1[s] implies S1[ All (y,s)] ) )let P be
QC-pred_symbol of
k,
Al;
( S1[ VERUM Al] & S1[P ! ll] & ( S1[s] implies S1[ 'not' s] ) & ( S1[s] & S1[t] implies S1[s '&' t] ) & ( S1[s] implies S1[ All (y,s)] ) )thus
S1[
VERUM Al]
( S1[P ! ll] & ( S1[s] implies S1[ 'not' s] ) & ( S1[s] & S1[t] implies S1[s '&' t] ) & ( S1[s] implies S1[ All (y,s)] ) )A2:
rng ll c= bound_QC-variables Al
by RELAT_1:def 19;
thus
S1[
P ! ll]
( ( S1[s] implies S1[ 'not' s] ) & ( S1[s] & S1[t] implies S1[s '&' t] ) & ( S1[s] implies S1[ All (y,s)] ) )thus
(
S1[
s] implies
S1[
'not' s] )
( ( S1[s] & S1[t] implies S1[s '&' t] ) & ( S1[s] implies S1[ All (y,s)] ) )proof
assume A20:
( ( not
x in still_not-bound_in s implies for
v,
w being
Element of
Valuations_in (
Al,
A) st ( for
y being
bound_QC-variable of
Al 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) )
;
for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al 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 (
Al,
A) st ( for
y being
bound_QC-variable of
Al st
x <> y holds
w . y = v . y ) holds
(Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w
verumproof
let v,
w be
Element of
Valuations_in (
Al,
A);
( ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) implies (Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w )
assume A21:
for
y being
bound_QC-variable of
Al st
x <> y holds
w . y = v . y
;
(Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w
A22:
now ( (Valid (('not' s),J)) . v = FALSE implies (Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w )assume A23:
(Valid (('not' s),J)) . v = FALSE
;
(Valid (('not' s),J)) . v = (Valid (('not' s),J)) . wthen
'not' ((Valid (s,J)) . v) = FALSE
by Th10;
then
(Valid (s,J)) . v = TRUE
by MARGREL1:11;
then
(Valid (s,J)) . w = TRUE
by A20, A21, QC_LANG3:7;
then
'not' ((Valid (s,J)) . w) = FALSE
by MARGREL1:11;
hence
(Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w
by A23, Th10;
verum end;
now ( (Valid (('not' s),J)) . v = TRUE implies (Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w )assume A24:
(Valid (('not' s),J)) . v = TRUE
;
(Valid (('not' s),J)) . v = (Valid (('not' s),J)) . wthen
'not' ((Valid (s,J)) . v) = TRUE
by Th10;
then
(Valid (s,J)) . v = FALSE
by MARGREL1:11;
then
(Valid (s,J)) . w = FALSE
by A20, A21, QC_LANG3:7;
then
'not' ((Valid (s,J)) . w) = TRUE
by MARGREL1:11;
hence
(Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w
by A24, Th10;
verum end;
hence
(Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w
by A22, XBOOLEAN:def 3;
verum
end;
end; thus
(
S1[
s] &
S1[
t] implies
S1[
s '&' t] )
( S1[s] implies S1[ All (y,s)] )proof
assume that A25:
( not
x in still_not-bound_in s implies for
v,
w being
Element of
Valuations_in (
Al,
A) st ( for
y being
bound_QC-variable of
Al st
x <> y holds
w . y = v . y ) holds
(Valid (s,J)) . v = (Valid (s,J)) . w )
and A26:
( not
x in still_not-bound_in t implies for
v,
w being
Element of
Valuations_in (
Al,
A) st ( for
y being
bound_QC-variable of
Al st
x <> y holds
w . y = v . y ) holds
(Valid (t,J)) . v = (Valid (t,J)) . w )
and A27:
not
x in still_not-bound_in (s '&' t)
;
for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w
A28:
not
x in (still_not-bound_in s) \/ (still_not-bound_in t)
by A27, QC_LANG3:10;
thus
for
v,
w being
Element of
Valuations_in (
Al,
A) st ( for
y being
bound_QC-variable of
Al st
x <> y holds
w . y = v . y ) holds
(Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w
verumproof
let v,
w be
Element of
Valuations_in (
Al,
A);
( ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) implies (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w )
assume A29:
for
y being
bound_QC-variable of
Al st
x <> y holds
w . y = v . y
;
(Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w
A30:
now ( (Valid ((s '&' t),J)) . v = FALSE implies (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w )assume A31:
(Valid ((s '&' t),J)) . v = FALSE
;
(Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . wA32:
now ( (Valid (s,J)) . v = FALSE implies (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w )assume
(Valid (s,J)) . v = FALSE
;
(Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . wthen
(Valid (s,J)) . w = FALSE
by A25, A28, A29, XBOOLE_0:def 3;
then
((Valid (s,J)) . w) '&' ((Valid (t,J)) . w) = FALSE
by MARGREL1:12;
hence
(Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w
by A31, Th12;
verum end; A33:
now ( (Valid (t,J)) . v = FALSE implies (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w )assume
(Valid (t,J)) . v = FALSE
;
(Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . wthen
(Valid (t,J)) . w = FALSE
by A26, A28, A29, XBOOLE_0:def 3;
then
((Valid (s,J)) . w) '&' ((Valid (t,J)) . w) = FALSE
by MARGREL1:12;
hence
(Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w
by A31, Th12;
verum end;
((Valid (s,J)) . v) '&' ((Valid (t,J)) . v) = FALSE
by A31, Th12;
hence
(Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w
by A32, A33, MARGREL1:12;
verum end;
now ( (Valid ((s '&' t),J)) . v = TRUE implies (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w )assume A34:
(Valid ((s '&' t),J)) . v = TRUE
;
(Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . wthen A35:
((Valid (s,J)) . v) '&' ((Valid (t,J)) . v) = TRUE
by Th12;
then
(Valid (t,J)) . v = TRUE
by MARGREL1:12;
then A36:
(Valid (t,J)) . w = TRUE
by A26, A28, A29, XBOOLE_0:def 3;
(Valid (s,J)) . v = TRUE
by A35, MARGREL1:12;
then
(Valid (s,J)) . w = TRUE
by A25, A28, A29, XBOOLE_0:def 3;
then
((Valid (s,J)) . w) '&' ((Valid (t,J)) . w) = TRUE
by A36;
hence
(Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w
by A34, Th12;
verum end;
hence
(Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w
by A30, XBOOLEAN:def 3;
verum
end;
end; thus
(
S1[
s] implies
S1[
All (
y,
s)] )
verumproof
assume that A37:
( not
x in still_not-bound_in s implies for
v,
w being
Element of
Valuations_in (
Al,
A) st ( for
y being
bound_QC-variable of
Al st
x <> y holds
w . y = v . y ) holds
(Valid (s,J)) . v = (Valid (s,J)) . w )
and A38:
not
x in still_not-bound_in (All (y,s))
;
for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w
A39:
not
x in (still_not-bound_in s) \ {y}
by A38, QC_LANG3:12;
thus
for
v,
w being
Element of
Valuations_in (
Al,
A) st ( for
z being
bound_QC-variable of
Al st
x <> z holds
w . z = v . z ) holds
(Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w
verumproof
let v,
w be
Element of
Valuations_in (
Al,
A);
( ( for z being bound_QC-variable of Al st x <> z holds
w . z = v . z ) implies (Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w )
assume A40:
for
z being
bound_QC-variable of
Al st
x <> z holds
w . z = v . z
;
(Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w
A41:
now ( (Valid ((All (y,s)),J)) . v = FALSE implies (Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w )assume A42:
(Valid ((All (y,s)),J)) . v = FALSE
;
(Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . wthen
(FOR_ALL (y,(Valid (s,J)))) . v = FALSE
by Lm1;
then consider v1 being
Element of
Valuations_in (
Al,
A)
such that A43:
(Valid (s,J)) . v1 = FALSE
and A44:
for
z being
bound_QC-variable of
Al st
y <> z holds
v1 . z = v . z
by Th2;
then
(FOR_ALL (y,(Valid (s,J)))) . w = FALSE
by A39, A45, Th2, XBOOLE_0:def 5;
hence
(Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w
by A42, Lm1;
verum end;
now ( (Valid ((All (y,s)),J)) . v = TRUE implies (Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w )assume A53:
(Valid ((All (y,s)),J)) . v = TRUE
;
(Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . wthen A54:
(FOR_ALL (y,(Valid (s,J)))) . v = TRUE
by Lm1;
for
v1 being
Element of
Valuations_in (
Al,
A) st ( for
z being
bound_QC-variable of
Al st
y <> z holds
v1 . z = w . z ) holds
(Valid (s,J)) . v1 = TRUE
then
(FOR_ALL (y,(Valid (s,J)))) . w = TRUE
by Th3;
hence
(Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w
by A53, Lm1;
verum end;
hence
(Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w
by A41, XBOOLEAN:def 3;
verum
end;
end; end;
for s being Element of CQC-WFF Al holds S1[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 (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid (p,J)) . v = (Valid (p,J)) . w )
; verum