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 S_{1}[ 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: 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}[q] holds

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

S_{1}[r '&' s]

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

S_{1}[ All (z,q)]

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, A5, A17, A21;

A38: for p being Element of CQC-WFF Al holds S_{1}[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

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 S

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: S

proof

A5:
for k being Nat
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;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

for P being QC-pred_symbol of k,Al

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

proof

A17:
for q 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]

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)

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;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

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

( the_arity_of P = len l & the_arity_of P2 = len l2 )
by Th1;
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

end;.= 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

hence
CQC_Subst (l,S) = CQC_Subst ((Al2 -Cast l),S2)
by A9, FINSEQ_2:9; :: thesis: verum
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;

end;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 )
;

end;

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;.= (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

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;.= (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

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

S

proof

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

assume A18: S_{1}[q]
; :: thesis: S_{1}[ '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;assume A18: S

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

S

proof

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

assume A22: ( S_{1}[r] & S_{1}[s] )
; :: thesis: S_{1}[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;assume A22: ( 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

for q being Element of CQC-WFF Al st S

S

proof

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

S_{1}[ All (z,q)]

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

assume A26: S_{1}[q]
; :: thesis: S_{1}[ 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;S

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

assume A26: S

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

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

A38: for p being Element of CQC-WFF Al holds S

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