:: deftheorem Def3 defines CON CQC_SIM1:def 3 :
for A being QC-alphabet
for f, g being Function of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)
for n being Nat
for b₅ being Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) holds
( b₅ = CON (f,g,n) iff for t being QC-symbol of A
for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))
for p, q being Element of CQC-WFF A st p = f . (t,h) & q = g . ((t + n),h) holds
b₅ . (t,h) = p '&' q );