let Al be QC-alphabet ; :: thesis: for r being Element of CQC-WFF Al

for A being non empty set

for Al2 being Al -expanding QC-alphabet

for J2 being interpretation of Al2,A

for Jp being interpretation of Al,A

for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast r iff Jp,vp |= r )

let r be Element of CQC-WFF Al; :: thesis: for A being non empty set

for Al2 being Al -expanding QC-alphabet

for J2 being interpretation of Al2,A

for Jp being interpretation of Al,A

for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast r iff Jp,vp |= r )

let A be non empty set ; :: thesis: for Al2 being Al -expanding QC-alphabet

for J2 being interpretation of Al2,A

for Jp being interpretation of Al,A

for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast r iff Jp,vp |= r )

let Al2 be Al -expanding QC-alphabet ; :: thesis: for J2 being interpretation of Al2,A

for Jp being interpretation of Al,A

for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast r iff Jp,vp |= r )

let J2 be interpretation of Al2,A; :: thesis: for Jp being interpretation of Al,A

for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast r iff Jp,vp |= r )

let Jp be interpretation of Al,A; :: thesis: for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast r iff Jp,vp |= r )

let v2 be Element of Valuations_in (Al2,A); :: thesis: for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast r iff Jp,vp |= r )

let vp be Element of Valuations_in (Al,A); :: thesis: ( Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) implies ( J2,v2 |= Al2 -Cast r iff Jp,vp |= r ) )

defpred S_{1}[ Element of CQC-WFF Al] means for J2 being interpretation of Al2,A

for Jp being interpretation of Al,A

for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast $1 iff Jp,vp |= $1 );

A1: S_{1}[ VERUM Al]

for P being QC-pred_symbol of k,Al

for l being CQC-variable_list of k,Al holds S_{1}[P ! l]
_{1}[p] holds

S_{1}[ 'not' p]
_{1}[p] & S_{1}[r] holds

S_{1}[p '&' r]

for r being Element of CQC-WFF Al st S_{1}[r] holds

S_{1}[ All (x,r)]

for x being bound_QC-variable of Al

for k being Nat

for l being CQC-variable_list of k,Al

for P being QC-pred_symbol of k,Al holds

( S_{1}[ VERUM Al] & S_{1}[P ! l] & ( S_{1}[r] implies S_{1}[ 'not' r] ) & ( S_{1}[r] & S_{1}[s] implies S_{1}[r '&' s] ) & ( S_{1}[r] implies S_{1}[ All (x,r)] ) )
by A1, A2, A19, A26, A30;

for r being Element of CQC-WFF Al holds S_{1}[r]
from CQC_LANG:sch 1(A59);

hence ( Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) implies ( J2,v2 |= Al2 -Cast r iff Jp,vp |= r ) ) ; :: thesis: verum

for A being non empty set

for Al2 being Al -expanding QC-alphabet

for J2 being interpretation of Al2,A

for Jp being interpretation of Al,A

for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast r iff Jp,vp |= r )

let r be Element of CQC-WFF Al; :: thesis: for A being non empty set

for Al2 being Al -expanding QC-alphabet

for J2 being interpretation of Al2,A

for Jp being interpretation of Al,A

for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast r iff Jp,vp |= r )

let A be non empty set ; :: thesis: for Al2 being Al -expanding QC-alphabet

for J2 being interpretation of Al2,A

for Jp being interpretation of Al,A

for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast r iff Jp,vp |= r )

let Al2 be Al -expanding QC-alphabet ; :: thesis: for J2 being interpretation of Al2,A

for Jp being interpretation of Al,A

for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast r iff Jp,vp |= r )

let J2 be interpretation of Al2,A; :: thesis: for Jp being interpretation of Al,A

for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast r iff Jp,vp |= r )

let Jp be interpretation of Al,A; :: thesis: for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast r iff Jp,vp |= r )

let v2 be Element of Valuations_in (Al2,A); :: thesis: for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast r iff Jp,vp |= r )

let vp be Element of Valuations_in (Al,A); :: thesis: ( Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) implies ( J2,v2 |= Al2 -Cast r iff Jp,vp |= r ) )

defpred S

for Jp being interpretation of Al,A

for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast $1 iff Jp,vp |= $1 );

A1: S

proof

A2:
for k being Nat
let J2 be interpretation of Al2,A; :: thesis: for Jp being interpretation of Al,A

for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast (VERUM Al) iff Jp,vp |= VERUM Al )

let Jp be interpretation of Al,A; :: thesis: for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast (VERUM Al) iff Jp,vp |= VERUM Al )

let v2 be Element of Valuations_in (Al2,A); :: thesis: for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast (VERUM Al) iff Jp,vp |= VERUM Al )

let vp be Element of Valuations_in (Al,A); :: thesis: ( Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) implies ( J2,v2 |= Al2 -Cast (VERUM Al) iff Jp,vp |= VERUM Al ) )

J2,v2 |= VERUM Al2 by VALUAT_1:32;

hence ( Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) implies ( J2,v2 |= Al2 -Cast (VERUM Al) iff Jp,vp |= VERUM Al ) ) by VALUAT_1:32; :: thesis: verum

end;for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast (VERUM Al) iff Jp,vp |= VERUM Al )

let Jp be interpretation of Al,A; :: thesis: for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast (VERUM Al) iff Jp,vp |= VERUM Al )

let v2 be Element of Valuations_in (Al2,A); :: thesis: for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast (VERUM Al) iff Jp,vp |= VERUM Al )

let vp be Element of Valuations_in (Al,A); :: thesis: ( Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) implies ( J2,v2 |= Al2 -Cast (VERUM Al) iff Jp,vp |= VERUM Al ) )

J2,v2 |= VERUM Al2 by VALUAT_1:32;

hence ( Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) implies ( J2,v2 |= Al2 -Cast (VERUM Al) iff Jp,vp |= VERUM Al ) ) by VALUAT_1:32; :: thesis: verum

for P being QC-pred_symbol of k,Al

for l being CQC-variable_list of k,Al holds S

proof

A19:
for p being Element of CQC-WFF Al st S
let k be Nat; :: thesis: for P being QC-pred_symbol of k,Al

for l being CQC-variable_list of k,Al holds S_{1}[P ! l]

let P be QC-pred_symbol of k,Al; :: thesis: for l being CQC-variable_list of k,Al holds S_{1}[P ! l]

let l be CQC-variable_list of k,Al; :: thesis: S_{1}[P ! l]

let J2 be interpretation of Al2,A; :: thesis: for Jp being interpretation of Al,A

for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast (P ! l) iff Jp,vp |= P ! l )

let Jp be interpretation of Al,A; :: thesis: for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast (P ! l) iff Jp,vp |= P ! l )

let v2 be Element of Valuations_in (Al2,A); :: thesis: for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast (P ! l) iff Jp,vp |= P ! l )

let vp be Element of Valuations_in (Al,A); :: thesis: ( Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) implies ( J2,v2 |= Al2 -Cast (P ! l) iff Jp,vp |= P ! l ) )

assume A3: ( Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) ) ; :: thesis: ( J2,v2 |= Al2 -Cast (P ! l) iff Jp,vp |= P ! l )

set p = P ! l;

the_arity_of P = len l by Th1;

then A4: P ! l = <*P*> ^ l by QC_LANG1:def 12;

( P is QC-pred_symbol of k,Al2 & l is CQC-variable_list of k,Al2 ) by Th5, Th6;

then consider P2 being QC-pred_symbol of k,Al2, l2 being CQC-variable_list of k,Al2 such that

A5: ( P = P2 & l = l2 ) ;

A6: the_arity_of P2 = len l2 by Th1;

A7: v2 *' l2 = vp *' l

end;for l being CQC-variable_list of k,Al holds S

let P be QC-pred_symbol of k,Al; :: thesis: for l being CQC-variable_list of k,Al holds S

let l be CQC-variable_list of k,Al; :: thesis: S

let J2 be interpretation of Al2,A; :: thesis: for Jp being interpretation of Al,A

for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast (P ! l) iff Jp,vp |= P ! l )

let Jp be interpretation of Al,A; :: thesis: for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast (P ! l) iff Jp,vp |= P ! l )

let v2 be Element of Valuations_in (Al2,A); :: thesis: for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast (P ! l) iff Jp,vp |= P ! l )

let vp be Element of Valuations_in (Al,A); :: thesis: ( Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) implies ( J2,v2 |= Al2 -Cast (P ! l) iff Jp,vp |= P ! l ) )

assume A3: ( Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) ) ; :: thesis: ( J2,v2 |= Al2 -Cast (P ! l) iff Jp,vp |= P ! l )

set p = P ! l;

the_arity_of P = len l by Th1;

then A4: P ! l = <*P*> ^ l by QC_LANG1:def 12;

( P is QC-pred_symbol of k,Al2 & l is CQC-variable_list of k,Al2 ) by Th5, Th6;

then consider P2 being QC-pred_symbol of k,Al2, l2 being CQC-variable_list of k,Al2 such that

A5: ( P = P2 & l = l2 ) ;

A6: the_arity_of P2 = len l2 by Th1;

A7: v2 *' l2 = vp *' l

proof

A16:
( J2,v2 |= Al2 -Cast (P ! l) implies Jp,vp |= P ! l )
A8:
bound_QC-variables Al c= bound_QC-variables Al2
by Th4;

A9: for j being Nat st 1 <= j & j <= len l holds

( l . j in bound_QC-variables Al iff l . j in bound_QC-variables Al2 )

set t2 = { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al2 ) } ;

A11: { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al ) } = { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al2 ) }

A15: vp | (still_not-bound_in l) = v2 | ((bound_QC-variables Al) /\ (still_not-bound_in l)) by A3, RELAT_1:71

.= v2 | (still_not-bound_in l) by XBOOLE_1:28 ;

v2 *' l2 = l * (vp | (still_not-bound_in l)) by A5, A14, A15, SUBLEMMA:59

.= vp *' l by SUBLEMMA:59 ;

hence v2 *' l2 = vp *' l ; :: thesis: verum

end;A9: for j being Nat st 1 <= j & j <= len l holds

( l . j in bound_QC-variables Al iff l . j in bound_QC-variables Al2 )

proof

set t1 = { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al ) } ;
let j be Nat; :: thesis: ( 1 <= j & j <= len l implies ( l . j in bound_QC-variables Al iff l . j in bound_QC-variables Al2 ) )

assume A10: ( 1 <= j & j <= len l ) ; :: thesis: ( l . j in bound_QC-variables Al iff l . j in bound_QC-variables Al2 )

thus ( l . j in bound_QC-variables Al implies l . j in bound_QC-variables Al2 ) by A8; :: thesis: ( l . j in bound_QC-variables Al2 implies l . j in bound_QC-variables Al )

end;assume A10: ( 1 <= j & j <= len l ) ; :: thesis: ( l . j in bound_QC-variables Al iff l . j in bound_QC-variables Al2 )

thus ( l . j in bound_QC-variables Al implies l . j in bound_QC-variables Al2 ) by A8; :: thesis: ( l . j in bound_QC-variables Al2 implies l . j in bound_QC-variables Al )

hereby :: thesis: verum

assume
l . j in bound_QC-variables Al2
; :: thesis: l . j in bound_QC-variables Al

len l = k by CARD_1:def 7;

then j in Seg k by A10, FINSEQ_1:1;

then j in dom l by FINSEQ_1:89;

hence l . j in bound_QC-variables Al by FUNCT_1:102; :: thesis: verum

end;len l = k by CARD_1:def 7;

then j in Seg k by A10, FINSEQ_1:1;

then j in dom l by FINSEQ_1:89;

hence l . j in bound_QC-variables Al by FUNCT_1:102; :: thesis: verum

set t2 = { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al2 ) } ;

A11: { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al ) } = { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al2 ) }

proof

A14:
still_not-bound_in l = still_not-bound_in l2
by A5, A11;
thus
{ (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al ) } c= { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al2 ) }
:: according to XBOOLE_0:def 10 :: thesis: { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al2 ) } c= { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al ) }

end;proof

thus
{ (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al2 ) } c= { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al ) }
:: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al ) } or x in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al2 ) } )

assume x in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al ) } ; :: thesis: x in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al2 ) }

then consider i being Nat such that

A12: ( x = l . i & 1 <= i & i <= len l & l . i in bound_QC-variables Al ) ;

( x = l . i & 1 <= i & i <= len l & l . i in bound_QC-variables Al2 ) by A9, A12;

hence x in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al2 ) } ; :: thesis: verum

end;assume x in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al ) } ; :: thesis: x in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al2 ) }

then consider i being Nat such that

A12: ( x = l . i & 1 <= i & i <= len l & l . i in bound_QC-variables Al ) ;

( x = l . i & 1 <= i & i <= len l & l . i in bound_QC-variables Al2 ) by A9, A12;

hence x in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al2 ) } ; :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al2 ) } or x in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al ) } )

assume x in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al2 ) } ; :: thesis: x in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al ) }

then consider i being Nat such that

A13: ( x = l . i & 1 <= i & i <= len l & l . i in bound_QC-variables Al2 ) ;

( x = l . i & 1 <= i & i <= len l & l . i in bound_QC-variables Al ) by A9, A13;

hence x in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al ) } ; :: thesis: verum

end;assume x in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al2 ) } ; :: thesis: x in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al ) }

then consider i being Nat such that

A13: ( x = l . i & 1 <= i & i <= len l & l . i in bound_QC-variables Al2 ) ;

( x = l . i & 1 <= i & i <= len l & l . i in bound_QC-variables Al ) by A9, A13;

hence x in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al ) } ; :: thesis: verum

A15: vp | (still_not-bound_in l) = v2 | ((bound_QC-variables Al) /\ (still_not-bound_in l)) by A3, RELAT_1:71

.= v2 | (still_not-bound_in l) by XBOOLE_1:28 ;

v2 *' l2 = l * (vp | (still_not-bound_in l)) by A5, A14, A15, SUBLEMMA:59

.= vp *' l by SUBLEMMA:59 ;

hence v2 *' l2 = vp *' l ; :: thesis: verum

proof

( not J2,v2 |= Al2 -Cast (P ! l) implies not Jp,vp |= P ! l )
assume
J2,v2 |= Al2 -Cast (P ! l)
; :: thesis: Jp,vp |= P ! l

then J2,v2 |= P2 ! l2 by A4, A5, A6, QC_LANG1:def 12;

then (Valid ((P2 ! l2),J2)) . v2 = TRUE by VALUAT_1:def 7;

then (l2 'in' (J2 . P2)) . v2 = TRUE by VALUAT_1:6;

then A17: vp *' l in J2 . P2 by A7, VALUAT_1:def 4;

vp *' l in Jp . P by FUNCT_1:49, A3, A5, A17;

then (l 'in' (Jp . P)) . vp = TRUE by VALUAT_1:def 4;

then (Valid ((P ! l),Jp)) . vp = TRUE by VALUAT_1:6;

hence Jp,vp |= P ! l by VALUAT_1:def 7; :: thesis: verum

end;then J2,v2 |= P2 ! l2 by A4, A5, A6, QC_LANG1:def 12;

then (Valid ((P2 ! l2),J2)) . v2 = TRUE by VALUAT_1:def 7;

then (l2 'in' (J2 . P2)) . v2 = TRUE by VALUAT_1:6;

then A17: vp *' l in J2 . P2 by A7, VALUAT_1:def 4;

vp *' l in Jp . P by FUNCT_1:49, A3, A5, A17;

then (l 'in' (Jp . P)) . vp = TRUE by VALUAT_1:def 4;

then (Valid ((P ! l),Jp)) . vp = TRUE by VALUAT_1:6;

hence Jp,vp |= P ! l by VALUAT_1:def 7; :: thesis: verum

proof

hence
( J2,v2 |= Al2 -Cast (P ! l) iff Jp,vp |= P ! l )
by A16; :: thesis: verum
assume
not J2,v2 |= Al2 -Cast (P ! l)
; :: thesis: not Jp,vp |= P ! l

then not J2,v2 |= P2 ! l2 by A4, A5, A6, QC_LANG1:def 12;

then not (Valid ((P2 ! l2),J2)) . v2 = TRUE by VALUAT_1:def 7;

then not (l2 'in' (J2 . P2)) . v2 = TRUE by VALUAT_1:6;

then A18: not vp *' l in J2 . P2 by A7, VALUAT_1:def 4;

not vp *' l in Jp . P by FUNCT_1:49, A3, A5, A18;

then not (l 'in' (Jp . P)) . vp = TRUE by VALUAT_1:def 4;

then not (Valid ((P ! l),Jp)) . vp = TRUE by VALUAT_1:6;

hence not Jp,vp |= P ! l by VALUAT_1:def 7; :: thesis: verum

end;then not J2,v2 |= P2 ! l2 by A4, A5, A6, QC_LANG1:def 12;

then not (Valid ((P2 ! l2),J2)) . v2 = TRUE by VALUAT_1:def 7;

then not (l2 'in' (J2 . P2)) . v2 = TRUE by VALUAT_1:6;

then A18: not vp *' l in J2 . P2 by A7, VALUAT_1:def 4;

not vp *' l in Jp . P by FUNCT_1:49, A3, A5, A18;

then not (l 'in' (Jp . P)) . vp = TRUE by VALUAT_1:def 4;

then not (Valid ((P ! l),Jp)) . vp = TRUE by VALUAT_1:6;

hence not Jp,vp |= P ! l by VALUAT_1:def 7; :: thesis: verum

S

proof

A26:
for p, r being Element of CQC-WFF Al st S
let p be Element of CQC-WFF Al; :: thesis: ( S_{1}[p] implies S_{1}[ 'not' p] )

assume A20: S_{1}[p]
; :: thesis: S_{1}[ 'not' p]

let J2 be interpretation of Al2,A; :: thesis: for Jp being interpretation of Al,A

for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast ('not' p) iff Jp,vp |= 'not' p )

let Jp be interpretation of Al,A; :: thesis: for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast ('not' p) iff Jp,vp |= 'not' p )

let v2 be Element of Valuations_in (Al2,A); :: thesis: for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast ('not' p) iff Jp,vp |= 'not' p )

let vp be Element of Valuations_in (Al,A); :: thesis: ( Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) implies ( J2,v2 |= Al2 -Cast ('not' p) iff Jp,vp |= 'not' p ) )

assume A21: ( Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) ) ; :: thesis: ( J2,v2 |= Al2 -Cast ('not' p) iff Jp,vp |= 'not' p )

end;assume A20: S

let J2 be interpretation of Al2,A; :: thesis: for Jp being interpretation of Al,A

for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast ('not' p) iff Jp,vp |= 'not' p )

let Jp be interpretation of Al,A; :: thesis: for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast ('not' p) iff Jp,vp |= 'not' p )

let v2 be Element of Valuations_in (Al2,A); :: thesis: for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast ('not' p) iff Jp,vp |= 'not' p )

let vp be Element of Valuations_in (Al,A); :: thesis: ( Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) implies ( J2,v2 |= Al2 -Cast ('not' p) iff Jp,vp |= 'not' p ) )

assume A21: ( Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) ) ; :: thesis: ( J2,v2 |= Al2 -Cast ('not' p) iff Jp,vp |= 'not' p )

per cases
( not J2,v2 |= Al2 -Cast p or J2,v2 |= Al2 -Cast p )
;

end;

suppose A22:
not J2,v2 |= Al2 -Cast p
; :: thesis: ( J2,v2 |= Al2 -Cast ('not' p) iff Jp,vp |= 'not' p )

then A23:
not Jp,vp |= p
by A20, A21;

J2,v2 |= 'not' (Al2 -Cast p) by A22, VALUAT_1:17;

hence ( J2,v2 |= Al2 -Cast ('not' p) iff Jp,vp |= 'not' p ) by A23, VALUAT_1:17; :: thesis: verum

end;J2,v2 |= 'not' (Al2 -Cast p) by A22, VALUAT_1:17;

hence ( J2,v2 |= Al2 -Cast ('not' p) iff Jp,vp |= 'not' p ) by A23, VALUAT_1:17; :: thesis: verum

suppose A24:
J2,v2 |= Al2 -Cast p
; :: thesis: ( J2,v2 |= Al2 -Cast ('not' p) iff Jp,vp |= 'not' p )

then A25:
Jp,vp |= p
by A20, A21;

not J2,v2 |= 'not' (Al2 -Cast p) by VALUAT_1:17, A24;

hence ( J2,v2 |= Al2 -Cast ('not' p) iff Jp,vp |= 'not' p ) by A25, VALUAT_1:17; :: thesis: verum

end;not J2,v2 |= 'not' (Al2 -Cast p) by VALUAT_1:17, A24;

hence ( J2,v2 |= Al2 -Cast ('not' p) iff Jp,vp |= 'not' p ) by A25, VALUAT_1:17; :: thesis: verum

S

proof

A30:
for x being bound_QC-variable of Al
let p, r be Element of CQC-WFF Al; :: thesis: ( S_{1}[p] & S_{1}[r] implies S_{1}[p '&' r] )

assume A27: ( S_{1}[p] & S_{1}[r] )
; :: thesis: S_{1}[p '&' r]

let J2 be interpretation of Al2,A; :: thesis: for Jp being interpretation of Al,A

for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast (p '&' r) iff Jp,vp |= p '&' r )

let Jp be interpretation of Al,A; :: thesis: for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast (p '&' r) iff Jp,vp |= p '&' r )

let v2 be Element of Valuations_in (Al2,A); :: thesis: for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast (p '&' r) iff Jp,vp |= p '&' r )

let vp be Element of Valuations_in (Al,A); :: thesis: ( Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) implies ( J2,v2 |= Al2 -Cast (p '&' r) iff Jp,vp |= p '&' r ) )

assume A28: ( Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) ) ; :: thesis: ( J2,v2 |= Al2 -Cast (p '&' r) iff Jp,vp |= p '&' r )

A29: ( J2,v2 |= Al2 -Cast (p '&' r) implies Jp,vp |= p '&' r )

end;assume A27: ( S

let J2 be interpretation of Al2,A; :: thesis: for Jp being interpretation of Al,A

for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast (p '&' r) iff Jp,vp |= p '&' r )

let Jp be interpretation of Al,A; :: thesis: for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast (p '&' r) iff Jp,vp |= p '&' r )

let v2 be Element of Valuations_in (Al2,A); :: thesis: for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast (p '&' r) iff Jp,vp |= p '&' r )

let vp be Element of Valuations_in (Al,A); :: thesis: ( Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) implies ( J2,v2 |= Al2 -Cast (p '&' r) iff Jp,vp |= p '&' r ) )

assume A28: ( Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) ) ; :: thesis: ( J2,v2 |= Al2 -Cast (p '&' r) iff Jp,vp |= p '&' r )

A29: ( J2,v2 |= Al2 -Cast (p '&' r) implies Jp,vp |= p '&' r )

proof

( Jp,vp |= p '&' r implies J2,v2 |= Al2 -Cast (p '&' r) )
assume
J2,v2 |= Al2 -Cast (p '&' r)
; :: thesis: Jp,vp |= p '&' r

then J2,v2 |= (Al2 -Cast p) '&' (Al2 -Cast r) ;

then ( J2,v2 |= Al2 -Cast p & J2,v2 |= Al2 -Cast r ) by VALUAT_1:18;

then ( Jp,vp |= p & Jp,vp |= r ) by A27, A28;

hence Jp,vp |= p '&' r by VALUAT_1:18; :: thesis: verum

end;then J2,v2 |= (Al2 -Cast p) '&' (Al2 -Cast r) ;

then ( J2,v2 |= Al2 -Cast p & J2,v2 |= Al2 -Cast r ) by VALUAT_1:18;

then ( Jp,vp |= p & Jp,vp |= r ) by A27, A28;

hence Jp,vp |= p '&' r by VALUAT_1:18; :: thesis: verum

proof

hence
( J2,v2 |= Al2 -Cast (p '&' r) iff Jp,vp |= p '&' r )
by A29; :: thesis: verum
assume
Jp,vp |= p '&' r
; :: thesis: J2,v2 |= Al2 -Cast (p '&' r)

then ( Jp,vp |= p & Jp,vp |= r ) by VALUAT_1:18;

then ( J2,v2 |= Al2 -Cast p & J2,v2 |= Al2 -Cast r ) by A27, A28;

then J2,v2 |= (Al2 -Cast p) '&' (Al2 -Cast r) by VALUAT_1:18;

hence J2,v2 |= Al2 -Cast (p '&' r) ; :: thesis: verum

end;then ( Jp,vp |= p & Jp,vp |= r ) by VALUAT_1:18;

then ( J2,v2 |= Al2 -Cast p & J2,v2 |= Al2 -Cast r ) by A27, A28;

then J2,v2 |= (Al2 -Cast p) '&' (Al2 -Cast r) by VALUAT_1:18;

hence J2,v2 |= Al2 -Cast (p '&' r) ; :: thesis: verum

for r being Element of CQC-WFF Al st S

S

proof

A59:
for r, s being Element of CQC-WFF Al
let x be bound_QC-variable of Al; :: thesis: for r being Element of CQC-WFF Al st S_{1}[r] holds

S_{1}[ All (x,r)]

let r be Element of CQC-WFF Al; :: thesis: ( S_{1}[r] implies S_{1}[ All (x,r)] )

assume A31: S_{1}[r]
; :: thesis: S_{1}[ All (x,r)]

let J2 be interpretation of Al2,A; :: thesis: for Jp being interpretation of Al,A

for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast (All (x,r)) iff Jp,vp |= All (x,r) )

let Jp be interpretation of Al,A; :: thesis: for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast (All (x,r)) iff Jp,vp |= All (x,r) )

let v2 be Element of Valuations_in (Al2,A); :: thesis: for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast (All (x,r)) iff Jp,vp |= All (x,r) )

let vp be Element of Valuations_in (Al,A); :: thesis: ( Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) implies ( J2,v2 |= Al2 -Cast (All (x,r)) iff Jp,vp |= All (x,r) ) )

assume A32: ( Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) ) ; :: thesis: ( J2,v2 |= Al2 -Cast (All (x,r)) iff Jp,vp |= All (x,r) )

A33: ( J2,v2 |= Al2 -Cast (All (x,r)) implies Jp,vp |= All (x,r) )

end;S

let r be Element of CQC-WFF Al; :: thesis: ( S

assume A31: S

let J2 be interpretation of Al2,A; :: thesis: for Jp being interpretation of Al,A

for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast (All (x,r)) iff Jp,vp |= All (x,r) )

let Jp be interpretation of Al,A; :: thesis: for v2 being Element of Valuations_in (Al2,A)

for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast (All (x,r)) iff Jp,vp |= All (x,r) )

let v2 be Element of Valuations_in (Al2,A); :: thesis: for vp being Element of Valuations_in (Al,A) st Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) holds

( J2,v2 |= Al2 -Cast (All (x,r)) iff Jp,vp |= All (x,r) )

let vp be Element of Valuations_in (Al,A); :: thesis: ( Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) implies ( J2,v2 |= Al2 -Cast (All (x,r)) iff Jp,vp |= All (x,r) ) )

assume A32: ( Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) ) ; :: thesis: ( J2,v2 |= Al2 -Cast (All (x,r)) iff Jp,vp |= All (x,r) )

A33: ( J2,v2 |= Al2 -Cast (All (x,r)) implies Jp,vp |= All (x,r) )

proof

( Jp,vp |= All (x,r) implies J2,v2 |= Al2 -Cast (All (x,r)) )
assume
J2,v2 |= Al2 -Cast (All (x,r))
; :: thesis: Jp,vp |= All (x,r)

then A34: J2,v2 |= All ((Al2 -Cast x),(Al2 -Cast r)) ;

for vp1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds

vp1 . y = vp . y ) holds

Jp,vp1 |= r

end;then A34: J2,v2 |= All ((Al2 -Cast x),(Al2 -Cast r)) ;

for vp1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds

vp1 . y = vp . y ) holds

Jp,vp1 |= r

proof

hence
Jp,vp |= All (x,r)
by VALUAT_1:29; :: thesis: verum
let vp1 be Element of Valuations_in (Al,A); :: thesis: ( ( for y being bound_QC-variable of Al st x <> y holds

vp1 . y = vp . y ) implies Jp,vp1 |= r )

assume A35: for y being bound_QC-variable of Al st x <> y holds

vp1 . y = vp . y ; :: thesis: Jp,vp1 |= r

set s = (Al2 -Cast x) .--> (vp1 . x);

A36: (Al2 -Cast x) .--> (vp1 . x) = {(Al2 -Cast x)} --> (vp1 . x) by FUNCOP_1:def 9;

set v21 = v2 +* ((Al2 -Cast x) .--> (vp1 . x));

v2 is Element of Funcs ((bound_QC-variables Al2),A) by VALUAT_1:def 1;

then A37: ( dom v2 = bound_QC-variables Al2 & rng v2 c= A ) by FUNCT_2:92;

dom ((Al2 -Cast x) .--> (vp1 . x)) = {(Al2 -Cast x)} by A36;

then dom (v2 +* ((Al2 -Cast x) .--> (vp1 . x))) = (dom v2) \/ {(Al2 -Cast x)} by FUNCT_4:def 1;

then A38: dom (v2 +* ((Al2 -Cast x) .--> (vp1 . x))) = bound_QC-variables Al2 by A37, XBOOLE_1:12;

A39: (rng v2) \/ {(vp1 . x)} c= A by A37, XBOOLE_1:8;

rng ((Al2 -Cast x) .--> (vp1 . x)) = {(vp1 . x)} by A36, FUNCOP_1:8;

then rng (v2 +* ((Al2 -Cast x) .--> (vp1 . x))) c= (rng v2) \/ {(vp1 . x)} by FUNCT_4:17;

then rng (v2 +* ((Al2 -Cast x) .--> (vp1 . x))) c= A by A39;

then v2 +* ((Al2 -Cast x) .--> (vp1 . x)) is Element of Funcs ((bound_QC-variables Al2),A) by A38, FUNCT_2:def 2;

then reconsider v21 = v2 +* ((Al2 -Cast x) .--> (vp1 . x)) as Element of Valuations_in (Al2,A) by VALUAT_1:def 1;

for y being bound_QC-variable of Al2 st Al2 -Cast x <> y holds

v21 . y = v2 . y by FUNCT_4:83;

then A40: J2,v21 |= Al2 -Cast r by A34, VALUAT_1:29;

vp1 is Element of Funcs ((bound_QC-variables Al),A) by VALUAT_1:def 1;

then A41: dom vp1 = bound_QC-variables Al by FUNCT_2:92

.= (dom v21) /\ (bound_QC-variables Al) by A38, Th4, XBOOLE_1:28 ;

for c being object st c in dom vp1 holds

vp1 . c = v21 . c

hence Jp,vp1 |= r by A32, A31, A40; :: thesis: verum

end;vp1 . y = vp . y ) implies Jp,vp1 |= r )

assume A35: for y being bound_QC-variable of Al st x <> y holds

vp1 . y = vp . y ; :: thesis: Jp,vp1 |= r

set s = (Al2 -Cast x) .--> (vp1 . x);

A36: (Al2 -Cast x) .--> (vp1 . x) = {(Al2 -Cast x)} --> (vp1 . x) by FUNCOP_1:def 9;

set v21 = v2 +* ((Al2 -Cast x) .--> (vp1 . x));

v2 is Element of Funcs ((bound_QC-variables Al2),A) by VALUAT_1:def 1;

then A37: ( dom v2 = bound_QC-variables Al2 & rng v2 c= A ) by FUNCT_2:92;

dom ((Al2 -Cast x) .--> (vp1 . x)) = {(Al2 -Cast x)} by A36;

then dom (v2 +* ((Al2 -Cast x) .--> (vp1 . x))) = (dom v2) \/ {(Al2 -Cast x)} by FUNCT_4:def 1;

then A38: dom (v2 +* ((Al2 -Cast x) .--> (vp1 . x))) = bound_QC-variables Al2 by A37, XBOOLE_1:12;

A39: (rng v2) \/ {(vp1 . x)} c= A by A37, XBOOLE_1:8;

rng ((Al2 -Cast x) .--> (vp1 . x)) = {(vp1 . x)} by A36, FUNCOP_1:8;

then rng (v2 +* ((Al2 -Cast x) .--> (vp1 . x))) c= (rng v2) \/ {(vp1 . x)} by FUNCT_4:17;

then rng (v2 +* ((Al2 -Cast x) .--> (vp1 . x))) c= A by A39;

then v2 +* ((Al2 -Cast x) .--> (vp1 . x)) is Element of Funcs ((bound_QC-variables Al2),A) by A38, FUNCT_2:def 2;

then reconsider v21 = v2 +* ((Al2 -Cast x) .--> (vp1 . x)) as Element of Valuations_in (Al2,A) by VALUAT_1:def 1;

for y being bound_QC-variable of Al2 st Al2 -Cast x <> y holds

v21 . y = v2 . y by FUNCT_4:83;

then A40: J2,v21 |= Al2 -Cast r by A34, VALUAT_1:29;

vp1 is Element of Funcs ((bound_QC-variables Al),A) by VALUAT_1:def 1;

then A41: dom vp1 = bound_QC-variables Al by FUNCT_2:92

.= (dom v21) /\ (bound_QC-variables Al) by A38, Th4, XBOOLE_1:28 ;

for c being object st c in dom vp1 holds

vp1 . c = v21 . c

proof

then
v21 | (bound_QC-variables Al) = vp1
by FUNCT_1:46, A41;
let c be object ; :: thesis: ( c in dom vp1 implies vp1 . c = v21 . c )

assume A42: c in dom vp1 ; :: thesis: vp1 . c = v21 . c

end;assume A42: c in dom vp1 ; :: thesis: vp1 . c = v21 . c

per cases
( c = Al2 -Cast x or c <> Al2 -Cast x )
;

end;

suppose A43:
c = Al2 -Cast x
; :: thesis: vp1 . c = v21 . c

then
c in dom ((Al2 -Cast x) .--> (vp1 . x))
by FUNCOP_1:74;

hence v21 . c = ((Al2 -Cast x) .--> (vp1 . x)) . c by FUNCT_4:13

.= vp1 . c by A43, FUNCOP_1:72 ;

:: thesis: verum

end;hence v21 . c = ((Al2 -Cast x) .--> (vp1 . x)) . c by FUNCT_4:13

.= vp1 . c by A43, FUNCOP_1:72 ;

:: thesis: verum

suppose A44:
c <> Al2 -Cast x
; :: thesis: vp1 . c = v21 . c

reconsider c = c as bound_QC-variable of Al by A41, A42, XBOOLE_0:def 4;

v21 . c = v2 . c by A44, FUNCT_4:83

.= (v2 | (bound_QC-variables Al)) . c by FUNCT_1:49

.= vp1 . c by A32, A35, A44 ;

hence vp1 . c = v21 . c ; :: thesis: verum

end;v21 . c = v2 . c by A44, FUNCT_4:83

.= (v2 | (bound_QC-variables Al)) . c by FUNCT_1:49

.= vp1 . c by A32, A35, A44 ;

hence vp1 . c = v21 . c ; :: thesis: verum

hence Jp,vp1 |= r by A32, A31, A40; :: thesis: verum

proof

hence
( J2,v2 |= Al2 -Cast (All (x,r)) iff Jp,vp |= All (x,r) )
by A33; :: thesis: verum
assume A45:
Jp,vp |= All (x,r)
; :: thesis: J2,v2 |= Al2 -Cast (All (x,r))

for v21 being Element of Valuations_in (Al2,A) st ( for y being bound_QC-variable of Al2 st Al2 -Cast x <> y holds

v21 . y = v2 . y ) holds

J2,v21 |= Al2 -Cast r

hence J2,v2 |= Al2 -Cast (All (x,r)) ; :: thesis: verum

end;for v21 being Element of Valuations_in (Al2,A) st ( for y being bound_QC-variable of Al2 st Al2 -Cast x <> y holds

v21 . y = v2 . y ) holds

J2,v21 |= Al2 -Cast r

proof

then
J2,v2 |= All ((Al2 -Cast x),(Al2 -Cast r))
by VALUAT_1:29;
let v21 be Element of Valuations_in (Al2,A); :: thesis: ( ( for y being bound_QC-variable of Al2 st Al2 -Cast x <> y holds

v21 . y = v2 . y ) implies J2,v21 |= Al2 -Cast r )

assume A46: for y being bound_QC-variable of Al2 st Al2 -Cast x <> y holds

v21 . y = v2 . y ; :: thesis: J2,v21 |= Al2 -Cast r

set s = x .--> (v21 . (Al2 -Cast x));

A47: x .--> (v21 . (Al2 -Cast x)) = {x} --> (v21 . (Al2 -Cast x)) by FUNCOP_1:def 9;

set vp1 = vp +* (x .--> (v21 . (Al2 -Cast x)));

vp is Element of Funcs ((bound_QC-variables Al),A) by VALUAT_1:def 1;

then A48: ( dom vp = bound_QC-variables Al & rng vp c= A ) by FUNCT_2:92;

dom (x .--> (v21 . (Al2 -Cast x))) = {x} by A47;

then dom (vp +* (x .--> (v21 . (Al2 -Cast x)))) = (dom vp) \/ {x} by FUNCT_4:def 1;

then A49: dom (vp +* (x .--> (v21 . (Al2 -Cast x)))) = bound_QC-variables Al by A48, XBOOLE_1:12;

A50: (rng vp) \/ {(v21 . (Al2 -Cast x))} c= A by A48, XBOOLE_1:8;

rng (x .--> (v21 . (Al2 -Cast x))) = {(v21 . (Al2 -Cast x))} by A47, FUNCOP_1:8;

then rng (vp +* (x .--> (v21 . (Al2 -Cast x)))) c= (rng vp) \/ {(v21 . (Al2 -Cast x))} by FUNCT_4:17;

then rng (vp +* (x .--> (v21 . (Al2 -Cast x)))) c= A by A50;

then vp +* (x .--> (v21 . (Al2 -Cast x))) is Element of Funcs ((bound_QC-variables Al),A) by A49, FUNCT_2:def 2;

then reconsider vp1 = vp +* (x .--> (v21 . (Al2 -Cast x))) as Element of Valuations_in (Al,A) by VALUAT_1:def 1;

for y being bound_QC-variable of Al st x <> y holds

vp1 . y = vp . y by FUNCT_4:83;

then A51: Jp,vp1 |= r by A45, VALUAT_1:29;

v21 is Element of Funcs ((bound_QC-variables Al2),A) by VALUAT_1:def 1;

then A52: dom v21 = bound_QC-variables Al2 by FUNCT_2:92;

vp1 is Element of Funcs ((bound_QC-variables Al),A) by VALUAT_1:def 1;

then A53: dom vp1 = bound_QC-variables Al by FUNCT_2:92

.= (dom v21) /\ (bound_QC-variables Al) by A52, Th4, XBOOLE_1:28 ;

for c being object st c in dom vp1 holds

vp1 . c = v21 . c

hence J2,v21 |= Al2 -Cast r by A32, A31, A51; :: thesis: verum

end;v21 . y = v2 . y ) implies J2,v21 |= Al2 -Cast r )

assume A46: for y being bound_QC-variable of Al2 st Al2 -Cast x <> y holds

v21 . y = v2 . y ; :: thesis: J2,v21 |= Al2 -Cast r

set s = x .--> (v21 . (Al2 -Cast x));

A47: x .--> (v21 . (Al2 -Cast x)) = {x} --> (v21 . (Al2 -Cast x)) by FUNCOP_1:def 9;

set vp1 = vp +* (x .--> (v21 . (Al2 -Cast x)));

vp is Element of Funcs ((bound_QC-variables Al),A) by VALUAT_1:def 1;

then A48: ( dom vp = bound_QC-variables Al & rng vp c= A ) by FUNCT_2:92;

dom (x .--> (v21 . (Al2 -Cast x))) = {x} by A47;

then dom (vp +* (x .--> (v21 . (Al2 -Cast x)))) = (dom vp) \/ {x} by FUNCT_4:def 1;

then A49: dom (vp +* (x .--> (v21 . (Al2 -Cast x)))) = bound_QC-variables Al by A48, XBOOLE_1:12;

A50: (rng vp) \/ {(v21 . (Al2 -Cast x))} c= A by A48, XBOOLE_1:8;

rng (x .--> (v21 . (Al2 -Cast x))) = {(v21 . (Al2 -Cast x))} by A47, FUNCOP_1:8;

then rng (vp +* (x .--> (v21 . (Al2 -Cast x)))) c= (rng vp) \/ {(v21 . (Al2 -Cast x))} by FUNCT_4:17;

then rng (vp +* (x .--> (v21 . (Al2 -Cast x)))) c= A by A50;

then vp +* (x .--> (v21 . (Al2 -Cast x))) is Element of Funcs ((bound_QC-variables Al),A) by A49, FUNCT_2:def 2;

then reconsider vp1 = vp +* (x .--> (v21 . (Al2 -Cast x))) as Element of Valuations_in (Al,A) by VALUAT_1:def 1;

for y being bound_QC-variable of Al st x <> y holds

vp1 . y = vp . y by FUNCT_4:83;

then A51: Jp,vp1 |= r by A45, VALUAT_1:29;

v21 is Element of Funcs ((bound_QC-variables Al2),A) by VALUAT_1:def 1;

then A52: dom v21 = bound_QC-variables Al2 by FUNCT_2:92;

vp1 is Element of Funcs ((bound_QC-variables Al),A) by VALUAT_1:def 1;

then A53: dom vp1 = bound_QC-variables Al by FUNCT_2:92

.= (dom v21) /\ (bound_QC-variables Al) by A52, Th4, XBOOLE_1:28 ;

for c being object st c in dom vp1 holds

vp1 . c = v21 . c

proof

then
v21 | (bound_QC-variables Al) = vp1
by FUNCT_1:46, A53;
let c be object ; :: thesis: ( c in dom vp1 implies vp1 . c = v21 . c )

assume A54: c in dom vp1 ; :: thesis: vp1 . c = v21 . c

end;assume A54: c in dom vp1 ; :: thesis: vp1 . c = v21 . c

per cases
( c = x or c <> x )
;

end;

suppose A55:
c = x
; :: thesis: vp1 . c = v21 . c

then
c in dom (x .--> (v21 . (Al2 -Cast x)))
by FUNCOP_1:74;

then vp1 . c = (x .--> (v21 . (Al2 -Cast x))) . x by A55, FUNCT_4:13

.= v21 . c by A55, FUNCOP_1:72 ;

hence vp1 . c = v21 . c ; :: thesis: verum

end;then vp1 . c = (x .--> (v21 . (Al2 -Cast x))) . x by A55, FUNCT_4:13

.= v21 . c by A55, FUNCOP_1:72 ;

hence vp1 . c = v21 . c ; :: thesis: verum

suppose A56:
c <> x
; :: thesis: vp1 . c = v21 . c

A57:
c in bound_QC-variables Al
by A53, A54, XBOOLE_0:def 4;

vp1 is Element of Funcs ((bound_QC-variables Al),A) by VALUAT_1:def 1;

then dom vp1 = bound_QC-variables Al by FUNCT_2:92;

then A58: dom vp1 c= bound_QC-variables Al2 by Th4;

vp1 . c = vp . c by A56, FUNCT_4:83

.= v2 . c by A32, A57, FUNCT_1:49

.= v21 . c by A56, A46, A54, A58 ;

hence vp1 . c = v21 . c ; :: thesis: verum

end;vp1 is Element of Funcs ((bound_QC-variables Al),A) by VALUAT_1:def 1;

then dom vp1 = bound_QC-variables Al by FUNCT_2:92;

then A58: dom vp1 c= bound_QC-variables Al2 by Th4;

vp1 . c = vp . c by A56, FUNCT_4:83

.= v2 . c by A32, A57, FUNCT_1:49

.= v21 . c by A56, A46, A54, A58 ;

hence vp1 . c = v21 . c ; :: thesis: verum

hence J2,v21 |= Al2 -Cast r by A32, A31, A51; :: thesis: verum

hence J2,v2 |= Al2 -Cast (All (x,r)) ; :: thesis: verum

for x being bound_QC-variable of Al

for k being Nat

for l being CQC-variable_list of k,Al

for P being QC-pred_symbol of k,Al holds

( S

for r being Element of CQC-WFF Al holds S

hence ( Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) implies ( J2,v2 |= Al2 -Cast r iff Jp,vp |= r ) ) ; :: thesis: verum