let Al be QC-alphabet ; :: thesis:
let r be Element of CQC-WFF Al; :: thesis:
let A be non empty set ; :: thesis:
let Al2 be Al -expanding QC-alphabet ; :: thesis:
let J2 be interpretation of Al2,A; :: thesis:
let Jp be interpretation of Al,A; :: thesis:
let v2 be Element of Valuations_in (Al2,A); :: thesis:
let vp be Element of Valuations_in (Al,A); :: thesis:
defpred S₁[ 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₁[ VERUM Al]

let J2 be interpretation of Al2,A; :: thesis:
let Jp be interpretation of Al,A; :: thesis:
let v2 be Element of Valuations_in (Al2,A); :: thesis:
let vp be Element of Valuations_in (Al,A); :: thesis:
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:

end;

A2: for k being Nat
for P being QC-pred_symbol of k,Al
for l being CQC-variable_list of k,Al holds S₁[P ! l]

proof

let k be Nat; :: thesis:
let P be QC-pred_symbol of k,Al; :: thesis:
let l be CQC-variable_list of k,Al; :: thesis:
let J2 be interpretation of Al2,A; :: thesis:
let Jp be interpretation of Al,A; :: thesis:
let v2 be Element of Valuations_in (Al2,A); :: thesis:
let vp be Element of Valuations_in (Al,A); :: thesis:
assume A3: ( Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) ) ; :: thesis:
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

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 )

proof

let j be Nat; :: thesis:
assume A10: ( 1 <= j & j <= len l ) ; :: thesis:
thus ( l . j in bound_QC-variables Al implies l . j in bound_QC-variables Al2 ) by A8; :: thesis:

hereby :: thesis:

assume l . j in bound_QC-variables Al2 ; :: thesis:
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:

end;

set t1 = { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al ) } ;
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

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:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al ) } ; :: thesis:
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:

end;

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:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables Al2 ) } ; :: thesis:
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:

end;

A14: still_not-bound_in l = still_not-bound_in l2 by A5, A11;
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:

end;

A16: ( J2,v2 |= Al2 -Cast (P ! l) implies Jp,vp |= P ! l )

proof

assume J2,v2 |= Al2 -Cast (P ! l) ; :: thesis:
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:

end;

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

proof

assume not J2,v2 |= Al2 -Cast (P ! l) ; :: thesis:
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:

end;

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

end;

A19: for p being Element of CQC-WFF Al st S₁[p] holds
S₁[ 'not' p]

proof

let p be Element of CQC-WFF Al; :: thesis:
assume A20: S₁[p] ; :: thesis:
let J2 be interpretation of Al2,A; :: thesis:
let Jp be interpretation of Al,A; :: thesis:
let v2 be Element of Valuations_in (Al2,A); :: thesis:
let vp be Element of Valuations_in (Al,A); :: thesis:
assume A21: ( Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) ) ; :: thesis:

per cases ;

suppose A22: not J2,v2 |= Al2 -Cast p ; :: thesis:

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:

end;

suppose A24: J2,v2 |= Al2 -Cast p ; :: thesis:

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:

end;

A26: for p, r being Element of CQC-WFF Al st S₁[p] & S₁[r] holds
S₁[p '&' r]

proof

let p, r be Element of CQC-WFF Al; :: thesis:
assume A27: ( S₁[p] & S₁[r] ) ; :: thesis:
let J2 be interpretation of Al2,A; :: thesis:
let Jp be interpretation of Al,A; :: thesis:
let v2 be Element of Valuations_in (Al2,A); :: thesis:
let vp be Element of Valuations_in (Al,A); :: thesis:
assume A28: ( Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) ) ; :: thesis:
A29: ( J2,v2 |= Al2 -Cast (p '&' r) implies Jp,vp |= p '&' r )

proof

end;

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

proof

end;

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

end;

A30: for x being bound_QC-variable of Al
for r being Element of CQC-WFF Al st S₁[r] holds
S₁[ All (x,r)]

proof

let x be bound_QC-variable of Al; :: thesis:
let r be Element of CQC-WFF Al; :: thesis:
assume A31: S₁[r] ; :: thesis:
let J2 be interpretation of Al2,A; :: thesis:
let Jp be interpretation of Al,A; :: thesis:
let v2 be Element of Valuations_in (Al2,A); :: thesis:
let vp be Element of Valuations_in (Al,A); :: thesis:
assume A32: ( Jp = J2 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) ) ; :: thesis:
A33: ( J2,v2 |= Al2 -Cast (All (x,r)) implies Jp,vp |= All (x,r) )

proof

assume J2,v2 |= Al2 -Cast (All (x,r)) ; :: thesis:
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

proof

let c be object ; :: thesis:
assume A42: c in dom vp1 ; :: thesis:

per cases ;

suppose A43: c = Al2 -Cast x ; :: thesis:

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:

end;

suppose A44: c <> Al2 -Cast x ; :: thesis:

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:

end;

then v21 | (bound_QC-variables Al) = vp1 by FUNCT_1:46, A41;
hence Jp,vp1 |= r by A32, A31, A40; :: thesis:

end;

hence Jp,vp |= All (x,r) by VALUAT_1:29; :: thesis:

end;

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

proof

assume A45: Jp,vp |= All (x,r) ; :: thesis:
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

proof

let c be object ; :: thesis:
assume A54: c in dom vp1 ; :: thesis:

per cases ;

suppose A55: c = x ; :: thesis:

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:

end;

suppose A56: c <> x ; :: thesis:

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:

end;

then v21 | (bound_QC-variables Al) = vp1 by FUNCT_1:46, A53;
hence J2,v21 |= Al2 -Cast r by A32, A31, A51; :: thesis:

end;

then J2,v2 |= All ((Al2 -Cast x),(Al2 -Cast r)) by VALUAT_1:29;
hence J2,v2 |= Al2 -Cast (All (x,r)) ; :: thesis:

end;

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

end;

A59: for r, s being Element of CQC-WFF Al
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₁[ VERUM Al] & S₁[P ! l] & ( S₁[r] implies S₁[ 'not' r] ) & ( S₁[r] & S₁[s] implies S₁[r '&' s] ) & ( S₁[r] implies S₁[ All (x,r)] ) ) by A1, A2, A19, A26, A30;
for r being Element of CQC-WFF Al holds S₁[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: