let S be non empty non void ManySortedSign ; :: thesis: ( S is monotonic implies InducedGraph S is well-founded )

set G = InducedGraph S;

assume S is monotonic ; :: thesis: InducedGraph S is well-founded

then reconsider S = S as non empty non void monotonic ManySortedSign ;

set A = the non-empty finite-yielding MSAlgebra over S;

assume not InducedGraph S is well-founded ; :: thesis: contradiction

then consider v being Element of the carrier of (InducedGraph S) such that

A1: for n being Nat ex c being directed Chain of InducedGraph S st

( not c is empty & (vertex-seq c) . ((len c) + 1) = v & len c > n ) by MSSCYC_1:def 4;

reconsider v = v as SortSymbol of S ;

consider s being non empty finite Subset of NAT such that

A2: s = { (depth t) where t is Element of the Sorts of (FreeEnv the non-empty finite-yielding MSAlgebra over S) . v : verum } and

depth (v, the non-empty finite-yielding MSAlgebra over S) = max s by CIRCUIT1:def 6;

max s is Nat by TARSKI:1;

then consider c being directed Chain of InducedGraph S such that

not c is empty and

A3: (vertex-seq c) . ((len c) + 1) = v and

A4: len c > max s by A1;

1 <= len c by A4, NAT_1:14;

then consider t being Element of the Sorts of (FreeMSA the Sorts of the non-empty finite-yielding MSAlgebra over S) . v such that

A5: depth t = len c by A3, Th2;

reconsider t9 = t as Element of the Sorts of (FreeEnv the non-empty finite-yielding MSAlgebra over S) . v ;

( ex t99 being Element of the Sorts of (FreeMSA the Sorts of the non-empty finite-yielding MSAlgebra over S) . v st

( t9 = t99 & depth t9 = depth t99 ) & depth t9 in s ) by A2, CIRCUIT1:def 5;

hence contradiction by A4, A5, XXREAL_2:def 8; :: thesis: verum

set G = InducedGraph S;

assume S is monotonic ; :: thesis: InducedGraph S is well-founded

then reconsider S = S as non empty non void monotonic ManySortedSign ;

set A = the non-empty finite-yielding MSAlgebra over S;

assume not InducedGraph S is well-founded ; :: thesis: contradiction

then consider v being Element of the carrier of (InducedGraph S) such that

A1: for n being Nat ex c being directed Chain of InducedGraph S st

( not c is empty & (vertex-seq c) . ((len c) + 1) = v & len c > n ) by MSSCYC_1:def 4;

reconsider v = v as SortSymbol of S ;

consider s being non empty finite Subset of NAT such that

A2: s = { (depth t) where t is Element of the Sorts of (FreeEnv the non-empty finite-yielding MSAlgebra over S) . v : verum } and

depth (v, the non-empty finite-yielding MSAlgebra over S) = max s by CIRCUIT1:def 6;

max s is Nat by TARSKI:1;

then consider c being directed Chain of InducedGraph S such that

not c is empty and

A3: (vertex-seq c) . ((len c) + 1) = v and

A4: len c > max s by A1;

1 <= len c by A4, NAT_1:14;

then consider t being Element of the Sorts of (FreeMSA the Sorts of the non-empty finite-yielding MSAlgebra over S) . v such that

A5: depth t = len c by A3, Th2;

reconsider t9 = t as Element of the Sorts of (FreeEnv the non-empty finite-yielding MSAlgebra over S) . v ;

( ex t99 being Element of the Sorts of (FreeMSA the Sorts of the non-empty finite-yielding MSAlgebra over S) . v st

( t9 = t99 & depth t9 = depth t99 ) & depth t9 in s ) by A2, CIRCUIT1:def 5;

hence contradiction by A4, A5, XXREAL_2:def 8; :: thesis: verum