scheme :: CQC_SIM1:sch 6
Sepregression{ F1() -> QC-alphabet , F2() -> Element of CQC-WFF F1(), P1[ object , object , object , object ] } :
for q being Element of CQC-WFF F1()
for t being QC-symbol of F1()
for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [q,t,K,f] in SepQuadruples F2() holds
P1[q,t,K,f]
provided
A1: P1[F2(), index F2(), {}. (bound_QC-variables F1()), id (bound_QC-variables F1())] and
A2: for q being Element of CQC-WFF F1()
for t being QC-symbol of F1()
for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [('not' q),t,K,f] in SepQuadruples F2() & P1[ 'not' q,t,K,f] holds
P1[q,t,K,f] and
A3: for q, r being Element of CQC-WFF F1()
for t being QC-symbol of F1()
for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [(q '&' r),t,K,f] in SepQuadruples F2() & P1[q '&' r,t,K,f] holds
( P1[q,t,K,f] & P1[r,t + (QuantNbr q),K,f] ) and
A4: for q being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for t being QC-symbol of F1()
for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [(All (x,q)),t,K,f] in SepQuadruples F2() & P1[ All (x,q),t,K,f] holds
P1[q,t ++ ,K \/ {x},f +* (x .--> (x. t))]