let Al be QC-alphabet ; :: thesis: for k being Nat
for p, r being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for P being QC-pred_symbol of k,Al
for l being CQC-variable_list of k,Al
for Al2 being Al -expanding QC-alphabet holds
( Al2 -Cast (VERUM Al) = VERUM Al2 & Al2 -Cast (P ! l) = (Al2 -Cast P) ! (Al2 -Cast l) & Al2 -Cast ('not' p) = 'not' (Al2 -Cast p) & Al2 -Cast (p '&' r) = (Al2 -Cast p) '&' (Al2 -Cast r) & Al2 -Cast (All (x,p)) = All ((Al2 -Cast x),(Al2 -Cast p)) )
let k be Nat; :: thesis: for p, r being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for P being QC-pred_symbol of k,Al
for l being CQC-variable_list of k,Al
for Al2 being Al -expanding QC-alphabet holds
( Al2 -Cast (VERUM Al) = VERUM Al2 & Al2 -Cast (P ! l) = (Al2 -Cast P) ! (Al2 -Cast l) & Al2 -Cast ('not' p) = 'not' (Al2 -Cast p) & Al2 -Cast (p '&' r) = (Al2 -Cast p) '&' (Al2 -Cast r) & Al2 -Cast (All (x,p)) = All ((Al2 -Cast x),(Al2 -Cast p)) )
let p, r be Element of CQC-WFF Al; :: thesis: for x being bound_QC-variable of Al
for P being QC-pred_symbol of k,Al
for l being CQC-variable_list of k,Al
for Al2 being Al -expanding QC-alphabet holds
( Al2 -Cast (VERUM Al) = VERUM Al2 & Al2 -Cast (P ! l) = (Al2 -Cast P) ! (Al2 -Cast l) & Al2 -Cast ('not' p) = 'not' (Al2 -Cast p) & Al2 -Cast (p '&' r) = (Al2 -Cast p) '&' (Al2 -Cast r) & Al2 -Cast (All (x,p)) = All ((Al2 -Cast x),(Al2 -Cast p)) )
let x be bound_QC-variable of Al; :: thesis: for P being QC-pred_symbol of k,Al
for l being CQC-variable_list of k,Al
for Al2 being Al -expanding QC-alphabet holds
( Al2 -Cast (VERUM Al) = VERUM Al2 & Al2 -Cast (P ! l) = (Al2 -Cast P) ! (Al2 -Cast l) & Al2 -Cast ('not' p) = 'not' (Al2 -Cast p) & Al2 -Cast (p '&' r) = (Al2 -Cast p) '&' (Al2 -Cast r) & Al2 -Cast (All (x,p)) = All ((Al2 -Cast x),(Al2 -Cast p)) )
let P be QC-pred_symbol of k,Al; :: thesis: for l being CQC-variable_list of k,Al
for Al2 being Al -expanding QC-alphabet holds
( Al2 -Cast (VERUM Al) = VERUM Al2 & Al2 -Cast (P ! l) = (Al2 -Cast P) ! (Al2 -Cast l) & Al2 -Cast ('not' p) = 'not' (Al2 -Cast p) & Al2 -Cast (p '&' r) = (Al2 -Cast p) '&' (Al2 -Cast r) & Al2 -Cast (All (x,p)) = All ((Al2 -Cast x),(Al2 -Cast p)) )
let l be CQC-variable_list of k,Al; :: thesis: for Al2 being Al -expanding QC-alphabet holds
( Al2 -Cast (VERUM Al) = VERUM Al2 & Al2 -Cast (P ! l) = (Al2 -Cast P) ! (Al2 -Cast l) & Al2 -Cast ('not' p) = 'not' (Al2 -Cast p) & Al2 -Cast (p '&' r) = (Al2 -Cast p) '&' (Al2 -Cast r) & Al2 -Cast (All (x,p)) = All ((Al2 -Cast x),(Al2 -Cast p)) )
let Al2 be Al -expanding QC-alphabet ; :: thesis: ( Al2 -Cast (VERUM Al) = VERUM Al2 & Al2 -Cast (P ! l) = (Al2 -Cast P) ! (Al2 -Cast l) & Al2 -Cast ('not' p) = 'not' (Al2 -Cast p) & Al2 -Cast (p '&' r) = (Al2 -Cast p) '&' (Al2 -Cast r) & Al2 -Cast (All (x,p)) = All ((Al2 -Cast x),(Al2 -Cast p)) )
A1: the_arity_of P = len l by Th1;
A2: the_arity_of (Al2 -Cast P) = len (Al2 -Cast l) by Th1;
thus Al2 -Cast (VERUM Al) = VERUM Al2 ; :: thesis: ( Al2 -Cast (P ! l) = (Al2 -Cast P) ! (Al2 -Cast l) & Al2 -Cast ('not' p) = 'not' (Al2 -Cast p) & Al2 -Cast (p '&' r) = (Al2 -Cast p) '&' (Al2 -Cast r) & Al2 -Cast (All (x,p)) = All ((Al2 -Cast x),(Al2 -Cast p)) )
thus Al2 -Cast (P ! l) = <*P*> ^ l by A1, QC_LANG1:def 12
.= (Al2 -Cast P) ! (Al2 -Cast l) by A2, QC_LANG1:def 12 ; :: thesis: ( Al2 -Cast ('not' p) = 'not' (Al2 -Cast p) & Al2 -Cast (p '&' r) = (Al2 -Cast p) '&' (Al2 -Cast r) & Al2 -Cast (All (x,p)) = All ((Al2 -Cast x),(Al2 -Cast p)) )
thus Al2 -Cast ('not' p) = 'not' (Al2 -Cast p) ; :: thesis: ( Al2 -Cast (p '&' r) = (Al2 -Cast p) '&' (Al2 -Cast r) & Al2 -Cast (All (x,p)) = All ((Al2 -Cast x),(Al2 -Cast p)) )
thus Al2 -Cast (p '&' r) = (Al2 -Cast p) '&' (Al2 -Cast r) ; :: thesis: Al2 -Cast (All (x,p)) = All ((Al2 -Cast x),(Al2 -Cast p))
thus Al2 -Cast (All (x,p)) = All ((Al2 -Cast x),(Al2 -Cast p)) ; :: thesis: verum