let X be non empty ARS ; :: thesis: ( X is COMP iff the reduction of X is complete )

set R = the reduction of X;

A2: ( X is CONF iff the reduction of X is confluent ) by Ch17;

( X is SN iff the reduction of X is strongly-normalizing ) by Ch7, Ch8;

hence ( X is COMP iff the reduction of X is complete ) by A2; :: thesis: verum

set R = the reduction of X;

A2: ( X is CONF iff the reduction of X is confluent ) by Ch17;

( X is SN iff the reduction of X is strongly-normalizing ) by Ch7, Ch8;

hence ( X is COMP iff the reduction of X is complete ) by A2; :: thesis: verum