let Al be QC-alphabet ; :: thesis: for Al2 being Al -expanding QC-alphabet
for p2 being Element of CQC-WFF Al2
for x2, y2 being bound_QC-variable of Al2
for p being Element of CQC-WFF Al
for x, y being bound_QC-variable of Al st p = p2 & x = x2 & y = y2 holds
p . (x,y) = p2 . (x2,y2)
let Al2 be Al -expanding QC-alphabet ; :: thesis: for p2 being Element of CQC-WFF Al2
for x2, y2 being bound_QC-variable of Al2
for p being Element of CQC-WFF Al
for x, y being bound_QC-variable of Al st p = p2 & x = x2 & y = y2 holds
p . (x,y) = p2 . (x2,y2)
defpred S1[ Element of CQC-WFF Al] means for p2 being Element of CQC-WFF Al2
for S being CQC_Substitution of Al
for S2 being CQC_Substitution of Al2 st $1 = p2 & S = S2 holds
CQC_Sub [$1,S] = CQC_Sub [p2,S2];
A1: S1[ VERUM Al]
proof
set p = VERUM Al;
let p2 be Element of CQC-WFF Al2; :: thesis: for S being CQC_Substitution of Al
for S2 being CQC_Substitution of Al2 st VERUM Al = p2 & S = S2 holds
CQC_Sub [(VERUM Al),S] = CQC_Sub [p2,S2]
let S be CQC_Substitution of Al; :: thesis: for S2 being CQC_Substitution of Al2 st VERUM Al = p2 & S = S2 holds
CQC_Sub [(VERUM Al),S] = CQC_Sub [p2,S2]
let S2 be CQC_Substitution of Al2; :: thesis: ( VERUM Al = p2 & S = S2 implies CQC_Sub [(VERUM Al),S] = CQC_Sub [p2,S2] )
assume A2: ( VERUM Al = p2 & S = S2 ) ; :: thesis: CQC_Sub [(VERUM Al),S] = CQC_Sub [p2,S2]
A3: VERUM Al2 = p2 by A2;
A4: ( [(VERUM Al),S] is Al -Sub_VERUM & [p2,S2] is Al2 -Sub_VERUM ) by A3, SUBSTUT1:def 19;
thus CQC_Sub [(VERUM Al),S] = VERUM Al2 by A4, SUBLEMMA:3
.= CQC_Sub [p2,S2] by A4, SUBLEMMA:3 ; :: thesis: verum
end;
A5: for k being Nat
for P being QC-pred_symbol of k,Al
for l being CQC-variable_list of k,Al holds S1[P ! l]
proof
let k be Nat; :: thesis: for P being QC-pred_symbol of k,Al
for l being CQC-variable_list of k,Al holds S1[P ! l]
let P be QC-pred_symbol of k,Al; :: thesis: for l being CQC-variable_list of k,Al holds S1[P ! l]
let l be CQC-variable_list of k,Al; :: thesis: S1[P ! l]
set P2 = Al2 -Cast P;
set l2 = Al2 -Cast l;
reconsider P2 = Al2 -Cast P as QC-pred_symbol of k,Al2 ;
reconsider l2 = Al2 -Cast l as CQC-variable_list of k,Al2 ;
let p2 be Element of CQC-WFF Al2; :: thesis: for S being CQC_Substitution of Al
for S2 being CQC_Substitution of Al2 st P ! l = p2 & S = S2 holds
CQC_Sub [(P ! l),S] = CQC_Sub [p2,S2]
let S be CQC_Substitution of Al; :: thesis: for S2 being CQC_Substitution of Al2 st P ! l = p2 & S = S2 holds
CQC_Sub [(P ! l),S] = CQC_Sub [p2,S2]
let S2 be CQC_Substitution of Al2; :: thesis: ( P ! l = p2 & S = S2 implies CQC_Sub [(P ! l),S] = CQC_Sub [p2,S2] )
assume A6: ( P ! l = p2 & S = S2 ) ; :: thesis: CQC_Sub [(P ! l),S] = CQC_Sub [p2,S2]
A7: p2 = Al2 -Cast (P ! l) by A6
.= P2 ! l2 by Th8 ;
set p = P ! l;
reconsider p = P ! l as Element of CQC-WFF Al ;
set sub = CQC_Subst (l,S);
A8: CQC_Subst (l,S) = CQC_Subst ((Al2 -Cast l),S2)
proof
A9: len (CQC_Subst (l,S)) = len l by SUBSTUT1:def 3
.= len (CQC_Subst ((Al2 -Cast l),S2)) by SUBSTUT1:def 3 ;
for n being Nat st n in dom (CQC_Subst (l,S)) holds
(CQC_Subst (l,S)) . n = (CQC_Subst ((Al2 -Cast l),S2)) . n
proof
let n be Nat; :: thesis: ( n in dom (CQC_Subst (l,S)) implies (CQC_Subst (l,S)) . n = (CQC_Subst ((Al2 -Cast l),S2)) . n )
assume A10: n in dom (CQC_Subst (l,S)) ; :: thesis: (CQC_Subst (l,S)) . n = (CQC_Subst ((Al2 -Cast l),S2)) . n
n in Seg (len (CQC_Subst (l,S))) by A10, FINSEQ_1:def 3;
then ( 1 <= n & n <= len (CQC_Subst (l,S)) ) by FINSEQ_1:1;
then A11: ( 1 <= n & n <= len l ) by SUBSTUT1:def 3;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
per cases ( l . n in dom S or not l . n in dom S ) ;
suppose A12: l . n in dom S ; :: thesis: (CQC_Subst (l,S)) . n = (CQC_Subst ((Al2 -Cast l),S2)) . n
(CQC_Subst (l,S)) . n = S . (l . n) by A11, A12, SUBSTUT1:def 3
.= (CQC_Subst ((Al2 -Cast l),S2)) . n by A6, A11, A12, SUBSTUT1:def 3 ;
hence (CQC_Subst (l,S)) . n = (CQC_Subst ((Al2 -Cast l),S2)) . n ; :: thesis: verum
end;
suppose A13: not l . n in dom S ; :: thesis: (CQC_Subst (l,S)) . n = (CQC_Subst ((Al2 -Cast l),S2)) . n
(CQC_Subst (l,S)) . n = l . n by A11, A13, SUBSTUT1:def 3
.= (CQC_Subst ((Al2 -Cast l),S2)) . n by A6, A11, A13, SUBSTUT1:def 3 ;
hence (CQC_Subst (l,S)) . n = (CQC_Subst ((Al2 -Cast l),S2)) . n ; :: thesis: verum
end;
end;
end;
hence CQC_Subst (l,S) = CQC_Subst ((Al2 -Cast l),S2) by A9, FINSEQ_2:9; :: thesis: verum
end;
( the_arity_of P = len l & the_arity_of P2 = len l2 ) by Th1;
then A14: ( [(P ! l),S] = Sub_P (P,l,S) & [(P2 ! l2),S2] = Sub_P (P2,l2,S2) ) by SUBSTUT1:def 18;
( P ! l is atomic & P2 ! l2 is atomic ) ;
then A15: ( P = the_pred_symbol_of (P ! l) & P2 = the_pred_symbol_of (P2 ! l2) ) by QC_LANG1:def 22;
A16: ( [(P ! l),S] `1 = P ! l & [(P ! l),S] `2 = S & [(P2 ! l2),S2] `1 = P2 ! l2 & [(P2 ! l2),S2] `2 = S2 & Sub_the_arguments_of [(P ! l),S] = l & Sub_the_arguments_of [(P2 ! l2),S2] = l2 ) by A14, SUBSTUT1:def 29;
thus CQC_Sub [(P ! l),S] = Al2 -Cast (P ! (CQC_Subst (l,S))) by A14, A15, A16, SUBLEMMA:6
.= (Al2 -Cast P) ! (Al2 -Cast (CQC_Subst (l,S))) by Th8
.= CQC_Sub [p2,S2] by A7, A8, A14, A15, A16, SUBLEMMA:6 ; :: thesis: verum
end;
A17: for q being Element of CQC-WFF Al st S1[q] holds
S1[ 'not' q]
proof
let q be Element of CQC-WFF Al; :: thesis: ( S1[q] implies S1[ 'not' q] )
assume A18: S1[q] ; :: thesis: S1[ 'not' q]
set p = 'not' q;
reconsider p = 'not' q as Element of CQC-WFF Al ;
set q2 = Al2 -Cast q;
reconsider q2 = Al2 -Cast q as Element of CQC-WFF Al2 ;
let p2 be Element of CQC-WFF Al2; :: thesis: for S being CQC_Substitution of Al
for S2 being CQC_Substitution of Al2 st 'not' q = p2 & S = S2 holds
CQC_Sub [('not' q),S] = CQC_Sub [p2,S2]
let S be CQC_Substitution of Al; :: thesis: for S2 being CQC_Substitution of Al2 st 'not' q = p2 & S = S2 holds
CQC_Sub [('not' q),S] = CQC_Sub [p2,S2]
let S2 be CQC_Substitution of Al2; :: thesis: ( 'not' q = p2 & S = S2 implies CQC_Sub [('not' q),S] = CQC_Sub [p2,S2] )
assume A19: ( 'not' q = p2 & S = S2 ) ; :: thesis: CQC_Sub [('not' q),S] = CQC_Sub [p2,S2]
A20: ( [q,S] `1 = q & [q,S] `2 = S & [q2,S2] `1 = q2 & [q2,S2] `2 = S2 ) ;
thus CQC_Sub [('not' q),S] = CQC_Sub (Sub_not [q,S]) by A20, SUBSTUT1:def 20
.= Al2 -Cast ('not' (CQC_Sub [q,S])) by SUBSTUT1:29
.= 'not' (CQC_Sub [q2,S2]) by A18, A19
.= CQC_Sub (Sub_not [q2,S2]) by SUBSTUT1:29
.= CQC_Sub [('not' q2),S2] by A20, SUBSTUT1:def 20
.= CQC_Sub [p2,S2] by A19 ; :: thesis: verum
end;
A21: for r, s being Element of CQC-WFF Al st S1[r] & S1[s] holds
S1[r '&' s]
proof
let r, s be Element of CQC-WFF Al; :: thesis: ( S1[r] & S1[s] implies S1[r '&' s] )
assume A22: ( S1[r] & S1[s] ) ; :: thesis: S1[r '&' s]
set r2 = Al2 -Cast r;
set s2 = Al2 -Cast s;
reconsider r2 = Al2 -Cast r, s2 = Al2 -Cast s as Element of CQC-WFF Al2 ;
let p2 be Element of CQC-WFF Al2; :: thesis: for S being CQC_Substitution of Al
for S2 being CQC_Substitution of Al2 st r '&' s = p2 & S = S2 holds
CQC_Sub [(r '&' s),S] = CQC_Sub [p2,S2]
let S be CQC_Substitution of Al; :: thesis: for S2 being CQC_Substitution of Al2 st r '&' s = p2 & S = S2 holds
CQC_Sub [(r '&' s),S] = CQC_Sub [p2,S2]
let S2 be CQC_Substitution of Al2; :: thesis: ( r '&' s = p2 & S = S2 implies CQC_Sub [(r '&' s),S] = CQC_Sub [p2,S2] )
assume A23: ( r '&' s = p2 & S = S2 ) ; :: thesis: CQC_Sub [(r '&' s),S] = CQC_Sub [p2,S2]
A24: ( CQC_Sub [r,S] = CQC_Sub [r2,S2] & CQC_Sub [s,S] = CQC_Sub [s2,S2] ) by A22, A23;
A25: ( [r,S] `1 = r & [r,S] `2 = S & [s,S] `1 = s & [s,S] `2 = S & [r2,S2] `1 = r2 & [r2,S2] `2 = S2 & [s2,S2] `1 = s2 & [s2,S2] `2 = S2 ) ;
thus CQC_Sub [(r '&' s),S] = CQC_Sub (CQCSub_& ([r,S],[s,S])) by SUBSTUT2:19
.= Al2 -Cast ((CQC_Sub [r,S]) '&' (CQC_Sub [s,S])) by A25, SUBLEMMA:23
.= (Al2 -Cast (CQC_Sub [r,S])) '&' (Al2 -Cast (CQC_Sub [s,S]))
.= CQC_Sub (CQCSub_& ([r2,S2],[s2,S2])) by A24, A25, SUBLEMMA:23
.= CQC_Sub [(r2 '&' s2),S2] by SUBSTUT2:19
.= CQC_Sub [p2,S2] by A23 ; :: thesis: verum
end;
for z being bound_QC-variable of Al
for q being Element of CQC-WFF Al st S1[q] holds
S1[ All (z,q)]
proof
let z be bound_QC-variable of Al; :: thesis: for q being Element of CQC-WFF Al st S1[q] holds
S1[ All (z,q)]
let q be Element of CQC-WFF Al; :: thesis: ( S1[q] implies S1[ All (z,q)] )
assume A26: S1[q] ; :: thesis: S1[ All (z,q)]
set p = All (z,q);
set q2 = Al2 -Cast q;
set z2 = Al2 -Cast z;
reconsider p = All (z,q) as Element of CQC-WFF Al ;
let p2 be Element of CQC-WFF Al2; :: thesis: for S being CQC_Substitution of Al
for S2 being CQC_Substitution of Al2 st All (z,q) = p2 & S = S2 holds
CQC_Sub [(All (z,q)),S] = CQC_Sub [p2,S2]
let S be CQC_Substitution of Al; :: thesis: for S2 being CQC_Substitution of Al2 st All (z,q) = p2 & S = S2 holds
CQC_Sub [(All (z,q)),S] = CQC_Sub [p2,S2]
let S2 be CQC_Substitution of Al2; :: thesis: ( All (z,q) = p2 & S = S2 implies CQC_Sub [(All (z,q)),S] = CQC_Sub [p2,S2] )
assume A27: ( All (z,q) = p2 & S = S2 ) ; :: thesis: CQC_Sub [(All (z,q)),S] = CQC_Sub [p2,S2]
set qsc = Qsc (q,z,S);
set qsc2 = Qsc ((Al2 -Cast q),(Al2 -Cast z),S2);
set sub = [(All (z,q)),S];
set sub2 = [(All ((Al2 -Cast z),(Al2 -Cast q))),S2];
set qscope = [q,((CFQ Al) . [(All (z,q)),S])];
set qscope2 = [(Al2 -Cast q),((CFQ Al2) . [(All ((Al2 -Cast z),(Al2 -Cast q))),S2])];
A28: QScope (q,z,S) = [[q,((CFQ Al) . [(All (z,q)),S])],z] by SUBSTUT2:def 3;
reconsider qscope = [q,((CFQ Al) . [(All (z,q)),S])] as Element of CQC-Sub-WFF Al ;
reconsider qsc = Qsc (q,z,S) as second_Q_comp of [qscope,z] by SUBSTUT2:def 3;
A29: QScope ((Al2 -Cast q),(Al2 -Cast z),S2) = [[(Al2 -Cast q),((CFQ Al2) . [(All ((Al2 -Cast z),(Al2 -Cast q))),S2])],(Al2 -Cast z)] by SUBSTUT2:def 3;
reconsider qscope2 = [(Al2 -Cast q),((CFQ Al2) . [(All ((Al2 -Cast z),(Al2 -Cast q))),S2])] as Element of CQC-Sub-WFF Al2 ;
reconsider qsc2 = Qsc ((Al2 -Cast q),(Al2 -Cast z),S2) as second_Q_comp of [qscope2,(Al2 -Cast z)] by SUBSTUT2:def 3;
A30: ( [(All (z,q)),S] = CQCSub_All ([qscope,z],qsc) & [qscope,z] is quantifiable & [(All ((Al2 -Cast z),(Al2 -Cast q))),S2] = CQCSub_All ([qscope2,(Al2 -Cast z)],qsc2) & [qscope2,(Al2 -Cast z)] is quantifiable ) by A28, A29, SUBSTUT2:22;
set expandsub = ExpandSub (z,q,(RestrictSub (z,(All (z,q)),S)));
set expandsub2 = ExpandSub ((Al2 -Cast z),(Al2 -Cast q),(RestrictSub ((Al2 -Cast z),(All ((Al2 -Cast z),(Al2 -Cast q))),S2)));
A31: ( All (z,q) is universal & All ((Al2 -Cast z),(Al2 -Cast q)) is universal ) ;
then ( z = bound_in (All (z,q)) & q = the_scope_of (All (z,q)) & Al2 -Cast z = bound_in (All ((Al2 -Cast z),(Al2 -Cast q))) & Al2 -Cast q = the_scope_of (All ((Al2 -Cast z),(Al2 -Cast q))) ) by QC_LANG1:def 27, QC_LANG1:def 28;
then ( All (z,q),S PQSub ExpandSub (z,q,(RestrictSub (z,(All (z,q)),S))) & All ((Al2 -Cast z),(Al2 -Cast q)),S2 PQSub ExpandSub ((Al2 -Cast z),(Al2 -Cast q),(RestrictSub ((Al2 -Cast z),(All ((Al2 -Cast z),(Al2 -Cast q))),S2))) ) by A31, SUBSTUT1:def 14;
then ( [[(All (z,q)),S],(ExpandSub (z,q,(RestrictSub (z,(All (z,q)),S))))] in QSub Al & [[(All ((Al2 -Cast z),(Al2 -Cast q))),S2],(ExpandSub ((Al2 -Cast z),(Al2 -Cast q),(RestrictSub ((Al2 -Cast z),(All ((Al2 -Cast z),(Al2 -Cast q))),S2))))] in QSub Al2 ) by SUBSTUT1:def 15;
then ( [[(All (z,q)),S],(ExpandSub (z,q,(RestrictSub (z,(All (z,q)),S))))] in (QSub Al) | (CQC-Sub-WFF Al) & [[(All ((Al2 -Cast z),(Al2 -Cast q))),S2],(ExpandSub ((Al2 -Cast z),(Al2 -Cast q),(RestrictSub ((Al2 -Cast z),(All ((Al2 -Cast z),(Al2 -Cast q))),S2))))] in (QSub Al2) | (CQC-Sub-WFF Al2) ) by RELAT_1:def 11;
then A32: ( [[(All (z,q)),S],(ExpandSub (z,q,(RestrictSub (z,(All (z,q)),S))))] in CFQ Al & [[(All ((Al2 -Cast z),(Al2 -Cast q))),S2],(ExpandSub ((Al2 -Cast z),(Al2 -Cast q),(RestrictSub ((Al2 -Cast z),(All ((Al2 -Cast z),(Al2 -Cast q))),S2))))] in CFQ Al2 ) by SUBSTUT2:def 2;
set scope = CQCSub_the_scope_of [(All (z,q)),S];
set scope2 = CQCSub_the_scope_of [(All ((Al2 -Cast z),(Al2 -Cast q))),S2];
A33: bound_in ([(All (z,q)),S] `1) = z by A31, QC_LANG1:def 27
.= bound_in ([(All ((Al2 -Cast z),(Al2 -Cast q))),S2] `1) by A31, QC_LANG1:def 27 ;
A34: the_scope_of ([(All (z,q)),S] `1) = q by A31, QC_LANG1:def 28
.= the_scope_of ([(All ((Al2 -Cast z),(Al2 -Cast q))),S2] `1) by A31, QC_LANG1:def 28 ;
A35: ExpandSub (z,q,(RestrictSub (z,(All (z,q)),S))) = ExpandSub ((Al2 -Cast z),(Al2 -Cast q),(RestrictSub ((Al2 -Cast z),(All ((Al2 -Cast z),(Al2 -Cast q))),S2))) by A27, Th15;
A36: CQC_Sub qscope = CQC_Sub [q,(ExpandSub (z,q,(RestrictSub (z,(All (z,q)),S))))] by A32, FUNCT_1:1
.= CQC_Sub qscope2 by A26, A32, A35, FUNCT_1:1 ;
CQC_Sub [p,S] = CQCQuant ([(All (z,q)),S],(CQC_Sub (CQCSub_the_scope_of [(All (z,q)),S]))) by A30, SUBLEMMA:27, SUBLEMMA:28
.= Quant ([(All (z,q)),S],(CQC_Sub (CQCSub_the_scope_of [(All (z,q)),S]))) by A30, SUBLEMMA:27, SUBLEMMA:def 7
.= All ((S_Bound (@ [(All (z,q)),S])),(CQC_Sub (CQCSub_the_scope_of [(All (z,q)),S]))) by SUBSTUT1:def 37
.= Al2 -Cast (All ((S_Bound (@ [(All (z,q)),S])),(CQC_Sub qscope))) by A30, SUBLEMMA:30
.= All ((S_Bound (@ [(All ((Al2 -Cast z),(Al2 -Cast q))),S2])),(CQC_Sub qscope2)) by A36, A27, A31, A33, A34, Th16
.= All ((S_Bound (@ [(All ((Al2 -Cast z),(Al2 -Cast q))),S2])),(CQC_Sub (CQCSub_the_scope_of [(All ((Al2 -Cast z),(Al2 -Cast q))),S2]))) by A30, SUBLEMMA:30
.= Quant ([(All ((Al2 -Cast z),(Al2 -Cast q))),S2],(CQC_Sub (CQCSub_the_scope_of [(All ((Al2 -Cast z),(Al2 -Cast q))),S2]))) by SUBSTUT1:def 37
.= CQCQuant ([(All ((Al2 -Cast z),(Al2 -Cast q))),S2],(CQC_Sub (CQCSub_the_scope_of [(All ((Al2 -Cast z),(Al2 -Cast q))),S2]))) by A30, SUBLEMMA:27, SUBLEMMA:def 7
.= CQC_Sub [p2,S2] by A27, A30, SUBLEMMA:27, SUBLEMMA:28 ;
hence CQC_Sub [(All (z,q)),S] = CQC_Sub [p2,S2] ; :: thesis: verum
end;
then A37: 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
( S1[ VERUM Al] & S1[P ! l] & ( S1[r] implies S1[ 'not' r] ) & ( S1[r] & S1[s] implies S1[r '&' s] ) & ( S1[r] implies S1[ All (x,r)] ) ) by A1, A5, A17, A21;
A38: for p being Element of CQC-WFF Al holds S1[p] from CQC_LANG:sch 1(A37);
 let p2 be Element of CQC-WFF Al2; :: thesis: for x2, y2 being bound_QC-variable of Al2
for p being Element of CQC-WFF Al
for x, y being bound_QC-variable of Al st p = p2 & x = x2 & y = y2 holds
p . (x,y) = p2 . (x2,y2)
let x2, y2 be bound_QC-variable of Al2; :: thesis: for p being Element of CQC-WFF Al
for x, y being bound_QC-variable of Al st p = p2 & x = x2 & y = y2 holds
p . (x,y) = p2 . (x2,y2)
let p be Element of CQC-WFF Al; :: thesis: for x, y being bound_QC-variable of Al st p = p2 & x = x2 & y = y2 holds
p . (x,y) = p2 . (x2,y2)
let x, y be bound_QC-variable of Al; :: thesis: ( p = p2 & x = x2 & y = y2 implies p . (x,y) = p2 . (x2,y2) )
assume A39: ( p = p2 & x = x2 & y = y2 ) ; :: thesis: p . (x,y) = p2 . (x2,y2)
thus p . (x,y) = CQC_Sub [p,(Sbst (x,y))] by SUBSTUT2:def 1
.= CQC_Sub [p2,(Sbst (x2,y2))] by A38, A39
.= p2 . (x2,y2) by SUBSTUT2:def 1 ; :: thesis: verum