The Mizar abstract of MSSCYC

Journal of Formalized Mathematics
Volume 8, 1996
University of Bialystok
Copyright (c) 1996 Association of Mizar Users
The abstract of the Mizar article:: The Correspondence Between Monotonic Many Sorted Signatures and Well-Founded Graphs. Part I
by
Czeslaw Bylinski, and
Piotr Rudnicki
Received February 14, 1996
MML identifier: MSSCYC_1
[ Mizar article, MML identifier index ]
environ

 vocabulary FINSET_1, FUNCT_1, RELAT_1, CARD_3, PROB_1, FUNCT_2, GRAPH_1,
      ORDERS_1, FINSEQ_1, GRAPH_2, QUANTAL1, BOOLE, RELAT_2, FUNCOP_1,
      PARTFUN1, CARD_1, ARYTM_1, TREES_2, TREES_4, TREES_1, AMI_1, MSUALG_1,
      ZF_REFLE, PBOOLE, MSATERM, TREES_9, FREEALG, MSUALG_2, MSAFREE2,
      PRE_CIRC, PRALG_1, MSAFREE, GROUP_6, PRELAMB, ALG_1, REALSET1, MSUALG_3,
      FUNCT_6, TARSKI, TDGROUP, QC_LANG1, UNIALG_2, DTCONSTR, TREES_3,
      MSSCYC_1, FINSEQ_4;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, XREAL_0, NAT_1,
      CARD_1, STRUCT_0, PROB_1, CARD_3, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
      FINSET_1, FINSEQ_1, FINSEQ_4, GRAPH_1, GRAPH_2, TOPREAL1, TREES_1,
      TREES_2, TREES_3, FUNCT_6, TREES_4, LANG1, DTCONSTR, PBOOLE, MSUALG_1,
      MSUALG_2, MSUALG_3, MSAFREE, PRE_CIRC, MSAFREE2, TREES_9, MSATERM;
 constructors NAT_1, WELLORD2, GRAPH_2, TOPREAL1, MSUALG_3, PRE_CIRC, MSAFREE2,
      TREES_9, MSATERM, EXTENS_1, FINSEQ_4, INT_1;
 clusters STRUCT_0, RELSET_1, FINSEQ_1, FINSEQ_5, RELAT_1, FINSET_1, GRAPH_1,
      GRAPH_2, TREES_2, TREES_3, DTCONSTR, TREES_9, MSUALG_1, MSUALG_2,
      MSAFREE, PRE_CIRC, MSAFREE2, EXTENS_1, PRELAMB, MSATERM, INT_1, XREAL_0;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin :: Some properties of graphs and trees

theorem :: MSSCYC_1:1
    for f being finite Function st
    for x being set st x in dom f holds f.x is finite
  holds product f is finite;

reserve G for Graph,
        k, m, n for Nat;

 definition let G be Graph;
  redefine mode Chain of G means
:: MSSCYC_1:def 1
 it is FinSequence of the Edges of G &
    ex p being FinSequence of the Vertices of G st
          p is_vertex_seq_of it;
 end;

theorem :: MSSCYC_1:2
   for p,q being FinSequence st n<=len p
  holds (1,n)-cut p = (1,n)-cut (p^q);

definition let G be Graph;
  let IT be Chain of G;
 redefine attr IT is oriented;
 synonym IT is directed;
end;

definition let G be Graph;
 let IT be Chain of G;
 attr IT is cyclic means
:: MSSCYC_1:def 2
 ex p being FinSequence of the Vertices of G st
        p is_vertex_seq_of IT & p.1 = p.(len p);
end;

definition let IT be Graph;
 attr IT is empty means
:: MSSCYC_1:def 3
 the Edges of IT is empty;
end;

definition
 cluster empty Graph;
end;

theorem :: MSSCYC_1:3
for G being Graph holds
 rng (the Source of G) \/ rng (the Target of G) c= the Vertices of G;

definition
  cluster finite simple connected non empty strict Graph;
end;

definition let G be non empty Graph;
 cluster the Edges of G -> non empty;
end;

theorem :: MSSCYC_1:4
for e being set
             for s, t being Element of the Vertices of G
 st s = (the Source of G).e & t = (the Target of G).e
  holds <*s, t*> is_vertex_seq_of <*e*>;

theorem :: MSSCYC_1:5
for e being set st e in the Edges of G
              holds <*e*> is directed Chain of G;

reserve G for non empty Graph;

definition let G;
 cluster directed non empty one-to-one Chain of G;
end;

theorem :: MSSCYC_1:6
 for G being Graph,
     c being Chain of G, vs being FinSequence of the Vertices of G st
  c is cyclic & vs is_vertex_seq_of c holds vs.1 = vs.(len vs);

theorem :: MSSCYC_1:7
for G being Graph, e being set st e in the Edges of G
             for fe being directed Chain of G st fe = <*e*>
         holds vertex-seq fe = <*(the Source of G).e, (the Target of G).e*>;

theorem :: MSSCYC_1:8
   for f being FinSequence holds len (m,n)-cut f <= len f;

theorem :: MSSCYC_1:9
   for c being directed Chain of G st 1<=m & m<=n & n<=len c
   holds (m,n)-cut c is directed Chain of G;

theorem :: MSSCYC_1:10
for oc being non empty directed Chain of G holds
 len vertex-seq oc = len oc +1;

definition let G; let oc be directed non empty Chain of G;
 cluster vertex-seq oc -> non empty;
end;

theorem :: MSSCYC_1:11
for oc being directed non empty Chain of G, n
                st 1<=n & n<=len oc
                 holds (vertex-seq oc).n = (the Source of G).(oc.n) &
                       (vertex-seq oc).(n+1) = (the Target of G).(oc.n);

theorem :: MSSCYC_1:12
for f being non empty FinSequence st 1<=m & m<=n & n<=len f
 holds (m,n)-cut f is non empty;

theorem :: MSSCYC_1:13
   for c, c1 being directed Chain of G
 st 1<=m & m<=n & n<=len c & c1 = (m,n)-cut c
  holds vertex-seq c1 = (m,n+1)-cut vertex-seq c;

theorem :: MSSCYC_1:14
for oc being directed non empty Chain of G
            holds (vertex-seq oc).(len oc +1) = (the Target of G).(oc.len oc);

theorem :: MSSCYC_1:15
for c1, c2 being directed non empty Chain of G
              holds (vertex-seq c1).(len c1 + 1) = (vertex-seq c2).1 iff
                    c1^c2 is directed non empty Chain of G;

theorem :: MSSCYC_1:16
for c, c1, c2 being directed non empty Chain of G st c =c1^c2
   holds (vertex-seq c).1 = (vertex-seq c1).1 &
         (vertex-seq c).(len c +1) = (vertex-seq c2).(len c2 +1);

theorem :: MSSCYC_1:17
for oc being directed non empty Chain of G st oc is cyclic
              holds (vertex-seq oc).1 = (vertex-seq oc).(len oc +1);

theorem :: MSSCYC_1:18
 for c being directed non empty Chain of G st c is cyclic
 for n ex ch being directed Chain of G st
              len ch = n & ch^c is directed non empty Chain of G;

definition let IT be Graph;
 attr IT is directed_cycle-less means
:: MSSCYC_1:def 4
 for dc being directed Chain of IT st dc is non empty
  holds dc is non cyclic;
 antonym IT is with_directed_cycle;
end;

definition
 cluster empty -> directed_cycle-less Graph;
end;

definition let IT be Graph;
 attr IT is well-founded means
:: MSSCYC_1:def 5
 for v being Element of the Vertices of IT
  ex n st for c being directed Chain of IT
    st c is non empty & (vertex-seq c).(len c +1) = v holds len c <= n;
end;

definition let G be empty Graph;
 cluster -> empty Chain of G;
end;

definition
 cluster empty -> well-founded Graph;
end;

definition
 cluster non well-founded -> non empty Graph;
end;

definition
 cluster well-founded Graph;
end;

definition
 cluster well-founded -> directed_cycle-less Graph;
end;

definition
 cluster non well-founded Graph;
end;

definition
 cluster directed_cycle-less Graph;
end;

theorem :: MSSCYC_1:19
  for t being DecoratedTree, p being Node of t, k being Nat
 holds p|k is Node of t;

begin :: Some properties of many sorted algebras

theorem :: MSSCYC_1:20
   for S being non void (non empty ManySortedSign),
        X being non-empty ManySortedSet of the carrier of S,
        t being Term of S,X st t is not root
 ex o being OperSymbol of S st t.{} = [o,the carrier of S];

theorem :: MSSCYC_1:21
 for S being non void non empty ManySortedSign,
     A being MSAlgebra over S,
     G being GeneratorSet of A,
     B being MSSubset of A
  st G c= B holds B is GeneratorSet of A;

definition
 let S be non void non empty ManySortedSign,
     A be finitely-generated (non-empty MSAlgebra over S);
 cluster non-empty locally-finite GeneratorSet of A;
end;

theorem :: MSSCYC_1:22
 for S being non void non empty ManySortedSign,
     A being non-empty MSAlgebra over S,
     X being non-empty GeneratorSet of A
   ex F being ManySortedFunction of FreeMSA X, A
    st F is_epimorphism FreeMSA X, A;

theorem :: MSSCYC_1:23
   for S being non void non empty ManySortedSign,
     A being non-empty MSAlgebra over S,
     X being non-empty GeneratorSet of A
  st A is non locally-finite
   holds FreeMSA X is non locally-finite;

definition
 let S be non void non empty ManySortedSign,
     X be non-empty locally-finite ManySortedSet of the carrier of S,
     v be SortSymbol of S;
 cluster FreeGen(v, X) -> finite;
end;

canceled;

theorem :: MSSCYC_1:25
 for S being non void non empty ManySortedSign,
     A being non-empty MSAlgebra over S, o be OperSymbol of S
  st (the Arity of S).o = {} holds dom Den(o, A) = {{}};

definition let IT be non void non empty ManySortedSign;
 attr IT is finitely_operated means
:: MSSCYC_1:def 6
 for s being SortSymbol of IT holds
  {o where o is OperSymbol of IT: the_result_sort_of o = s} is finite;
end;

theorem :: MSSCYC_1:26
   for S being non void non empty ManySortedSign,
     A being non-empty MSAlgebra over S, v be SortSymbol of S
  st S is finitely_operated holds Constants(A, v) is finite;

theorem :: MSSCYC_1:27
   for S being non void non empty ManySortedSign,
     X being non-empty ManySortedSet of the carrier of S,
     v being SortSymbol of S
 holds
   {t where t is Element of (the Sorts of FreeMSA X).v: depth t = 0}
 = FreeGen(v, X) \/ Constants(FreeMSA X, v);

theorem :: MSSCYC_1:28
   for S being non void non empty ManySortedSign,
     X being non-empty ManySortedSet of the carrier of S,
     v, vk being SortSymbol of S, o being OperSymbol of S,
     t being Element of (the Sorts of FreeMSA X).v,
     a being (ArgumentSeq of Sym(o,X)), k being Nat,
     ak being Element of (the Sorts of FreeMSA X).vk
  st t = [o,the carrier of S]-tree a & k in dom a & ak = a.k
   holds depth ak < depth t;
The abstract of the Mizar article:

The Correspondence Between Monotonic Many Sorted Signatures and Well-Founded Graphs. Part I
