scheme :: GRZLOG_1:sch 1
BinReplace{ F1() -> non empty set , F2( Element of F1(), Element of F1()) -> Element of F1(), P1[ Element of F1(), Element of F1()] } :
for a, b, c, d being Element of F1() st P1[a,b] & P1[c,d] holds
P1[F2(a,c),F2(b,d)]
provided
A2: for a, b, c being Element of F1() st P1[a,b] & P1[b,c] holds
P1[a,c] and
A3: for a, b being Element of F1() holds P1[F2(a,b),F2(b,a)] and
A4: for a, b, c being Element of F1() st P1[a,b] holds
P1[F2(a,c),F2(b,c)]