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 s' being QC-formula 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 x, y be bound_QC-variable; :: thesis: for p, q being Element of CQC-WFF
for J being interpretation of A
for s' being QC-formula 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: for J being interpretation of A
for s' being QC-formula 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 J be interpretation of A; :: thesis: for s' being QC-formula 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 s' be QC-formula; :: 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 )
defpred S1[ 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 S1[s] ) & S1[ VERUM ] & ( s is negative & S1[ the_argument_of s] implies S1[s] ) & ( s is conjunctive & S1[ the_left_argument_of s] & S1[ the_right_argument_of s] implies S1[s] ) & ( s is universal & S1[ the_scope_of s] implies S1[s] ) )
thus ( s is atomic implies S1[s] ) :: thesis: ( S1[ VERUM ] & ( s is negative & S1[ the_argument_of s] implies S1[s] ) & ( s is conjunctive & S1[ the_left_argument_of s] & S1[ the_right_argument_of s] implies S1[s] ) & ( s is universal & S1[ the_scope_of s] implies S1[s] ) )
proof
assume A2: s is atomic ; :: thesis: S1[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 A3: ( x <> y & p = s . x & 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 A4: v . x = v . y ; :: thesis: (Valid p,J) . v = (Valid q,J) . v
consider k being Element of NAT , P being QC-pred_symbol of k, l being QC-variable_list of such that
A5: s = P ! l by A2, QC_LANG1:def 17;
A6: ( p = P ! (Subst l,((a. 0 ) .--> x)) & q = P ! (Subst l,((a. 0 ) .--> y)) ) by A3, A5, CQC_LANG:30;
set lx = Subst l,((a. 0 ) .--> x);
set ly = Subst l,((a. 0 ) .--> y);
A7: ( { ((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 ) } = {} & { ((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 A6, CQC_LANG:17;
( { ((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 ) } = {} & { ((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 A6, CQC_LANG:17;
then reconsider lx = Subst l,((a. 0 ) .--> x), ly = Subst l,((a. 0 ) .--> y) as CQC-variable_list of by A7, CQC_LANG:15;
A8: ( len (v *' lx) = k & ( for i being Element of NAT st 1 <= i & i <= k holds
(v *' lx) . i = v . (lx . i) ) ) by Def8;
A9: ( len (v *' ly) = k & ( for i being Element of NAT st 1 <= i & i <= k holds
(v *' ly) . i = v . (ly . i) ) ) by Def8;
A10: v *' lx = v *' ly
proof
now
let i be Nat; :: thesis: ( 1 <= i & i <= len (v *' lx) implies (v *' lx) . i = (v *' ly) . i )
assume A11: ( 1 <= i & i <= len (v *' lx) ) ; :: thesis: (v *' lx) . i = (v *' ly) . i
then A12: ( 1 <= i & i <= len l ) by A8, FINSEQ_1:def 18;
A13: i in NAT by ORDINAL1:def 13;
A14: now
assume l . i <> a. 0 ; :: thesis: (v *' lx) . i = (v *' ly) . i
then A15: ( lx . i = l . i & ly . i = l . i ) by A12, A13, CQC_LANG:11;
( v . (lx . i) = (v *' lx) . i & v . (ly . i) = (v *' ly) . i ) by A8, A11, Def8;
hence (v *' lx) . i = (v *' ly) . i by A15; :: thesis: verum
end;
now
assume l . i = a. 0 ; :: thesis: (v *' lx) . i = (v *' ly) . i
then A16: ( lx . i = x & ly . i = y ) by A12, A13, CQC_LANG:11;
( v . (lx . i) = (v *' lx) . i & v . (ly . i) = (v *' ly) . i ) by A8, A11, Def8;
hence (v *' lx) . i = (v *' ly) . i by A4, A16; :: thesis: verum
end;
hence (v *' lx) . i = (v *' ly) . i by A14; :: thesis: verum
end;
hence v *' lx = v *' ly by A8, A9, FINSEQ_1:18; :: thesis: verum
end;
A17: now
assume (Valid p,J) . v = TRUE ; :: thesis: (Valid q,J) . v = TRUE
then v *' lx in J . P by A6, Th16;
hence (Valid q,J) . v = TRUE by A6, A10, Th16; :: thesis: verum
end;
now
assume (Valid p,J) . v = FALSE ; :: thesis: (Valid q,J) . v = FALSE
then not v *' lx in J . P by A6, Th17;
hence (Valid q,J) . v = FALSE by A6, A10, Th17; :: thesis: verum
end;
hence (Valid p,J) . v = (Valid q,J) . v by A17, XBOOLEAN:def 3; :: thesis: verum
end;
end;
thus S1[ VERUM ] :: thesis: ( ( s is negative & S1[ the_argument_of s] implies S1[s] ) & ( s is conjunctive & S1[ the_left_argument_of s] & S1[ the_right_argument_of s] implies S1[s] ) & ( s is universal & S1[ the_scope_of s] implies S1[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 A18: ( x <> y & p = VERUM . x & 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 & q = VERUM ) by A18, CQC_LANG:28;
hence (Valid p,J) . v = (Valid q,J) . v ; :: thesis: verum
end;
thus ( s is negative & S1[ the_argument_of s] implies S1[s] ) :: thesis: ( ( s is conjunctive & S1[ the_left_argument_of s] & S1[ the_right_argument_of s] implies S1[s] ) & ( s is universal & S1[ the_scope_of s] implies S1[s] ) )
proof
assume that
A19: s is negative and
A20: 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: S1[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 A21: ( x <> y & p = s . x & 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 A22: v . x = v . y ; :: thesis: (Valid p,J) . v = (Valid q,J) . v
A23: ( s . x = 'not' ((the_argument_of s) . x) & s . y = 'not' ((the_argument_of s) . y) ) by A19, CQC_LANG:31;
then reconsider pa = (the_argument_of s) . x as Element of CQC-WFF by A21, CQC_LANG:18;
reconsider qa = (the_argument_of s) . y as Element of CQC-WFF by A21, A23, CQC_LANG:18;
A24: now
assume (Valid p,J) . v = TRUE ; :: thesis: (Valid q,J) . v = TRUE
then 'not' ((Valid pa,J) . v) = TRUE by A21, A23, Th20;
then (Valid pa,J) . v = FALSE by MARGREL1:41;
then (Valid qa,J) . v = FALSE by A20, A22;
then 'not' ((Valid qa,J) . v) = TRUE by MARGREL1:41;
hence (Valid q,J) . v = TRUE by A21, A23, Th20; :: thesis: verum
end;
now
assume (Valid p,J) . v = FALSE ; :: thesis: (Valid q,J) . v = FALSE
then 'not' ((Valid pa,J) . v) = FALSE by A21, A23, Th20;
then (Valid pa,J) . v = TRUE by MARGREL1:41;
then (Valid qa,J) . v = TRUE by A20, A22;
then 'not' ((Valid qa,J) . v) = FALSE by MARGREL1:41;
hence (Valid q,J) . v = FALSE by A21, A23, Th20; :: thesis: verum
end;
hence (Valid p,J) . v = (Valid q,J) . v by A24, XBOOLEAN:def 3; :: thesis: verum
end;
end;
thus ( s is conjunctive & S1[ the_left_argument_of s] & S1[ the_right_argument_of s] implies S1[s] ) :: thesis: ( s is universal & S1[ the_scope_of s] implies S1[s] )
proof
assume that
A25: s is conjunctive and
A26: 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
A27: 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: S1[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 A28: ( x <> y & p = s . x & 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 A29: v . x = v . y ; :: thesis: (Valid p,J) . v = (Valid q,J) . v
A30: ( s . x = ((the_left_argument_of s) . x) '&' ((the_right_argument_of s) . x) & s . y = ((the_left_argument_of s) . y) '&' ((the_right_argument_of s) . y) ) by A25, 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 A28, CQC_LANG:19;
reconsider qla = (the_left_argument_of s) . y, qra = (the_right_argument_of s) . y as Element of CQC-WFF by A28, A30, CQC_LANG:19;
A31: now
assume (Valid p,J) . v = TRUE ; :: thesis: (Valid q,J) . v = TRUE
then ((Valid pla,J) . v) '&' ((Valid pra,J) . v) = TRUE by A28, A30, Th22;
then ( (Valid pla,J) . v = TRUE & (Valid pra,J) . v = TRUE ) by MARGREL1:45;
then ( (Valid qla,J) . v = TRUE & (Valid qra,J) . v = TRUE ) by A26, A27, A29;
then ((Valid qla,J) . v) '&' ((Valid qra,J) . v) = TRUE ;
hence (Valid q,J) . v = TRUE by A28, A30, Th22; :: thesis: verum
end;
now
assume A32: (Valid p,J) . v = FALSE ; :: thesis: (Valid p,J) . v = (Valid q,J) . v
then A33: ((Valid pla,J) . v) '&' ((Valid pra,J) . v) = FALSE by A28, A30, Th22;
A34: now
assume (Valid pla,J) . v = FALSE ; :: thesis: (Valid p,J) . v = (Valid q,J) . v
then (Valid qla,J) . v = FALSE by A26, A29;
then ((Valid qla,J) . v) '&' ((Valid qra,J) . v) = FALSE by MARGREL1:45;
hence (Valid p,J) . v = (Valid q,J) . v by A28, A30, A32, Th22; :: thesis: verum
end;
now
assume (Valid pra,J) . v = FALSE ; :: thesis: (Valid p,J) . v = (Valid q,J) . v
then (Valid qra,J) . v = FALSE by A27, A29;
then ((Valid qla,J) . v) '&' ((Valid qra,J) . v) = FALSE by MARGREL1:45;
hence (Valid p,J) . v = (Valid q,J) . v by A28, A30, A32, Th22; :: thesis: verum
end;
hence (Valid p,J) . v = (Valid q,J) . v by A33, A34, MARGREL1:45; :: thesis: verum
end;
hence (Valid p,J) . v = (Valid q,J) . v by A31, XBOOLEAN:def 3; :: thesis: verum
end;
end;
thus ( s is universal & S1[ the_scope_of s] implies S1[s] ) :: thesis: verum
proof
assume that
A35: s is universal and
A36: 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: S1[s]
consider xx being bound_QC-variable, pp being Element of QC-WFF such that
A37: s = All xx,pp by A35, QC_LANG1:def 20;
A38: xx = bound_in s by A35, A37, 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: 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 A39: ( x <> y & p = s . x & 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 A40: v . x = v . y ; :: thesis: (Valid p,J) . v = (Valid q,J) . v
A41: now
assume A42: 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 A35, CQC_LANG:36;
then reconsider ps = (the_scope_of s) . x as Element of CQC-WFF by A39, CQC_LANG:23;
A43: All (bound_in s),ps = p by A35, A39, A42, CQC_LANG:36;
A44: now
assume A45: 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 A35, CQC_LANG:36;
then reconsider qs = (the_scope_of s) . y as Element of CQC-WFF by A39, CQC_LANG:23;
A46: All (bound_in s),qs = q by A35, A39, A45, CQC_LANG:36;
A47: ( Valid (All (bound_in s),ps),J = FOR_ALL (bound_in s),(Valid ps,J) & Valid (All (bound_in s),qs),J = FOR_ALL (bound_in s),(Valid qs,J) ) by Lm1;
A48: now
assume A49: (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 A50: for y being bound_QC-variable st bound_in s <> y holds
v1 . y = v . y ; :: thesis: (Valid qs,J) . v1 = TRUE
then A51: ( v1 . x = v . x & v1 . y = v . y ) by A42, A45;
(Valid ps,J) . v1 = TRUE by A43, A47, A49, A50, Th8;
hence (Valid qs,J) . v1 = TRUE by A36, A40, A51; :: thesis: verum
end;
hence (Valid q,J) . v = TRUE by A46, A47, Th8; :: thesis: verum
end;
now
assume A52: (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
A53: (Valid ps,J) . v1 = FALSE and
A54: for y being bound_QC-variable st bound_in s <> y holds
v1 . y = v . y by A43, A47, A52, Th7;
( v1 . x = v . x & v1 . y = v . y ) by A42, A45, A54;
then (Valid qs,J) . v1 = FALSE by A36, A40, A53;
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 A54; :: thesis: verum
end;
hence (Valid q,J) . v = FALSE by A46, A47, Th7; :: thesis: verum
end;
hence (Valid p,J) . v = (Valid q,J) . v by A48, XBOOLEAN:def 3; :: thesis: verum
end;
now
assume A55: y = bound_in s ; :: thesis: (Valid p,J) . v = (Valid q,J) . v
then q = All y,pp by A37, A38, A39, CQC_LANG:37;
hence (Valid p,J) . v = (Valid q,J) . v by A37, A38, A39, A55, CQC_LANG:40; :: thesis: verum
end;
hence (Valid p,J) . v = (Valid q,J) . v by A44; :: thesis: verum
end;
now
assume A56: x = bound_in s ; :: thesis: (Valid p,J) . v = (Valid q,J) . v
then p = All x,pp by A37, A38, A39, CQC_LANG:37;
hence (Valid p,J) . v = (Valid q,J) . v by A37, A38, A39, A56, CQC_LANG:40; :: thesis: verum
end;
hence (Valid p,J) . v = (Valid q,J) . v by A41; :: thesis: verum
end;
end;
end;
for s being Element of QC-WFF holds S1[s] from QC_LANG1:sch 2(A1);
 hence ( 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 ) ; :: thesis: verum