:: Mizar Analysis of Algorithms: Preliminaries
::  by Grzegorz Bancerek
::
:: Received July 9, 2007
:: Copyright (c) 2007 Association of Mizar Users

environ

 vocabularies AOFA_000, UNIALG_1, FUNCT_1, BINOP_1, GROUP_1, FINSEQ_1, RELAT_1,
      BINTREE1, FUNCT_2, PARTFUN1, COMPUT_1, BOOLE, MSUALG_1, FUNCT_7,
      ZF_REFLE, SUPINF_1, RLVECT_1, FUNCOP_1, FUNCT_4, ARYTM, PROB_1, TARSKI,
      TREES_4, FINSEQ_2, ARYTM_1, FINSET_1, CQC_LANG, SUBSET_1, FUNCT_3,
      VECTSP_1, SETFAM_1, FREEALG, FINSEQ_4, DTCONSTR, CARD_1, TREES_2, LANG1,
      TDGROUP, TREES_3, TREES_1, MEMBERED, SQUARE_1, WELLORD1, INCPROJ,
      FACIRC_1, UNIALG_2, PRELAMB, FUNCT_5, CQC_SIM1, ALG_1, ORDINAL2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ENUMSET1, SETFAM_1, ORDINAL1,
      MEMBERED, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FINSET_1, LANG1,
      FINSEQ_1, BINOP_1, CARD_1, CARD_3, FRAENKEL, FINSEQ_2, PRE_CIRC,
      XXREAL_2,
      FACIRC_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, TREES_1, TREES_2,
      TREES_3, NAT_1, BINARITH, SUPINF_1, MESFUNC1, FUNCOP_1, FUNCT_4, FUNCT_5,
      FUNCT_7, ABIAN, CAT_2, MARGREL1, STRUCT_0, UNIALG_1, UNIALG_2, ALG_1,
      FREEALG, PUA2MSS1, COMPUT_1, SUPINF_2, TREES_4, DTCONSTR, FINSEQ_4,
      RECDEF_1;
 constructors PUA2MSS1, COMPUT_1, BINARITH, REAL_1, BORSUK_1, SUPINF_2,
      FINSEQ_4, FACIRC_1, ALG_1, FREEALG, FINSEQOP, PRE_CIRC, WELLORD2, CAT_2,
      ABIAN, RECDEF_1, MESFUNC1, NAT_1, SUPINF_1;
 registrations FUNCT_1, FINSEQ_2, FUNCT_2, FINSEQ_1, UNIALG_1, NAT_1, STRUCT_0,
      PUA2MSS1, DTCONSTR, FREEALG, FUNCT_7, CARD_5, SUBSET_1, XXREAL_0,
      XREAL_0, TREES_2, TREES_3, MEMBERED, XBOOLE_0, FINSET_1, TREES_1,
      PRE_CIRC, FACIRC_1, RELAT_1, VALUED_0, CARD_1, XXREAL_2;
 requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
 definitions SUBSET_1, TREES_4, MEMBERED, TARSKI, PUA2MSS1, FUNCT_1, MESFUNC1,
      FREEALG, RELAT_1, FINSEQ_1, UNIALG_1, UNIALG_2, COMPUT_1, BINOP_1,
      XBOOLE_0;
 theorems XBOOLE_1, ZFMISC_1, RELAT_1, RELSET_1, FUNCT_2, FUNCOP_1, CATALG_1,
      COMPUT_1, UNIALG_1, FINSEQ_1, FINSEQ_2, TARSKI, XBOOLE_0, FINSEQ_3,
      XREAL_1, FUNCT_7, NAT_1, ORDINAL1, PARTFUN1, FUNCT_3, BINARITH, DTCONSTR,
      FUNCT_4, FREEALG, TREES_4, FUNCT_1, LANG1, CARD_2, CARD_1, CARD_4,
      CARD_5, TREES_3, PRE_CIRC, ENUMSET1, FINSEQ_5, WELLORD2, GROUP_7,
      UNIALG_2, FINSET_1, STIRL2_1, JORDAN16, ALTCAT_1, FUNCT_5, FUNCT_6,
      MSUALG_1, ALG_1, XREAL_0, XXREAL_0, SETFAM_1, MSUALG_8, SUPINF_2,
      POLYNOM1, XXREAL_2;
 schemes NAT_1, FUNCT_1, RECDEF_1, FINSEQ_2, CIRCCMB3, PRE_CIRC, WELLORD2,
      XBOOLE_0, CLASSES1, ALTCAT_2, FINSEQ_1;

begin :: Binary operations, orbits, and iterations

notation
  let x,y be set;
  antonym x nin y for x in y;
end;

theorem Th1:
  for f,g,h being Function
  for A being set st A c= dom f & A c= dom g & rng h c= A &
  for x being set st x in A holds f.x = g.x holds f*h = g*h
proof
  let f,g,h be Function;
  let A be set such that
A1: A c= dom f and
A2: A c= dom g and
A3: rng h c= A and
A4: for x being set st x in A holds f.x = g.x;
A5: dom (f*h) = dom h & dom (g*h) = dom h by A1,A2,A3,RELAT_1:46,XBOOLE_1:1;
  now
    let x be set;
    assume x in dom h;
    then (f*h).x = f.(h.x) & (g*h).x = g.(h.x) & h.x in rng h
    by FUNCT_1:12,23;
    hence (f*h).x = (g*h).x by A3,A4;
  end;
  hence f*h = g*h by A5,FUNCT_1:9;
end;

registration
  let x,y be non empty set;
  cluster <*x,y*> -> non-empty;
  coherence
  proof
    assume {} in rng <*x,y*>;
    then {} in {x,y} by FINSEQ_2:147;
    hence thesis by TARSKI:def 2;
  end;
end;

registration
  let p,q be non-empty FinSequence;
  cluster p^q -> non-empty;
  coherence
  proof
    assume {} in rng (p^q);
    then {} in (rng p) \/ rng q by FINSEQ_1:44;
    then {} in rng p or {} in rng q by XBOOLE_0:def 2;
    hence thesis by RELAT_1:def 9;
  end;
end;

definition
  let f be homogeneous Function;
  let x be set;
  pred x is_a_unity_wrt f means
  :
  Def1: for y,z being set st <*y,z*> in dom f or <*z,y*> in dom f
  holds <*x,y*> in dom f & f.<*x,y*> = y & <*y,x*> in dom f & f.<*y,x*> = y;
end;

definition
  let f be homogeneous Function;
  attr f is associative means
  :
  Def2: for x,y,z being set st <*x,y*> in dom f & <*y,z*> in dom f &
  <*f.<*x,y*>,z*> in dom f & <*x,f.<*y,z*>*> in dom f
  holds f.<*f.<*x,y*>,z*> = f.<*x,f.<*y,z*>*>;
  attr f is unital means
  : Def3:
  ex x being set st x is_a_unity_wrt f;
end;

definition
  let X be set;
  let Y be non empty set;
  let Z be FinSequenceSet of X;
  let y be Element of Y;
  redefine func Z --> y -> PartFunc of X*,Y;
  coherence
  proof
    dom (Z --> y) = Z & Z c= X* & rng (Z --> y) c= {y}
    by FUNCOP_1:19,COMPUT_1:13;
    hence thesis by RELSET_1:11;
  end;
end;

registration
  let X be non empty set;
  let x be Element of X;
  let n be Nat;
  cluster (n-tuples_on X) --> x ->
    non empty quasi_total homogeneous PartFunc of X*, X;
  coherence
  proof
    reconsider m = n as Element of NAT by ORDINAL1:def 13;
    set f = (n-tuples_on X) --> x;
A1: m-tuples_on X c= X* & rng f c= X &
    dom f = m-tuples_on X by CATALG_1:6,FUNCOP_1:19;
    then reconsider f as non empty homogeneous PartFunc of X*, X
    by COMPUT_1:19;
    arity f = m by A1,COMPUT_1:27;
    hence thesis by A1,COMPUT_1:25;
  end;
end;

theorem Th2:
  for X being non empty set, x being Element of X
  for n being Nat holds arity ((n-tuples_on X) --> x) = n
proof
  let X be non empty set;
  let x be Element of X;
  let n be Nat;
  reconsider m = n as Element of NAT by ORDINAL1:def 13;
  set f = (n-tuples_on X) --> x;
  dom f = m-tuples_on X by FUNCOP_1:19;
  hence arity f = n by COMPUT_1:27;
end;

Lm1: now
  let X be non empty set;
  let x be Element of X;
  thus (0-tuples_on X) --> x is nullary
  proof
    thus arity ((0-tuples_on X) --> x) = 0 by Th2;
  end;
  thus (1-tuples_on X) --> x is unary
  proof
    thus arity ((1-tuples_on X) --> x) = 1 by Th2;
  end;
  thus (2-tuples_on X) --> x is binary
  proof
    thus arity ((2-tuples_on X) --> x) = 2 by Th2;
  end;
  thus (3-tuples_on X) --> x is ternary
  proof
    thus arity ((3-tuples_on X) --> x) = 3 by Th2;
  end;
end;

registration
  let X be non empty set;
  let x be Element of X;
  cluster (0-tuples_on X) --> x -> nullary (homogeneous PartFunc of X*, X);
  coherence by Lm1;
  cluster (1-tuples_on X) --> x -> unary (homogeneous PartFunc of X*, X);
  coherence by Lm1;
  cluster (2-tuples_on X) --> x -> binary (homogeneous PartFunc of X*, X);
  coherence by Lm1;
  cluster (3-tuples_on X) --> x -> ternary (homogeneous PartFunc of X*, X);
  coherence by Lm1;
end;

registration
  let X be non empty set;
  cluster binary associative unital
    (non empty quasi_total homogeneous PartFunc of X*, X);
  existence
  proof
    consider x being Element of X;
    deffunc F((Element of X), Element of X) = IFEQ($1,x,$2,$1);
    (ex f being Function of 2-tuples_on X, X st
    for x,y being Element of X holds f.<*x,y*> = F(x,y)) &
    for f1,f2 being Function of 2-tuples_on X, X st
    (for x,y being Element of X holds f1.<*x,y*> = F(x,y)) &
    (for x,y being Element of X holds f2.<*x,y*> = F(x,y))
    holds f1 = f2 from CIRCCMB3:sch 7;
    then consider f being Function of 2-tuples_on X, X such that
A1: for a,b being Element of X holds f.<*a,b*> = IFEQ(a,x,b,a);
A2: 2-tuples_on X c= X* & rng f c= X &
    dom f = 2-tuples_on X by CATALG_1:6,FUNCT_2:def 1;
    then reconsider f as non empty homogeneous PartFunc of X*, X
    by RELSET_1:11,COMPUT_1:19;
    arity f = 2 by A2,COMPUT_1:27;
    then reconsider f as non empty quasi_total homogeneous PartFunc of X*, X
    by A2,COMPUT_1:25;
    take f;
    thus arity f = 2 by A2,COMPUT_1:27;
    hereby
      let u,y,z be set;
      assume <*u,y*> in dom f & <*y,z*> in dom f;
      then reconsider u' = u, y' = y, z' = z as Element of X by A2,CATALG_1:11;
      assume <*f.<*u,y*>,z*> in dom f & <*u,f.<*y,z*>*> in dom f;
A3:   (u = x implies IFEQ(u,x,y,u) = y) & (u <> x implies IFEQ(u,x,y,u) = u) &
      (u = x implies IFEQ(u,x,IFEQ(y,x,z,y),u) = IFEQ(y,x,z,y)) &
      (u <> x implies IFEQ(u,x,IFEQ(y,x,z,y),u) = u) &
      (u <> x implies IFEQ(u,x,z,u) = u) by FUNCOP_1:def 8;
      thus f.<*f.<*u,y*>,z*> = f.<*IFEQ(u',x,y',u'),z'*> by A1
        .= IFEQ(IFEQ(u,x,y,u),x,z,IFEQ(u,x,y,u)) by A1
        .= f.<*u',IFEQ(y',x,z',y')*> by A1,A3
        .= f.<*u,f.<*y,z*>*> by A1;
    end;
    take x;
    let y,z be set;
    assume <*y,z*> in dom f or <*z,y*> in dom f;
    then reconsider y' = y as Element of X by A2,CATALG_1:11;
    <*x,y'*> in 2-tuples_on X by CATALG_1:10;
    hence <*x,y*> in dom f by FUNCT_2:def 1;
    thus f.<*x,y*> = IFEQ(x,x,y',x) by A1
      .= y by FUNCOP_1:def 8;
    <*y',x*> in 2-tuples_on X by CATALG_1:10;
    hence <*y,x*> in dom f by FUNCT_2:def 1;
A4: x = y or x <> y;
    thus f.<*y,x*> = IFEQ(y',x,x,y') by A1
      .= y by A4,FUNCOP_1:def 8;
  end;
  cluster nullary (non empty quasi_total homogeneous PartFunc of X*, X);
  existence
  proof
    consider x being Element of X;
    set f = (0-tuples_on X) --> x;
    take f; thus arity f = 0 by Th2;
  end;
  cluster ternary (non empty quasi_total homogeneous PartFunc of X*, X);
  existence
  proof
    consider x being Element of X;
    set f = (3-tuples_on X) --> x;
    take f; thus arity f = 3 by Th2;
  end;
end;

theorem Th3:
  for X being non empty set for p being FinSequence of FinTrees X
  for x,t being set st t in rng p holds t <> x-tree p
proof
  let X be non empty set;
  let p be FinSequence of FinTrees X;
  let x,t be set;
  assume
A1: t in rng p;
  then reconsider T = t as Element of FinTrees X;
  reconsider A = dom T as finite Tree;
  defpred P[set] means not contradiction;
  deffunc F(Element of A) = len $1;
  {F(e) where e is Element of A: P[e]} is finite from PRE_CIRC:sch 1;
  then reconsider B = {F(e) where e is Element of A: P[e]} as finite set;
  consider e being Element of A;
A2: F(e) in B;
  B is real-membered
  proof
    let a be set;
    assume a in B;
    then ex e being Element of A st a = F(e);
    hence a is real;
  end;
  then reconsider B as non empty finite real-membered set by A2;
  max B in B by XXREAL_2:def 8;
  then consider e being Element of A such that
A3: max B = len e;
  consider i being set such that
A4: i in dom p & t = p.i by A1,FUNCT_1:def 5;
  reconsider i as Nat by A4;
  i >= 1 by A4,FINSEQ_3:27;
  then consider j being Nat such that
A5: i = 1+j by NAT_1:10;
  i <= len p by A4,FINSEQ_3:27;
  then j < len p & j in NAT by A5,NAT_1:13,ORDINAL1:def 13;
  then
A6: <*j*>^e in dom (x-tree p) by A4,A5,TREES_4:11;
  len (<*j*>^e) = 1+len e by FINSEQ_5:8;
  then len (<*j*>^e) > max B by A3,NAT_1:13;
  then len (<*j*>^e) nin B by XXREAL_2:def 8;
  hence t <> x-tree p by A6;
end;

definition
  let f,g be Function;
  let X be set;
  func (f,X)+*g -> Function equals

  g+*(f|X);
  coherence;
end;

theorem Th4:
  for f,g being Function, x,X being set holds
  x in X & X c= dom f implies ((f,X)+*g).x = f.x
proof
  let f,g be Function;
  let x,X be set;
  assume
A1: x in X;
  assume X c= dom f;
  then x in dom f & dom (f|X) = dom f /\ X by A1,FUNCT_1:68;
  then
A2: x in dom (f|X) by A1,XBOOLE_0:def 3;
  then (f|X).x = f.x by FUNCT_1:68;
  hence ((f,X)+*g).x = f.x by A2,FUNCT_4:14;
end;

theorem Th5:
  for f,g being Function, x,X being set holds
  x nin X & x in dom g implies ((f,X)+*g).x = g.x
proof
  let f,g be Function;
  let x,X be set;
  assume x nin X;
  then x nin dom f /\ X by XBOOLE_0:def 3;
  then x nin dom (f|X) by FUNCT_1:68;
  hence thesis by FUNCT_4:12;
end;

definition
  let X,Y be non empty set;
  let f,g be Element of Funcs(X,Y);
  let A be set;
  redefine func (f,A)+*g -> Element of Funcs(X,Y);
  coherence
  proof
    dom f = X & dom g = X & rng f c= Y & rng g c= Y by FUNCT_2:169;
    then dom g \/ dom (f|A) = X by XBOOLE_1:12;
    then
A1: dom ((f,A)+*g) = X by FUNCT_4:def 1;
    rng ((f,A)+*g) c= rng g \/ rng (f|A) & rng g \/ rng (f|A) c= Y \/ Y
    by FUNCT_4:18;
    then rng ((f,A)+*g) c= Y by XBOOLE_1:1;
    hence thesis by A1,FUNCT_2:def 2;
  end;
end;

definition
  let X,Y,Z be non empty set;
  let f be Element of Funcs(X,Y);
  let g be Element of Funcs(Y,Z);
  redefine func g*f -> Element of Funcs(X,Z);
  coherence
  proof
    g*f is Function of X,Z;
    hence thesis by FUNCT_2:11;
  end;
end;

definition
  let f be Function;
  let x be set;
  func f orbit x equals
  {iter(f,n).x where n is Element of NAT: x in dom iter(f,n)};
  coherence;
end;

theorem Th6:
  for f being Function, x being set st x in dom f holds x in f orbit x
proof
  let f be Function;
  let x be set;
  assume x in dom f;
  then
A1: x in dom f \/ rng f & iter(f,0) = id (dom f \/ rng f)
  by XBOOLE_0:def 2,FUNCT_7:70;
  then iter(f,0).x = x & dom iter(f,0) = dom f \/ rng f by FUNCT_1:34;
  hence x in f orbit x by A1;
end;

theorem
  for f being Function, x,y being set
  st rng f c= dom f & y in f orbit x holds f.y in f orbit x
proof
  let f be Function;
  let x,y be set;
  assume
A1: rng f c= dom f;
  assume y in f orbit x;
  then consider n being Element of NAT such that
A2: y = iter(f,n).x & x in dom iter(f,n);
A3: iter(f,n+1) = f*iter(f,n) by FUNCT_7:73;
  then
A4: f.y = iter(f,n+1).x by A2,FUNCT_1:23;
  y in rng iter(f,n) & rng iter(f,n) c= dom f \/ rng f &
  dom f \/ rng f = dom f by A1,A2,XBOOLE_1:12,FUNCT_7:74,FUNCT_1:def 5;
  then x in dom iter(f,n+1) by A2,A3,FUNCT_1:21;
  hence f.y in f orbit x by A4;
end;

theorem
  for f being Function, x being set st x in dom f holds f.x in f orbit x
proof
  let f be Function;
  let x be set;
  assume
A1: x in dom f;
  iter(f,1) = f by FUNCT_7:72;
  hence f.x in f orbit x by A1;
end;

theorem Th9:
  for f being Function, x being set st x in dom f & f.x in dom f
  holds f orbit (f.x) c= f orbit x
proof
  let f be Function;
  let x be set;
  assume
A1: x in dom f & f.x in dom f;
  let a be set;
  assume a in f orbit (f.x);
  then consider n being Element of NAT such that
A2: a = iter(f,n).(f.x) & f.x in dom iter(f,n);
  iter(f,n+1) = iter(f,n)*f by FUNCT_7:71;
  then a = iter(f,n+1).x & x in dom iter(f,n+1) by A1,A2,FUNCT_1:21,23;
  hence thesis;
end;

definition
  let f be Function such that
A1: rng f c= dom f;
  let A be set;
  let x be set;
  defpred T[Nat] means
  for a being set st a in dom f holds a in dom iter(f,$1);
A2: dom f \/ rng f = dom f by A1,XBOOLE_1:12;
  then iter(f,0) = id dom f by FUNCT_7:70;
  then
A3: T[0] by FUNCT_1:34;
A4: now
    let i be Element of NAT;
    assume
A5: T[i];
    thus T[i+1]
    proof
      let a be set;
      assume a in dom f;
      then
A6:   a in dom iter(f,i) by A5;
      then
A7:   iter(f,i).a in rng iter(f,i) & rng iter(f,i) c= dom f
      by A2,FUNCT_1:def 5,FUNCT_7:74;
      iter(f,i+1) = f*iter(f,i) by FUNCT_7:73;
      hence thesis by A6,A7,FUNCT_1:21;
    end;
  end;
A8: for i being Element of NAT holds T[i] from NAT_1:sch 1(A3,A4);
  func (A,x) iter f -> Function means

  dom it = dom f &
  for a being set st a in dom f holds (f orbit a c= A implies it.a = x) &
  for n being Nat st iter(f,n).a nin A &
  for i being Nat st i < n holds iter(f,i).a in A holds it.a = iter(f,n).a;
  existence
  proof
    defpred P[set] means f orbit $1 c= A;
    consider Z being set such that
A9: for a being set holds a in Z iff a in dom f & P[a] from XBOOLE_0:sch 1;
A10: Z c= dom f
    proof
      let a be set; thus thesis by A9;
    end;
    defpred Q[set,set] means ex n being Nat st $2 = iter(f,n).$1 & $2 nin A &
    for i being Nat st i < n holds iter(f,i).$1 in A;
A11: for a being set st a in (dom f) \ Z ex b being set st Q[a,b]
    proof
      let a be set;
      assume a in (dom f) \ Z;
      then a in dom f & a nin Z by XBOOLE_0:def 4;
      then not f orbit a c= A by A9;
      then consider y being set such that
A12:  y in f orbit a & y nin A by TARSKI:def 3;
      consider n1 being Element of NAT such that
A13:  y = iter(f,n1).a & a in dom iter(f,n1) by A12;
      defpred R[Nat] means iter(f,$1).a nin A;
A14:  ex n being Nat st R[n] by A12,A13;
      consider n being Nat such that
A15:  R[n] and
A16:  for m being Nat st R[m] holds n <= m from NAT_1:sch 5(A14);
      take b = iter(f,n).a, n; thus b = iter(f,n).a & b nin A by A15;
      let i be Nat;
      thus thesis by A16;
    end;
    consider h being Function such that
A17: dom h = (dom f) \ Z and
A18: for a being set st a in (dom f) \ Z holds Q[a,h.a] from CLASSES1:sch 1(A11
    );
    take g = (Z-->x)+*h;
    dom (Z-->x) = Z by FUNCOP_1:19;
    hence dom g = Z \/ (dom f \ Z) by A17,FUNCT_4:def 1
      .= dom f by A10,XBOOLE_1:45;
    let a be set;
    assume
A19: a in dom f;
    hereby
      assume f orbit a c= A;
      then a in Z by A19,A9;
      then a nin dom f \ Z & (Z-->x).a = x by XBOOLE_0:def 4,FUNCOP_1:13;
      hence g.a = x by A17,FUNCT_4:12;
    end;
    let n be Nat;
    assume
A20: iter(f,n).a nin A & for i being Nat st i < n holds iter(f,i).a in A;
A21: n in NAT by ORDINAL1:def 13;
    then a in dom iter(f,n) by A19,A8;
    then iter(f,n).a in f orbit a by A21;
    then not f orbit a c= A by A20;
    then a nin Z by A9;
    then
A22: a in dom f \ Z by A19,XBOOLE_0:def 4;
    then consider n2 being Nat such that
A23: h.a = iter(f,n2).a & h.a nin A &
    for i being Nat st i < n2 holds iter(f,i).a in A by A18;
    n <= n2 & n2 <= n by A20,A23;
    then n = n2 by XXREAL_0:1;
    hence g.a = iter(f,n).a by A17,A22,A23,FUNCT_4:14;
  end;
  uniqueness
  proof
    let f1,f2 be Function such that
A24: dom f1 = dom f and
A25: for a being set st a in dom f holds (f orbit a c= A implies f1.a = x) &
    for n being Nat st iter(f,n).a nin A &
    for i being Nat st i < n holds iter(f,i).a in A
    holds f1.a = iter(f,n).a and
A26: dom f2 = dom f and
A27: for a being set st a in dom f holds (f orbit a c= A implies f2.a = x) &
    for n being Nat st iter(f,n).a nin A &
    for i being Nat st i < n holds iter(f,i).a in A holds f2.a = iter(f,n).a;
    now
      let a be set;
      assume
A28:  a in dom f;
      per cases;
      suppose
A29:    f orbit a c= A;
        hence f1.a = x by A25,A28
          .= f2.a by A27,A28,A29;
      end;
      suppose not f orbit a c= A;
        then consider y being set such that
A30:    y in f orbit a & y nin A by TARSKI:def 3;
        consider n1 being Element of NAT such that
A31:    y = iter(f,n1).a & a in dom iter(f,n1) by A30;
        defpred R[Nat] means iter(f,$1).a nin A;
A32:    ex n being Nat st R[n] by A30,A31;
        consider n being Nat such that
A33:    R[n] and
A34:    for m being Nat st R[m] holds n <= m from NAT_1:sch 5(A32);
A35:    for i be Nat holds i < n implies iter(f,i).a in A by A34;
        hence f1.a = iter(f,n).a by A25,A28,A33
          .= f2.a by A27,A28,A33,A35;
      end;
    end;
    hence thesis by A24,A26,FUNCT_1:9;
  end;
end;

definition
  let f be Function such that
A1: rng f c= dom f;
  let A be set;
  let g be Function;
  defpred T[Nat] means
  for a being set st a in dom f holds a in dom iter(f,$1);
A2: dom f \/ rng f = dom f by A1,XBOOLE_1:12;
  then iter(f,0) = id dom f by FUNCT_7:70;
  then
A3: T[0] by FUNCT_1:34;
A4: now
    let i be Element of NAT;
    assume
A5: T[i];
    thus T[i+1]
    proof
      let a be set;
      assume a in dom f;
      then
A6:   a in dom iter(f,i) by A5;
      then
A7:   iter(f,i).a in rng iter(f,i) & rng iter(f,i) c= dom f
      by A2,FUNCT_1:def 5,FUNCT_7:74;
      iter(f,i+1) = f*iter(f,i) by FUNCT_7:73;
      hence thesis by A6,A7,FUNCT_1:21;
    end;
  end;
A8: for i being Element of NAT holds T[i] from NAT_1:sch 1(A3,A4);
  func (A,g) iter f -> Function means
  : Def7:
  dom it = dom f &
  for a being set st a in dom f holds (f orbit a c= A implies it.a = g.a) &
  for n being Nat st iter(f,n).a nin A &
  for i being Nat st i < n holds iter(f,i).a in A holds it.a = iter(f,n).a;
  existence
  proof
    defpred P[set] means f orbit $1 c= A;
    consider Z being set such that
A9: for a being set holds a in Z iff a in dom f & P[a] from XBOOLE_0:sch 1;
A10: Z c= dom f
    proof
      let a be set; thus thesis by A9;
    end;
    defpred Q[set,set] means ex n being Nat st $2 = iter(f,n).$1 & $2 nin A &
    for i being Nat st i < n holds iter(f,i).$1 in A;
A11: for a being set st a in (dom f) \ Z ex b being set st Q[a,b]
    proof
      let a be set;
      assume a in (dom f) \ Z;
      then a in dom f & a nin Z by XBOOLE_0:def 4;
      then not f orbit a c= A by A9;
      then consider y being set such that
A12:  y in f orbit a & y nin A by TARSKI:def 3;
      consider n1 being Element of NAT such that
A13:  y = iter(f,n1).a & a in dom iter(f,n1) by A12;
      defpred R[Nat] means iter(f,$1).a nin A;
A14:  ex n being Nat st R[n] by A12,A13;
      consider n being Nat such that
A15:  R[n] and
A16:  for m being Nat st R[m] holds n <= m from NAT_1:sch 5(A14);
      take b = iter(f,n).a, n; thus b = iter(f,n).a & b nin A by A15;
      let i be Nat;
      thus thesis by A16;
    end;
    consider h being Function such that
A17: dom h = (dom f) \ Z and
A18: for a being set st a in (dom f) \ Z holds Q[a,h.a] from CLASSES1:sch 1(A11
    );
    take i = (Z-->0)+*(g|Z)+*h;
    dom (Z-->0) = Z by FUNCOP_1:19;
    then dom ((Z-->0)+*(g|Z)) = Z \/ dom(g|Z) by FUNCT_4:def 1
      .= Z by RELAT_1:87,XBOOLE_1:12;
    hence dom i = Z \/ (dom f \ Z) by A17,FUNCT_4:def 1
      .= dom f by A10,XBOOLE_1:45;
    let a be set;
    assume
A19: a in dom f;
    hereby
      assume f orbit a c= A;
      then
A20:  a in Z by A19,A9;
      then a nin dom f \ Z & (Z-->0).a = 0 by XBOOLE_0:def 4,FUNCOP_1:13;
      then
A21:  i.a = ((Z-->0)+*(g|Z)).a by A17,FUNCT_4:12;
      per cases;
      suppose a in dom(g|Z);
        then i.a = (g|Z).a by A21,FUNCT_4:14;
        hence i.a = g.a by A20,FUNCT_1:72;
      end;
      suppose a nin dom(g|Z);
        then i.a = (Z-->0).a & (Z-->0).a = 0 & a nin dom g
        by A20,A21,FUNCT_4:12,FUNCOP_1:13,RELAT_1:86;
        hence i.a = g.a by FUNCT_1:def 4;
      end;
    end;
    let n be Nat;
    reconsider n' = n as Element of NAT by ORDINAL1:def 13;
    assume
A22: iter(f,n).a nin A & for i being Nat st i < n holds iter(f,i).a in A;
    a in dom iter(f,n') by A19,A8;
    then iter(f,n).a in f orbit a;
    then not f orbit a c= A by A22;
    then a nin Z by A9;
    then
A23: a in dom f \ Z by A19,XBOOLE_0:def 4;
    then consider n2 being Nat such that
A24: h.a = iter(f,n2).a & h.a nin A &
    for i being Nat st i < n2 holds iter(f,i).a in A by A18;
    n <= n2 & n2 <= n by A22,A24;
    then n = n2 by XXREAL_0:1;
    hence i.a = iter(f,n).a by A17,A23,A24,FUNCT_4:14;
  end;
  uniqueness
  proof
    let f1,f2 be Function such that
A25: dom f1 = dom f and
A26: for a being set st a in dom f holds (f orbit a c= A implies f1.a = g.a) &
    for n being Nat st iter(f,n).a nin A &
    for i being Nat st i < n holds iter(f,i).a in A
    holds f1.a = iter(f,n).a and
A27: dom f2 = dom f and
A28: for a being set st a in dom f holds (f orbit a c= A implies f2.a = g.a) &
    for n being Nat st iter(f,n).a nin A &
    for i being Nat st i < n holds iter(f,i).a in A holds f2.a = iter(f,n).a;
    now
      let a be set;
      assume
A29:  a in dom f;
      per cases;
      suppose
A30:    f orbit a c= A;
        hence f1.a = g.a by A26,A29
          .= f2.a by A28,A29,A30;
      end;
      suppose not f orbit a c= A;
        then consider y being set such that
A31:    y in f orbit a & y nin A by TARSKI:def 3;
        consider n1 being Element of NAT such that
A32:    y = iter(f,n1).a & a in dom iter(f,n1) by A31;
        defpred R[Nat] means iter(f,$1).a nin A;
A33:    ex n being Nat st R[n] by A31,A32;
        consider n being Nat such that
A34:    R[n] and
A35:    for m being Nat st R[m] holds n <= m from NAT_1:sch 5(A33);
A36:    for i be Nat holds i < n implies iter(f,i).a in A by A35;
        hence f1.a = iter(f,n).a by A26,A29,A34
          .= f2.a by A28,A29,A34,A36;
      end;
    end;
    hence thesis by A25,A27,FUNCT_1:9;
  end;
end;

theorem Th10:
  for f,g being Function, a,A being set st rng f c= dom f & a in dom f holds
  not f orbit a c= A implies
  ex n being Nat st ((A,g) iter f).a = iter(f,n).a & iter(f,n).a nin A &
  for i being Nat st i < n holds iter(f,i).a in A
proof
  let f,g be Function;
  let a,A be set;
  assume
A1: rng f c= dom f;
  assume
A2: a in dom f;
  assume not f orbit a c= A;
  then consider y being set such that
A3: y in f orbit a & y nin A by TARSKI:def 3;
  consider n1 being Element of NAT such that
A4: y = iter(f,n1).a & a in dom iter(f,n1) by A3;
  defpred R[Nat] means iter(f,$1).a nin A;
A5: ex n being Nat st R[n] by A3,A4;
  consider n being Nat such that
A6: R[n] and
A7: for m being Nat st R[m] holds n <= m from NAT_1:sch 5(A5);
  take n;
  for i being Nat holds i < n implies iter(f,i).a in A by A7;
  hence ((A,g) iter f).a = iter(f,n).a by A1,A2,A6,Def7;
  thus thesis by A6,A7;
end;

theorem Th11:
  for f,g being Function, a,A being set
  st rng f c= dom f & a in dom f & g*f = g holds
  a in A implies ((A,g) iter f).a = ((A,g) iter f).(f.a)
proof
  let f,g be Function;
  let a,A be set;
  assume
A1: rng f c= dom f & a in dom f & g*f = g & a in A;
  then
A2: f.a in rng f by FUNCT_1:def 5;
  then
A3: f orbit (f.a) c= f orbit a by A1,Th9;
  per cases;
  suppose
A4: f orbit a c= A;
    then f orbit (f.a) c= A by A3,XBOOLE_1:1;
    then ((A,g) iter f).(f.a) = g.(f.a) by A1,A2,Def7
      .= g.a by A1,FUNCT_1:
    23;
    hence ((A,g) iter f).a = ((A,g) iter f).(f.a) by A1,A4,Def7;
  end;
  suppose not f orbit a c= A;
    then consider n being Nat such that
A5: ((A,g) iter f).a = iter(f,n).a & iter(f,n).a nin A &
    for i being Nat st i < n holds iter(f,i).a in A by A1,Th10;
    dom f \/ rng f = dom f by A1,XBOOLE_1:12;
    then iter(f,0) = id dom f by FUNCT_7:70;
    then n <> 0 by A1,A5,FUNCT_1:35;
    then n > 0;
    then n >= 0+1 by NAT_1:13;
    then consider i being Nat such that
A6: n = 1+i by NAT_1:10;
    iter(f,n) = iter(f,i)*f by A6,FUNCT_7:71;
    then
A7: iter(f,n).a = iter(f,i).(f.a) by A1,FUNCT_1:23;
    now
      let j be Nat;
      assume j < i;
      then j+1 < n by A6,XREAL_1:10;
      then iter(f,j+1) = iter(f,j)*f & iter(f,j+1).a in A by A5,FUNCT_7:71;
      hence iter(f,j).(f.a) in A by A1,FUNCT_1:23;
    end;
    hence ((A,g) iter f).a = ((A,g) iter f).(f.a) by A1,A2,A5,A7,Def7;
  end;
end;

theorem Th12:
  for f,g being Function, a,A being set st rng f c= dom f & a in dom f holds
  a nin A implies ((A,g) iter f).a = a
proof
  let f,g be Function;
  let a,A be set;
  assume
A1: rng f c= dom f & a in dom f & a nin A;
  then dom f \/ rng f = dom f by XBOOLE_1:12;
  then iter(f,0) = id dom f by FUNCT_7:70;
  then
A2: a = iter(f,0).a by A1,FUNCT_1:35;
  for i being Nat st i < 0 holds iter(f,i).a in A;
  hence ((A,g) iter f).a = a by A1,A2,Def7;
end;

definition
  let X be non empty set;
  let f be Element of Funcs(X,X);
  let A be set;
  let g be Element of Funcs(X,X);
  redefine func (A,g) iter f -> Element of Funcs(X,X);
  coherence
  proof
A1: dom f = X & rng f c= X by FUNCT_2:def 1;
    then
A2: dom ((A,g) iter f) = dom f by Def7;
    rng ((A,g) iter f) c= X
    proof
      let a be set;
      assume a in rng ((A,g) iter f);
      then consider b being set such that
A3:   b in dom ((A,g) iter f) & a = ((A,g) iter f).b by FUNCT_1:def 5;
      reconsider b as Element of X by A1,Def7,A3;
      per cases;
      suppose f orbit b c= A;
        then a = g.b by A1,A3,Def7;
        hence a in X;
      end;
      suppose not f orbit b c= A;
        then consider n being Nat such that
A4:     ((A,g) iter f).b = iter(f,n).b & iter(f,n).b nin A &
        for i being Nat st i < n holds iter(f,i).b in A by A1,Th10;
A5:     n in NAT by ORDINAL1:def 13;
        then dom iter(f,n) = dom f by A1,FUNCT_7:76;
        then rng iter(f,n) c= X & a in rng iter(f,n)
        by A1,A3,A4,A5,FUNCT_7:76,FUNCT_1:12;
        hence a in X;
      end;
    end;
    hence thesis by A1,A2,FUNCT_2:def 2;
  end;
end;

begin :: Free universal algebras

theorem Th13:
  for X being non empty set, S being non empty FinSequence of NAT
  ex A being Universal_Algebra st the carrier of A = X & signature A = S
proof
  let X be non empty set;
  let S be non empty FinSequence of NAT;
A1: dom S = Seg len S & rng S c= NAT by FINSEQ_1:def 3;
  consider x being Element of X;
  defpred P[set,set] means
  ex i,j being Nat st $1 = i & j = S.i & $2 = (j-tuples_on X)--> x;
A2: for y being set st y in dom S ex z being set st P[y,z]
  proof
    let y be set;
    assume y in dom S;
    then reconsider i = y as Element of NAT;
    reconsider j = S.i as Element of NAT;
    take z = (j-tuples_on X)--> x, i, j; thus thesis;
  end;
  consider ch being Function such that
A3: dom ch = dom S & for y being set st y in dom S holds P[y,ch.y]
  from CLASSES1:sch 1(A2);
  reconsider ch as FinSequence by A3,A1,FINSEQ_1:def 2;
  rng ch c= PFuncs(X*,X)
  proof
    let y be set;
    assume y in rng ch;
    then consider xi being set such that
A4: xi in dom ch & y = ch.xi by FUNCT_1:def 5;
    consider i,j being Nat such that
A5: xi = i & j = S.i & y = (j-tuples_on X)--> x by A3,A4;
    dom ((j-tuples_on X)--> x) = (j-tuples_on X) &
    rng ((j-tuples_on X)--> x) c= {x} by FUNCOP_1:19;
    hence thesis by A5,PARTFUN1:def 5;
  end;
  then reconsider ch as PFuncFinSequence of X by FINSEQ_1:def 4;
  set A = UAStr(#X,ch#);
A6: A is quasi_total
  proof
    let n be Nat, h be PartFunc of (the carrier of A)*, the carrier of A;
    assume n in dom the charact of A & h = (the charact of A).n;
    then ex i,j being Nat st n = i & j = S.i & h = (j-tuples_on X)--> x by A3;
    hence thesis;
  end;
A7: A is non-empty
  proof
    thus the charact of A <> {} by A3;
    assume {} in rng the charact of A;
    then consider a being set such that
A8: a in dom ch & {} = ch.a by FUNCT_1:def 5;
    ex i,j being Nat st a = i & j = S.i & {} = (j-tuples_on X)--> x by A8,A3;
    hence thesis;
  end;
  A is partial
  proof
    let n be Nat, h be PartFunc of (the carrier of A)*, the carrier of A;
    assume n in dom the charact of A & h = (the charact of A).n;
    then ex i,j being Nat st n = i & j = S.i & h = (j-tuples_on X)--> x by A3;
    hence thesis;
  end;
  then reconsider A as Universal_Algebra by A6,A7;
  take A;
  thus the carrier of A = X;
A9: len ch = len S by A3,FINSEQ_3:31;
  now
    let n be Nat such that
A10: n in dom S;
    let h be homogeneous non empty PartFunc of (the carrier of A)*,
    the carrier of A;
    assume h = (the charact of A).n;
    then consider i,j being Nat such that
A11: n = i & j = S.i & h = (j-tuples_on X)--> x by A3,A10;
    consider z being Element of j-tuples_on X;
    dom h = j-tuples_on X & len z = j by A11,FUNCOP_1:19,FINSEQ_2:109;
    hence S.n = arity h by A11,UNIALG_1:def 10;
  end;
  hence signature A = S by A9,UNIALG_1:def 11;
end;

theorem Th14:
  for S being non empty FinSequence of NAT
  ex A being Universal_Algebra st the carrier of A = NAT & signature A = S &
  for i,j being Nat st i in dom S & j = S.i
  holds (the charact of A).i = (j-tuples_on NAT) --> i
proof
  set X = NAT;
  let S be non empty FinSequence of NAT;
A1: dom S = Seg len S & rng S c= NAT by FINSEQ_1:def 3;
  defpred P[set,set] means
  ex i,j being Element of NAT st $1 = i & j = S.i & $2 = (j-tuples_on X)-->i;
A2: for y being set st y in dom S ex z being set st P[y,z]
  proof
    let y be set;
    assume y in dom S;
    then reconsider i = y as Element of NAT;
    reconsider j = S.i as Element of NAT;
    take z = (j-tuples_on X)--> i, i, j; thus thesis;
  end;
  consider ch being Function such that
A3: dom ch = dom S & for y being set st y in dom S holds P[y,ch.y]
  from CLASSES1:sch 1(A2);
  reconsider ch as FinSequence by A3,A1,FINSEQ_1:def 2;
  rng ch c= PFuncs(X*,X)
  proof
    let y be set;
    assume y in rng ch;
    then consider xi being set such that
A4: xi in dom ch & y = ch.xi by FUNCT_1:def 5;
    consider i,j being Element of NAT such that
A5: xi = i & j = S.i & y = (j-tuples_on X)--> i by A3,A4;
    dom ((j-tuples_on X)--> i) = (j-tuples_on X) &
    rng ((j-tuples_on X)--> i) c= {i} by FUNCOP_1:19;
    hence thesis by A5,PARTFUN1:def 5;
  end;
  then reconsider ch as PFuncFinSequence of X by FINSEQ_1:def 4;
  set A = UAStr(#X,ch#);
A6: A is quasi_total
  proof
    let n be Nat, h be PartFunc of (the carrier of A)*, the carrier of A;
    assume n in dom the charact of A & h = (the charact of A).n;
    then ex i,j being Element of NAT st
    n = i & j = S.i & h = (j-tuples_on X)--> i by A3;
    hence thesis;
  end;
A7: A is non-empty
  proof
    thus the charact of A <> {} by A3;
    assume {} in rng the charact of A;
    then consider a being set such that
A8: a in dom ch & {} = ch.a by FUNCT_1:def 5;
    ex i,j being Element of NAT st
    a = i & j = S.i & {} = (j-tuples_on X)--> i by A8,A3;
    hence thesis;
  end;
  A is partial
  proof
    let n be Nat, h be PartFunc of (the carrier of A)*, the carrier of A;
    assume n in dom the charact of A & h = (the charact of A).n;
    then ex i,j being Element of NAT st
    n = i & j = S.i & h = (j-tuples_on X)--> i by A3;
    hence thesis;
  end;
  then reconsider A as Universal_Algebra by A6,A7;
  take A;
  thus the carrier of A = X;
A9: len ch = len S by A3,FINSEQ_3:31;
  now
    let n be Nat such that
A10: n in dom S;
    let h be homogeneous non empty PartFunc of (the carrier of A)*,
    the carrier of A;
    assume h = (the charact of A).n;
    then consider i,j being Element of NAT such that
A11: n = i & j = S.i & h = (j-tuples_on X)--> i by A3,A10;
    consider z being Element of j-tuples_on X;
    dom h = j-tuples_on X & len z = j by A11,FUNCOP_1:19,FINSEQ_2:109;
    hence S.n = arity h by A11,UNIALG_1:def 10;
  end;
  hence signature A = S by A9,UNIALG_1:def 11;
  consider A being Universal_Algebra;
  let i,j be Nat;
  assume i in dom S;
  then ex i1,j being Element of NAT st
  i = i1 & j = S.i1 & ch.i = (j-tuples_on X)--> i1 by A3;
  hence thesis;
end;

theorem
  for S being non empty FinSequence of NAT
  for i,j being Nat st i in dom S & j = S.i
  for X being non empty set, f being Function of j-tuples_on X, X
  ex A being Universal_Algebra st the carrier of A = X & signature A = S &
  (the charact of A).i = f
proof
  let S be non empty FinSequence of NAT;
  let i,j be Nat;
  reconsider j' = j as Element of NAT by ORDINAL1:def 13;
  assume
A1: i in dom S & j = S.i;
  let X be non empty set;
  consider A0 being Universal_Algebra such that
A2: the carrier of A0 = X & signature A0 = S by Th13;
  let f be Function of j-tuples_on X, X;
  j'-tuples_on X c= X* by CATALG_1:6;
  then reconsider f0 = f as PartFunc of X*,X by RELSET_1:15;
  consider z being Element of j-tuples_on X;
A3: dom f0 = j-tuples_on X by FUNCT_2:def 1;
  f0 is homogeneous
  proof
    let x,y be FinSequence;
    assume x in dom f0 & y in dom f0;
    then len x = j & len y = j by A3,FINSEQ_2:109;
    hence len x = len y;
  end;
  then reconsider f0 as homogeneous non empty PartFunc of X*,X;
A4: len z = j by FINSEQ_2:109;
  then
A5: arity f0 = j by A3,UNIALG_1:def 10;
  set ch = (the charact of A0)+*(i,f0);
  f0 in PFuncs(X*, X) by PARTFUN1:119;
  then {f0} c= PFuncs(X*,X) & rng the charact of A0 c= PFuncs(X*,X)
  by A2,ZFMISC_1:37;
  then rng ch c= (rng the charact of A0) \/ {f0} &
  (rng the charact of A0) \/ {f0} c= PFuncs(X*, X) by XBOOLE_1:8,POLYNOM1:6;
  then rng ch c= PFuncs(X*, X) by XBOOLE_1:1;
  then reconsider ch as FinSequence of PFuncs(X*,X) by FINSEQ_1:def 4;
A6: dom ch = dom the charact of A0 by FUNCT_7:32;
  set A = UAStr(#X,ch#);
A7: A is quasi_total
  proof
    let n be Nat, h be PartFunc of (the carrier of A)*, the carrier of A;
    assume
A8: n in dom the charact of A & h = (the charact of A).n;
    then (n = i implies h = f0) & (n <> i implies h = (the charact of A0).n) &
    the charact of A0 is quasi_total by A6,FUNCT_7:33,34;
    hence thesis by A2,A5,A3,COMPUT_1:25,A8,A6,UNIALG_1:def 5;
  end;
A9: A is non-empty
  proof
    thus the charact of A <> {} by A6;
    assume {} in rng the charact of A;
    then consider a being set such that
A10: a in dom ch & {} = ch.a by FUNCT_1:def 5;
    reconsider a as Element of NAT by A10;
    (a = i implies {} = f0) & (a <> i implies {} = (the charact of A0).a) &
    {} nin rng the charact of A0 by A10,A6,FUNCT_7:33,34,RELAT_1:def 9;
    hence thesis by A6,A10;
  end;
  A is partial
  proof
    let n be Nat, h be PartFunc of (the carrier of A)*, the carrier of A;
    assume n in dom the charact of A & h = (the charact of A).n;
    then (n = i implies h = f0) & (n <> i implies h = (the charact of A0).n) &
    the charact of A0 is homogeneous by A6,FUNCT_7:33,34;
    hence thesis;
  end;
  then reconsider A as Universal_Algebra by A7,A9;
  take A;
  thus the carrier of A = X;
A11: len S = len the charact of A0 by A2,UNIALG_1:def 11;
  then
A12: dom S = dom the charact of A0 by FINSEQ_3:31;
A13: len S = len the charact of A by A11,A6,FINSEQ_3:31;
  now
    let n be Nat;
    assume
A14: n in dom S;
    let h be homogeneous non empty PartFunc of (the carrier of A )*,
    the carrier of A;
    assume h = (the charact of A).n;
    then (n = i implies h = f0) & (n <> i implies h = (the charact of A0).n)
    by A12,A14,FUNCT_7:33,34;
    hence S.n = arity h by A2,A1,A14,A4,A3,UNIALG_1:def 10,def 11;
  end;
  hence signature A = S by A13,UNIALG_1:def 11;
  thus (the charact of A).i = f by A1,A12,FUNCT_7:33;
end;

registration
  let f be non empty FinSequence of NAT;
  let D be non empty disjoint_with_NAT set;
  cluster -> Relation-like Function-like Element of FreeUnivAlgNSG(f,D);
  coherence
  proof
    let x be Element of FreeUnivAlgNSG(f,D);
    x is Element of TS(DTConUA(f,D));
    hence thesis;
  end;
end;

registration
  let f be non empty FinSequence of NAT;
  let D be non empty disjoint_with_NAT set;
  cluster -> DecoratedTree-like Element of FreeUnivAlgNSG(f,D);
  coherence
  proof
    let x be Element of FreeUnivAlgNSG(f,D);
    x is Element of TS(DTConUA(f,D));
    hence thesis;
  end;
  cluster -> DTree-yielding FinSequence of FreeUnivAlgNSG(f,D);
  coherence;
end;

theorem Th16:
  for G being non empty DTConstrStr for t being set st t in TS G holds
  (ex d being Symbol of G st d in Terminals G & t = root-tree d) or
  (ex o being Symbol of G, p being FinSequence of TS G
  st o ==> roots p & t = o-tree p)
proof
  let G be non empty DTConstrStr;
  let t be set;
  assume that
A1: t in TS G and
A2: not ex d being Symbol of G st d in Terminals G & t = root-tree d and
A3: not ex o being Symbol of G, p being FinSequence of TS G
  st o ==> roots p & t = o-tree p;
A4: (TS G) \ {t} c= TS G by XBOOLE_1:36;
  reconsider Y = (TS G) \ {t} as Subset of FinTrees the carrier of G;
A5: now
    let d be Symbol of G;
    assume d in Terminals G;
    then root-tree d in TS G & root-tree d <> t by A2,DTCONSTR:def 4;
    hence root-tree d in Y by ZFMISC_1:64;
  end;
  now
    let o be Symbol of G, p be FinSequence of Y;
    rng p c= Y by FINSEQ_1:def 4;
    then rng p c= TS G by A4,XBOOLE_1:1;
    then reconsider q = p as FinSequence of TS G by FINSEQ_1:def 4;
    assume o ==> roots p;
    then o-tree q in TS G & t <> o-tree q by A3,DTCONSTR:def 4;
    hence o-tree p in Y by ZFMISC_1:64;
  end;
  then TS G c= Y by A5,DTCONSTR:def 4;
  then t nin {t} by A1,XBOOLE_0:def 4;
  hence contradiction by TARSKI:def 1;
end;

theorem Th17:
  for X being disjoint_with_NAT non empty set
  for S being non empty FinSequence of NAT for i being Nat st i in dom S
  for p being FinSequence of FreeUnivAlgNSG(S,X) st len p = S.i holds
  Den(In(i, dom the charact of FreeUnivAlgNSG(S,X)),FreeUnivAlgNSG(S,X)).p
  = i-tree p
proof
  let X be disjoint_with_NAT non empty set;
  let S be non empty FinSequence of NAT;
  reconsider S' = S as non empty FinSequence of omega;
  set G = DTConUA(S,X);
  set A = FreeUnivAlgNSG(S,X);
  let i be Nat;
  assume
A1: i in dom S;
  then
A2: S'/.i = S.i by PARTFUN1:def 8;
  let p be FinSequence of A;
  assume len p = S.i;
  then p is Element of (S'/.i)-tuples_on TS G by A2,FINSEQ_2:110;
  then p in (S'/.i)-tuples_on TS G;
  then
A3: p in dom FreeOpNSG(i,S,X) by A1,FREEALG:def 11;
  len the charact of A = len S by FREEALG:def 12;
  then dom the charact of A = dom S by FINSEQ_3:31;
  then In(i, dom the charact of A) = i by A1,FUNCT_7:def 1;
  hence Den(In(i, dom the charact of A), A).p
  = FreeOpNSG(i,S,X).p by A1,FREEALG:def 12
    .= Sym(i,S,X)-tree p by A1,A3,FREEALG:def 11
    .= i-tree p by A1,FREEALG:def 10;
end;

definition
  let A be non-empty UAStr;
  let B be Subset of A;
  let n be Nat;
  func B|^n -> Subset of A means
  : Def8:
  ex
  F being Function of NAT, bool the carrier of A st it = F.n & F.0 = B &
  for n being Nat holds F.(n+1) = F.n \/
  {Den(o,A).p where o is (Element of dom the charact of A),
  p is Element of (the carrier of A)*: p in dom Den(o,A) & rng p c= F.n};
  existence
  proof
    defpred P[set,set,set] means
    $3 = $2 \/ {Den(o,A).p where o is (Element of dom the charact of A),
    p is Element of (the carrier of A)*: p in dom Den(o,A) & rng p c= $2};
A1: for n being Element of NAT
    for B1 being Subset of A ex B2 being Subset of A st P[n,B1,B2]
    proof
      let n be Element of NAT, B1 be Subset of A;
      set B2 = B1 \/ {Den(o,A).p where o is (Element of dom the charact of A),
      p is Element of (the carrier of A)*: p in dom Den(o,A) & rng p c= B1};
      B2 c= the carrier of A
      proof
        let x be set;
        assume
A2:     x in B2 & not x in the carrier of A;
        x in B1 implies x in the carrier of A;
        then x in {Den(o,A).p where o is (Element of dom the charact of A),
        p is Element of (the carrier of A)*: p in dom Den(o,A) & rng p c= B1}
        by A2,XBOOLE_0:def 2;
        then consider o being (Element of dom the charact of A), p being
        Element of (the carrier of A)* such that
A3:     x = Den(o,A).p & p in dom Den(o,A) & rng p c= B1;
        x in rng Den(o,A) by A3,FUNCT_1:def 5;
        hence contradiction by A2;
      end;
      then reconsider B2 as Subset of A;
      take B2;
      thus P[n,B1,B2];
    end;
    consider F being Function of NAT, bool the carrier of A such that
A4: F.0 = B & for n being Element of NAT holds P[n,F.n,F.(n+1)]
    from RECDEF_1:sch 2(A1);
    reconsider n' = n as Element of NAT by ORDINAL1:def 13;
    take a = F.n', F; thus a = F.n & F.0 = B by A4;
    let n be Nat;
    n in NAT by ORDINAL1:def 13;
    hence thesis by A4;
  end;
  uniqueness
  proof
    let C1,C2 be Subset of A;
    deffunc Rec(set,set) = $2 \/
    {Den(o,A).p where o is (Element of dom the charact of A),
    p is Element of (the carrier of A)*: p in dom Den(o,A) & rng p c= $2};
    given F1 being Function of NAT, bool the carrier of A such that
A5: C1 = F1.n and
A6: F1.0 = B & for n being Nat holds F1.(n+1) = Rec(n,F1.n);
    given F2 being Function of NAT, bool the carrier of A such that
A7: C2 = F2.n and
A8: F2.0 = B & for n being Nat holds F2.(n+1) = Rec(n,F2.n);
A9: dom F1 = NAT by FUNCT_2:def 1;
B9: F1.0 = B by A6;
C9: for n being Nat holds F1.(n+1) = Rec(n,F1.n) by A6;
A10: dom F2 = NAT by FUNCT_2:def 1;
B10: F2.0 = B by A8;
C10: for n being Nat holds F2.(n+1) = Rec(n,F2.n) by A8;
    F1 = F2 from NAT_1:sch 15(A9,B9,C9,A10,B10,C10);
    hence thesis by A5,A7;
  end;
end;

theorem Th18:
  for A being Universal_Algebra, B being Subset of A holds B|^0 = B
proof
  let A be Universal_Algebra;
  let B be Subset of A;
  ex F being Function of NAT, bool the carrier of A st B|^0 = F.0 & F.0 = B &
  for n being Nat holds F.(n+1) = F.n \/ {Den(o,A).p where o is (Element of
  dom the charact of A), p is Element of (the carrier of A)*: p in dom
  Den(o,A) & rng p c= F.n} by Def8;
  hence B|^0 = B;
end;

theorem Th19:
  for A being Universal_Algebra, B being Subset of A for n being Nat
  holds B|^(n+1) = (B|^n) \/ {Den(o,A).p
  where o is (Element of dom the charact of A),
  p is Element of (the carrier of A)*: p in dom Den(o,A) & rng p c= B|^n}
proof
  let A be Universal_Algebra;
  let B be Subset of A;
  let n be Nat;
  deffunc Rec(set,set) = $2 \/
  {Den(o,A).p where o is (Element of dom the charact of A),
  p is Element of (the carrier of A)*: p in dom Den(o,A) & rng p c= $2};
  consider F1 being Function of NAT, bool the carrier of A such that
A1: B|^(n) = F1.(n) and
A2: F1.0 = B & for n being Nat holds F1.(n+1) = Rec(n,F1.n) by Def8;
  consider F2 being Function of NAT, bool the carrier of A such that
A3: B|^(n+1) = F2.(n+1) and
A4: F2.0 = B & for n being Nat holds F2.(n+1) = Rec(n,F2.n) by Def8;
A5: dom F1 = NAT by FUNCT_2:def 1;
B5: F1.0 = B by A2;
C5: for n being Nat holds F1.(n+1) = Rec(n,F1.n) by A2;
A6: dom F2 = NAT by FUNCT_2:def 1;
B6: F2.0 = B by A4;
C6: for n being Nat holds F2.(n+1) = Rec(n,F2.n) by A4;
  F1 = F2 from NAT_1:sch 15(A5,B5,C5,A6,B6,C6);
  hence thesis by A1,A2,A3;
end;

theorem Th20:
  for A being Universal_Algebra, B being Subset of A for n being Nat
  for x being set holds x in B|^(n+1) iff x in B|^n or
  ex o being Element of dom the charact of A st
  ex p being Element of (the carrier of A)*
  st x = Den(o,A).p & p in dom Den(o,A) & rng p c= B|^n
proof
  let A be Universal_Algebra;
  let B be Subset of A;
  let n be Nat;
  set Z = {Den(o,A).p where o is (Element of dom the charact of A),
  p is Element of (the carrier of A)*: p in dom Den(o,A) & rng p c= B|^n};
  let x be set;
  B|^(n+1) = (B|^n) \/ Z by Th19;
  then x in B|^(n+1) iff x in B|^n or x in Z by XBOOLE_0:def 2;
  hence thesis;
end;

theorem Th21:
  for A being Universal_Algebra, B being Subset of A
  for n,m being Nat st n <= m holds B|^n c= B|^m
proof
  let A be Universal_Algebra;
  let B be Subset of A;
  let n,m be Nat;
  assume n <= m;
  then consider i being Nat such that
A1: m = n+i by NAT_1:10;
  defpred P[Nat] means B|^n c= B|^(n+$1);
A2: P[0];
A3: now
    let i be Nat;
    assume
A4: P[i];
    deffunc Rec(set,set) = $2 \/
    {Den(o,A).p where o is (Element of dom the charact of A),
    p is Element of (the carrier of A)*: p in dom Den(o,A) & rng p c= $2};
    B|^(n+i+1) = Rec(n,B|^(n+i)) by Th19;
    then B|^(n+i) c= B|^(n+(i+1)) by XBOOLE_1:7;
    hence P[i+1] by A4,XBOOLE_1:1;
  end;
  for i being Nat holds P[i] from NAT_1:sch 2(A2,A3);
  hence B|^n c= B|^m by A1;
end;

theorem Th22:
  for A being Universal_Algebra for B1,B2 being Subset of A st B1 c= B2
  for n being Nat holds B1|^n c= B2|^n
proof
  let A be Universal_Algebra;
  let B1,B2 be Subset of A such that
A1: B1 c= B2;
  defpred P[Nat] means B1|^$1 c= B2|^$1;
  B1|^0 = B1 by Th18;
  then
A2: P[0] by A1,Th18;
A3: now
    let n be Nat;
    assume
A4: P[n];
    thus P[n+1]
    proof
      let x be set;
      assume
A5:   x in B1|^(n+1) & x nin B2|^(n+1);
      then reconsider a = x as Element of A;
      a nin B1|^n by A5,Th20,A4;
      then consider o being (Element of dom the charact of A),
      p being Element of (the carrier of A)* such that
A6:   a = Den(o,A).p & p in dom Den(o,A) & rng p c= B1|^n by A5,Th20;
      rng p c= B2|^n by A4,A6,XBOOLE_1:1;
      hence contradiction by A5,A6,Th20;
    end;
  end;
  for n being Nat holds P[n] from NAT_1:sch 2(A2,A3);
  hence thesis;
end;

theorem Th23:
  for A being Universal_Algebra, B being Subset of A for n being Nat
  for x being set holds x in B|^(n+1) iff x in B or
  ex o being Element of dom the charact of A st
  ex p being Element of (the carrier of A)*
  st x = Den(o,A).p & p in dom Den(o,A) & rng p c= B|^n
proof
  let A be Universal_Algebra;
  let B be Subset of A;
  defpred P[Nat] means for x being set st x in B|^($1+1) holds x in B or
  ex o being Element of dom the charact of A st
  ex p being Element of (the carrier of A)*
  st x = Den(o,A).p & p in dom Den(o,A) & rng p c= B|^$1;
A1: B|^0 = B by Th18;
  then
A2: P[0] by Th20;
A3: now
    let n be Nat such that
A4: P[n];
    thus P[n+1]
    proof
      let x be set;
      assume x in B|^(n+1+1);
      then
A5:   x in B|^(n+1) or ex o being Element of dom the charact of A st
      ex p being Element of (the carrier of A)*
      st x = Den(o,A).p & p in dom Den(o,A) & rng p c= B|^(n+1) by Th20;
      now
        given o being (Element of dom the charact of A),
        p being Element of (the carrier of A)* such that
A6:     x = Den(o,A).p & p in dom Den(o,A) & rng p c= B|^n;
        take o,p;
        n <= n+1 by NAT_1:13;
        then B|^n c= B|^(n+1) by Th21;
        hence x = Den(o,A).p & p in dom Den(o,A) & rng p c= B|^(n+1)
        by A6,XBOOLE_1:1;
      end;
      hence thesis by A4,A5;
    end;
  end;
A7: for n being Nat holds P[n] from NAT_1:sch 2(A2,A3);
  let n be Nat;
  let x be set;
  B c= B|^n by A1,Th21;
  hence thesis by A7,Th20;
end;

scheme MaxVal{A() -> non empty set, B() -> set, P[set,set]}: ex n being Nat st
  for x being Element of A() st x in B() holds P[x,n]
provided
A1: B() is finite
and
A2: for x being Element of A() st x in B() ex n being Nat st P[x,n]
and
A3: for x being Element of A()
for n,m being Nat st P[x,n] & n <= m holds P[x,m]
proof
A4: for x being set st x in A()/\B() ex y being set st y in NAT & P[x,y]
  proof
    let x be set;
    assume
A5: x in A()/\B();
    then reconsider x as Element of A() by XBOOLE_0:def 3;
    x in B() by A5,XBOOLE_0:def 3;
    then consider n being Nat such that
A6: P[x,n] by A2;
    n is Element of NAT by ORDINAL1:def 13;
    hence thesis by A6;
  end;
  consider f being Function such that
A7: dom f = A()/\B() & rng f c= NAT and
A8: for x being set st x in A()/\B() holds P[x,f.x] from WELLORD2:sch 1(A4);
  dom f is finite by A7,A1;
  then reconsider Z = rng f as finite Subset of NAT by A7,FINSET_1:26;
  consider n being Element of NAT such that
A9: for i being Element of NAT st i in Z holds i <= n by STIRL2_1:66;
  take n;
  let x be Element of A();
  assume x in B();
  then
A10: x in A()/\B() by XBOOLE_0:def 3;
  then
A11: f.x in rng f by A7,FUNCT_1:def 5;
  then reconsider i = f.x as Element of NAT by A7;
  i <= n & P[x,i] by A8,A10,A9,A11;
  hence thesis by A3;
end;

theorem Th24:
  for A being Universal_Algebra, B being Subset of A ex C being Subset of A
  st C = union {B|^n where n is Element of NAT: not contradiction} &
  C is opers_closed
proof
  let A be Universal_Algebra;
  let B be Subset of A;
  set X = {B|^n where n is Element of NAT: not contradiction};
  set C = union X;
A1: union bool the carrier of A = the carrier of A by ZFMISC_1:99;
  X c= bool the carrier of A
  proof
    let x be set;
    assume x in X;
    then ex n being Element of NAT st x = B|^n;
    hence thesis;
  end;
  then reconsider C as Subset of A by A1,ZFMISC_1:95;
  take C; thus C = union {B|^n where n is Element of NAT: not contradiction};
  let o be Element of Operations A;
  consider s being set such that
A2: s in dom the charact of A & o = (the charact of A).s by FUNCT_1:def 5;
  reconsider s as OperSymbol of A by A2;
A3: dom o = (arity o)-tuples_on the carrier of A by UNIALG_2:2;
  let p be FinSequence of C;
  assume len p = arity o;
  then p is Element of dom Den(s,A) by A3,A2,FINSEQ_2:110;
  then
A4: p in dom Den(s,A) by A3,A2;
  defpred P[set,Nat] means $1 in B|^$2;
A5: rng p is finite;
A6: for x being Element of A st x in rng p ex n being Nat st P[x,n]
  proof
    let x be Element of A;
    assume
A7: x in rng p;
    rng p c= C by FINSEQ_1:def 4;
    then consider Y being set such that
A8: x in Y & Y in X by A7,TARSKI:def 4;
    consider n being Element of NAT such that
A9: Y = B|^n by A8;
    take n;
    thus P[x,n] by A8,A9;
  end;
A10: for x being Element of A
  for n,m being Nat st P[x,n] & n <= m holds P[x,m]
  proof
    let x be Element of A;
    let n,m be Nat;
    assume
A11: P[x,n];
    assume n <= m;
    then B|^n c= B|^m by Th21;
    hence thesis by A11;
  end;
  consider n being Nat such that
A12: for x being Element of A st x in rng p holds P[x,n] from MaxVal(A5,A6,A10
  );
  rng p c= B|^n
  proof
    let x be set;
    assume x in rng p;
    hence thesis by A12;
  end;
  then Den(s,A).p in {Den(a,A).r where a is (Element of dom the charact of A
  ), r is Element of (the carrier of A)*: r in dom Den(a,A) & rng r c= B|^n}
  by A4;
  then o.p in (B|^n)\/{Den(a,A).r where a is (Element of dom the charact of
  A),
  r is Element of (the carrier of A)*: r in dom Den(a,A) & rng r c= B|^n} &
  n+1 in NAT by A2,XBOOLE_0:def 2;
  then o.p in B|^(n+1) & B|^(n+1) in X by Th19;
  hence o.p in C by TARSKI:def 4;
end;

theorem Th25:
  for A being Universal_Algebra, B,C being Subset of A
  st C is opers_closed & B c= C
  holds union {B|^n where n is Element of NAT: not contradiction} c= C
proof
  let A be Universal_Algebra;
  let B,C be Subset of A;
  assume
A1: C is opers_closed;
  assume
A2: B c= C;
  let z be set;
  assume z in union {B|^n where n is Element of NAT: not contradiction};
  then consider Y being set such that
A3: z in Y & Y in {B|^n where n is Element of NAT: not contradiction}
  by TARSKI:def 4;
  consider n being Element of NAT such that
A4: Y = B|^n by A3;
  defpred P[Nat] means B|^$1 c= C;
A5: P[0] by A2,Th18;
A6: now
    let n be Nat;
    assume
A7: P[n];
    thus P[n+1]
    proof
      let x be set;
      assume
A8:   x in B|^(n+1) & x nin C;
      then x in (B|^n)\/{Den(o,A).p where o is (Element of dom the charact
      of A),
      p is Element of (the carrier of A)*: p in dom Den(o,A) & rng p c= B|^n}
      by Th19;
      then x in B|^n or
      x in {Den(o,A).p where o is (Element of dom the charact of A),
      p is Element of (the carrier of A)*: p in dom Den(o,A) & rng p c= B|^n}
      by XBOOLE_0:def 2;
      then consider o being (Element of dom the charact of A), p being Element
      of (the carrier of A)* such that
A9:   x = Den(o,A).p & p in dom Den(o,A) & rng p c= B|^n by A8,A7;
      rng p c= C by A9,A7,XBOOLE_1:1;
      then reconsider p as FinSequence of C by FINSEQ_1:def 4;
      reconsider oo = Den(o,A) as Element of Operations A;
      len p = arity oo & C is_closed_on oo
      by A1,A9,UNIALG_1:def 10,UNIALG_2:def 5;
      hence thesis by A8,A9,UNIALG_2:def 4;
    end;
  end;
  for n being Nat holds P[n] from NAT_1:sch 2(A5,A6);
  then P[n];
  hence thesis by A3,A4;
end;

definition
  let A be Universal_Algebra;
  func Generators A -> Subset of A equals

  (the carrier of A) \
  union {rng o where o is Element of Operations A: not contradiction};
  coherence;
end;

theorem Th26:
  for A being Universal_Algebra, a being Element of A holds
  a in Generators A iff not ex o being Element of Operations A st a in rng o
proof
  let A be Universal_Algebra;
  set Z = {rng o where o is Element of Operations A: not contradiction};
  let a be Element of A;
  hereby
    assume a in Generators A;
    then
A1: a nin union Z by XBOOLE_0:def 4;
    given o being Element of Operations A such that
A2: a in rng o;
    rng o in Z;
    hence contradiction by A1,A2,TARSKI:def 4;
  end;
  assume
A3: not ex o being Element of Operations A st a in rng o;
  assume a nin Generators A;
  then a in union Z by XBOOLE_0:def 4;
  then consider X being set such that
A4: a in X & X in Z by TARSKI:def 4;
  ex o being Element of Operations A st X = rng o by A4;
  hence contradiction by A3,A4;
end;

theorem
  for A being Universal_Algebra for B being Subset of A st B is opers_closed
  holds Constants A c= B
proof
  let A be Universal_Algebra;
  let B be Subset of A such that
A1: B is opers_closed;
  let x be set;
  assume x in Constants A;
  then consider a being Element of A such that
A2: x = a & ex o being Element of Operations A st arity o = 0 & a in rng o;
  consider o being Element of Operations A such that
A3: arity o = 0 & a in rng o by A2;
  consider s being set such that
A4: s in dom o & a = o.s by A3,FUNCT_1:def 5;
A5: dom o = 0-tuples_on the carrier of A by A3,UNIALG_2:2;
  reconsider s as Element of (the carrier of A)* by A4;
A6: len s = 0 by A4,A5,FINSEQ_2:109;
  then s = {};
  then rng s c= B by XBOOLE_1:2,RELAT_1:60;
  then s is FinSequence of B & B is_closed_on o
  by FINSEQ_1:def 4,A1,UNIALG_2:def 5;
  hence x in B by A2,A3,A4,A6,UNIALG_2:def 4;
end;

theorem Th28:
  for A being Universal_Algebra st Constants A = {} holds {} A is opers_closed
proof
  let A be Universal_Algebra such that
A1: Constants A = {};
  let o be Element of Operations A;
  let s be FinSequence of {} A;
  assume
A2: len s = arity o;
A3: {} A c= the carrier of A & rng s c= {} A by FINSEQ_1:def 4;
  s is Element of (arity o)-tuples_on the carrier of A &
  dom o = (arity o)-tuples_on the carrier of A by A2,FINSEQ_2:110,UNIALG_2:2;
  then
A4: o.s in rng o by FUNCT_1:def 5;
  then reconsider a = o.s as Element of A;
  a nin Constants A by A1;
  then s <> {} by A2,A4,CARD_1:47;
  hence thesis by A3;
end;

theorem
  for A being Universal_Algebra st Constants A = {}
  for G being GeneratorSet of A holds G <> {}
proof
  let A be Universal_Algebra such that
A1: Constants A = {};
  let G be GeneratorSet of A;
  assume
A2: G = {};
  then G = {} A;
  then G is opers_closed & G c= G & the carrier of A <> {} by A1,Th28;
  hence thesis by A2,FREEALG:def 5;
end;

theorem Th30:
  for A being Universal_Algebra for G being Subset of A
  holds G is GeneratorSet of A iff
  for I being Element of A ex n being Nat st I in G|^n
proof
  let A be Universal_Algebra;
  let B be Subset of A;
  set X = {B|^n where n is Element of NAT: not contradiction};
  consider C being Subset of A such that
A1: C = union X & C is opers_closed by Th24;
  B|^0 = B by Th18;
  then
A2: B in X;
  consider o being Element of Operations A;
  thus B is GeneratorSet of A implies for I being Element of A
  ex n being Nat st I in B|^n
  proof
    assume for D being Subset of A st D is opers_closed & B c= D
    holds D = the carrier of A;
    then
A3: C = the carrier of A by A1,A2,ZFMISC_1:92;
    let I be Element of A;
    consider Y being set such that
A4: I in Y & Y in X by A3,A1,TARSKI:def 4;
    ex n being Element of NAT st Y = B|^n by A4;
    hence thesis by A4;
  end;
  assume
A5: for I being Element of A ex n being Nat st I in B|^n;
  let D be Subset of A;
  assume D is opers_closed & B c= D;
  then
A6: union X c= D by Th25;
  thus D c= the carrier of A;
  let x be set;
  assume x in the carrier of A;
  then reconsider I = x as Element of A;
  consider n being Nat such that
A7: I in B|^n by A5;
  reconsider n as Element of NAT by ORDINAL1:def 13;
  B|^n in X;
  then I in union X by A7,TARSKI:def 4;
  hence thesis by A6;
end;

theorem Th31:
  for A being Universal_Algebra for B being Subset of A
  for G being GeneratorSet of A st G c= B holds B is GeneratorSet of A
proof
  let A be Universal_Algebra;
  let B be Subset of A;
  let G be GeneratorSet of A such that
A1: G c= B;
  now
    let a be Element of A;
    consider n being Nat such that
A2: a in G|^n by Th30;
    take n;
    G|^n c= B|^n by A1,Th22;
    hence a in B|^n by A2;
  end;
  hence thesis by Th30;
end;

theorem Th32:
  for A being Universal_Algebra for G being GeneratorSet of A
  for a being Element of A
  st not ex o being Element of Operations A st a in rng o holds a in G
proof
  let A be Universal_Algebra;
  let G be GeneratorSet of A;
  let a be Element of A;
  assume
A1: for o being Element of Operations A holds a nin rng o;
  defpred P[Nat] means a nin G|^$1;
  assume a nin G;
  then
A2: P[0] by Th18;
A3: now
    let n be Nat;
    assume
A4: P[n];
    thus P[n+1]
    proof
      assume a in G|^(n+1);
      then a in (G|^n) \/ {Den(o,A).p
      where o is (Element of dom the charact of A),
      p is Element of (the carrier of A)*: p in dom Den(o,A) & rng p c= G|^n}
      by Th19;
      then a in {Den(o,A).p where o is (Element of dom the charact of A),
      p is Element of (the carrier of A)*: p in dom Den(o,A) & rng p c= G|^n}
      by A4,XBOOLE_0:def 2;
      then consider o being (Element of dom the charact of A), p being
      Element of (the carrier of A)* such that
A5:   a = Den(o,A).p & p in dom Den(o,A) & rng p c= G|^n;
      Den(o,A) in Operations A & a in rng Den(o,A) by A5,FUNCT_1:def 5;
      hence contradiction by A1;
    end;
  end;
  for n being Nat holds P[n] from NAT_1:sch 2(A2,A3);
  hence contradiction by Th30;
end;

theorem
  for A being Universal_Algebra, G being GeneratorSet of A
  holds Generators A c= G
proof
  let A be Universal_Algebra;
  let G be GeneratorSet of A;
  let a be set;
  assume
A1: a in Generators A;
  then
A2: a nin union {rng o where o is Element of
  Operations A: not contradiction} by XBOOLE_0:def 4;
  reconsider I = a as Element of A by A1;
  assume a nin G;
  then consider o0 being Element of Operations A such that
A3: I in rng o0 by Th32;
  rng o0 in {rng o where o is Element of Operations A: not contradiction};
  hence contradiction by A2,A3,TARSKI:def 4;
end;

theorem Th34:
  for A being free Universal_Algebra for G being free GeneratorSet of A
  holds G = Generators A
proof
  let A be free Universal_Algebra;
  let G be free GeneratorSet of A;
  reconsider S = signature A as non empty FinSequence of NAT by MSUALG_1:9;
  consider B being Universal_Algebra such that
A1: the carrier of B = NAT & signature B = S and
A2: for i,j being Nat st i in dom S & j = S.i
  holds (the charact of B).i = (j-tuples_on NAT) --> i by Th14;
  reconsider f = G --> 0 as Function of G, the carrier of B by A1;
  A,B are_similar by A1,UNIALG_2:def 2;
  then consider h being Function of A,B such that
A3: h is_homomorphism A,B & h|G = f by FREEALG:def 6;
  len S = len the charact of B & len S = len the charact of A
  by A1,UNIALG_1:def 11;
  then
A4: dom S = dom the charact of B & dom S = dom the charact of A by
  FINSEQ_3:31;
  thus G c= Generators A
  proof
    let a be set;
    assume
A5: a in G;
    then reconsider I = a as Element of A;
    assume not thesis;
    then I in union {rng o where o is Element of Operations A: not
    contradiction} by XBOOLE_0:def 4;
    then consider Y being set such that
A6: I in Y & Y in{rng o where o is Element of Operations A:not contradiction}
    by TARSKI:def 4;
    consider o being Element of Operations A such that
A7: Y = rng o by A6;
    consider i being set such that
A8: i in dom the charact of A & o = (the charact of A).i by FUNCT_1:def 5;
    reconsider i as Element of NAT by A8;
    reconsider j = S.i as Element of NAT;
    reconsider o2 = (the charact of B).i as Element of Operations B
    by A4,A8,FUNCT_1:def 5;
    consider x being set such that
A9: x in dom o & I = o.x by A6,A7,FUNCT_1:def 5;
A10: dom o = (arity o)-tuples_on the carrier of A by UNIALG_2:2;
    reconsider x as FinSequence of A by A9,FINSEQ_1:def 11;
    reconsider hx = h*x as FinSequence of NAT by A1;
    len (h*x) = len x by FINSEQ_2:37
      .= arity o by A10,A9,FINSEQ_2:109
      .= j by A4,A8,UNIALG_1:def 11;
    then
A11: hx is Element of j-tuples_on NAT by FINSEQ_2:110;
    0 = f.I by A5,FUNCOP_1:13
      .= h.(o.x) by A3,A5,A9,FUNCT_1:72
      .= o2.(h*x) by A3,A8,A9,ALG_1:def 1
      .= ((j-tuples_on NAT) --> i).(h*x) by A2,A4,A8
      .= i by A11,FUNCOP_1:13;
    hence contradiction by A8,FINSEQ_3:27;
  end;
  let a be set;
  assume
A12: a in Generators A;
  then
A13: a in the carrier of A & a nin union {rng o where o is Element of
  Operations A: not contradiction} by XBOOLE_0:def 4;
  reconsider I = a as Element of A by A12;
  assume a nin G;
  then consider o0 being Element of Operations A such that
A14: I in rng o0 by Th32;
  rng o0 in {rng o where o is Element of Operations A: not contradiction};
  hence contradiction by A13,A14,TARSKI:def 4;
end;

registration
  let A be free Universal_Algebra;
  cluster Generators A -> free GeneratorSet of A;
  coherence
  proof
    consider G being free GeneratorSet of A;
    Generators A = G by Th34;
    hence thesis;
  end;
end;

definition
  let A be free Universal_Algebra;
  redefine func Generators A -> GeneratorSet of A;
  coherence
  proof
    consider G being free GeneratorSet of A;
    Generators A = G by Th34;
    hence thesis;
  end;
end;

registration
  let A,B be set;
  cluster [:A,B:] -> disjoint_with_NAT;
  coherence
  proof
    now
      let z be set;
      assume z in [:A,B:] & z in NAT;
      then z is Element of NAT &
      ex a,b being set st a in A & b in B & z = [a,b] by ZFMISC_1:def 2;
      hence contradiction;
    end;
    hence [:A,B:] misses NAT by XBOOLE_0:3;
  end;
end;

theorem
  for A being free Universal_Algebra for G being GeneratorSet of A
  for B being Universal_Algebra for h1,h2 being Function of A,B
  st h1 is_homomorphism A,B & h2 is_homomorphism A,B & h1|G = h2|G
  holds h1 = h2
proof
  let A be free Universal_Algebra;
  let G be GeneratorSet of A;
  let B be Universal_Algebra;
  let h1,h2 be Function of A,B such that
A1: h1 is_homomorphism A,B & h2 is_homomorphism A,B & h1|G = h2|G;
  defpred P[Nat] means
  for a being Element of A st a in G|^$1 holds h1.a = h2.a;
A2: P[0]
  proof
    let a be Element of A;
    assume a in G|^0;
    then a in G by Th18;
    then h1.a = (h1|G).a & h2.a = (h2|G).a by FUNCT_1:72;
    hence thesis by A1;
  end;
A3: for n being Nat st P[n] holds P[n+1]
  proof
    let n be Nat such that
A4: P[n];
    let a be Element of A;
    assume
A5: a in G|^(n+1) & h1.a <> h2.a;
    then a nin G|^n by A4;
    then consider o being (Element of dom the charact of A),
    p being Element of (the carrier of A)* such that
A6: a = Den(o,A).p & p in dom Den(o,A) & rng p c= G|^n by A5,Th20;
    A,B are_similar by A1,ALG_1:def 1;
    then len the charact of A = len the charact of B by UNIALG_2:3;
    then reconsider o' = o as Element of dom the charact of B by FINSEQ_3:31;
    Operations A = rng the charact of A & Operations B = rng the charact of B;
    then
A7: h1.a = Den(o',B).(h1*p) & h2.a = Den(o',B).(h2*p) by A6,A1,ALG_1: def 1;
    now
      dom h1 = the carrier of A & dom h2 = the carrier of A by FUNCT_2:def 1;
      hence G|^n c= dom h1 & G|^n c= dom h2;
      let x be set;
      assume x in G|^n;
      hence h1.x = h2.x by A4;
    end;
    hence thesis by A5,A7,A6,Th1;
  end;
A8: for n being Nat holds P[n] from NAT_1:sch 2(A2,A3);
  now
    let a be Element of A;
    ex n being Nat st a in G|^n by Th30;
    hence h1.a = h2.a by A8;
  end;
  hence h1 = h2 by FUNCT_2:113;
end;

Lm2: for A being free Universal_Algebra for o1,o2 being OperSymbol of A
for p1,p2 being FinSequence st p1 in dom Den(o1,A) & p2 in dom Den(o2,A)
holds Den(o1,A).p1 = Den(o2,A).p2 implies o1 = o2
proof
  let A be free Universal_Algebra;
  consider G being free GeneratorSet of A;
  let o1,o2 be OperSymbol of A;
  let p1,p2 be FinSequence such that
A1: p1 in dom Den(o1,A) & p2 in dom Den(o2,A) and
A2: Den(o1,A).p1 = Den(o2,A).p2;
  reconsider S = signature A as non empty FinSequence of NAT by MSUALG_1:9;
  consider B being Universal_Algebra such that
A3: the carrier of B = NAT & signature B = S and
A4: for i,j being Nat st i in dom S & j = S.i
  holds (the charact of B).i = (j-tuples_on NAT) --> i by Th14;
  reconsider f = G --> 0 as Function of G, the carrier of B by A3;
  A,B are_similar by A3,UNIALG_2:def 2;
  then consider h being Function of A,B such that
A5: h is_homomorphism A,B & h|G = f by FREEALG:def 6;
A6: len S = len the charact of B & len S = len the charact of A
  by A3,UNIALG_1:def 11;
  then
A7: dom S = dom the charact of B & dom S = dom the charact of A
  by FINSEQ_3:31;
  reconsider b1 = o1, b2 = o2 as OperSymbol of B by A6,FINSEQ_3:31;
  reconsider n1 = o1, n2 = o2 as Element of NAT;
  reconsider j1 = S.n1, j2 = S.n2 as Element of NAT;
  reconsider x1 = p1, x2 = p2 as FinSequence of A by A1,FINSEQ_1:def 11;
  reconsider h1 = h*x1, h2 = h*x2 as FinSequence of NAT by A3;
  reconsider oo1 = Den(o1,A), oo2 = Den(o2,A) as Element of Operations A;
A8: dom oo1 = (arity oo1)-tuples_on the carrier of A &
  dom oo2 = (arity oo2)-tuples_on the carrier of A by UNIALG_2:2;
  then len x1 = arity oo1 by A1,FINSEQ_2:109
    .= j1 by A7,UNIALG_1:def 11;
  then len h1 = j1 by FINSEQ_2:37;
  then
A9: h1 is Element of j1-tuples_on NAT by FINSEQ_2:110;
  len x2 = arity oo2 by A8,A1,FINSEQ_2:109
    .= j2 by A7,UNIALG_1:def 11;
  then len h2 = j2 by FINSEQ_2:37;
  then
A10: h2 is Element of j2-tuples_on NAT by FINSEQ_2:110;
  Den(o1,A) = (the charact of A).n1 & Den(o1,A) is Element of Operations A &
  Den(b1,B) = (the charact of B).n1 & Den(b1,B) is Element of Operations B &
  Den(o2,A) = (the charact of A).n2 & Den(o2,A) is Element of Operations A &
  Den(b2,B) = (the charact of B).n2 & Den(b2,B) is Element of Operations B;
  then
A11: h.(Den(o1,A).x1) = Den(b1,B).h1 & h.(Den(o2,A).x2) = Den(b2,B).h2
  by A1,A5,ALG_1:def 1;
  Den(b1,B) = (j1-tuples_on NAT)-->n1 & Den(b2,B) = (j2-tuples_on NAT)-->n2
  by A4,A7;
  then Den(b1,B).h1 = n1 & Den(b2,B).h2 = n2 by A9,A10,FUNCOP_1:13;
  hence o1 = o2 by A2,A11;
end;

theorem Th36:
  for A being free Universal_Algebra for o1,o2 being OperSymbol of A
  for p1,p2 being FinSequence st p1 in dom Den(o1,A) & p2 in dom Den(o2,A)
  holds Den(o1,A).p1 = Den(o2,A).p2 implies o1 = o2 & p1 = p2
proof
  let A be free Universal_Algebra;
  consider G being free GeneratorSet of A;
  let o1,o2 be OperSymbol of A;
  let p1,p2 be FinSequence such that
A1: p1 in dom Den(o1,A) & p2 in dom Den(o2,A) and
A2: Den(o1,A).p1 = Den(o2,A).p2; thus
A3: o1 = o2 by A1,A2,Lm2;
  reconsider S = signature A as non empty FinSequence of NAT by MSUALG_1:9;
  set G' = G \/ {the carrier of A};
  reconsider G' as non empty set;
  deffunc F(set) = root-tree [0,$1];
  consider g being Function such that
A4: dom g = G & for x being set st x in G holds g.x = F(x) from FUNCT_1:sch 3;
  set X = [:{0},G':];
  set B = FreeUnivAlgNSG(S,X);
A5: signature B = S by FREEALG:4;
A6: Terminals DTConUA(S,[:{0},G':]) = [:{0},G':] by FREEALG:3;
  rng g c= FreeGenSetNSG(S,[:{0},G':])
  proof
    let b be set;
    assume b in rng g;
    then consider a being set such that
A7: a in dom g & b = g.a by FUNCT_1:def 5;
    reconsider a as Element of A by A4,A7;
    a in G' & 0 in {0} by A4,A7,XBOOLE_0:def 2,TARSKI:def 1;
    then
A8: [0,a] in [:{0},G':] by ZFMISC_1:106;
    then reconsider s = [0,a] as Symbol of DTConUA(S,[:{0},G':]) by A6;
    root-tree s in FreeGenSetNSG(S,[:{0},G':]) by A6,A8;
    hence thesis by A4,A7;
  end;
  then reconsider g as Function of G, the carrier of B
   by A4,FUNCT_2:4,XBOOLE_1:1;
  signature B = S by FREEALG:4;
  then A,B are_similar by UNIALG_2:def 2;
  then consider h being Function of A,B such that
A9: h is_homomorphism A,B & h|G = g by FREEALG:def 6;
  defpred G[Nat] means
  for a1,a2 being set st a1 in G|^$1 & a2 in G|^$1 & h.a1 = h.a2
  holds a1 = a2;
A10: G|^0 = G by Th18;
A11: len S = len the charact of B & len S = len the charact of A
  by A5,UNIALG_1:def 11;
  then
A12: dom S = dom the charact of B & dom S = dom the charact of A
  by FINSEQ_3:31;
A13: now
    let o be Element of dom the charact of A;
    let p be FinSequence of A such that
A14: p in dom Den(o,A);
    reconsider q = p as FinSequence of A;
    reconsider hq = h*q as FinSequence of B;
    reconsider op = Den(o,A) as Element of Operations A;
    reconsider on = o as Element of NAT;
    reconsider o' = on as OperSymbol of B by A11,FINSEQ_3:31;
    reconsider op' = Den(o',B) as Element of Operations B;
    reconsider j = S.o' as Element of NAT;
    dom op = (arity op)-tuples_on the carrier of A by UNIALG_2:2;
    then
A15: len p = arity op by A14,FINSEQ_2:109
      .= j by A12,UNIALG_1:def 11;
    hence len p = S.o & len (h*p) = S.o by FINSEQ_2:37;
A16: h.(op.q) = op'.hq by A14,A9,ALG_1:def 1;
A17: In(o', dom the charact of B) = o' by FUNCT_7:def 1;
    o' in dom S & len hq = S.o' by A12,A15,FINSEQ_2:37;
    hence h.(Den(o,A).p) = o-tree (h*p) by A17,A16,Th17;
  end;
A18: G[0]
  proof
    let a1,a2 be set;
    assume
A19: a1 in G|^0 & a2 in G|^0 & h.a1 = h.a2;
    then h.a1 = g.a1 & h.a2 = g.a2 by A10,A9,FUNCT_1:72;
    then h.a1 = F(a1) & h.a2 = F(a2) by A19,A10,A4;
    then [0,a1] = [0,a2] by A19,TREES_4:4;
    hence a1 = a2 by ZFMISC_1:33;
  end;
A20: now
    let o be Element of dom the charact of A;
    let p be Element of (the carrier of A)*;
    assume p in dom Den(o,A);
    then
A21: h.(Den(o,A).p) = o-tree(h*p) by A13;
    let x be set;
    assume
A22: x in G;
    then
A23: h.x = g.x by A9,FUNCT_1:72
      .= F(x) by A22,A4;
    assume h.(Den(o,A).p) = h.x;
    hence contradiction by A23,A21,TREES_4:17;
  end;
A24: for k being Nat st G[k] holds G[k+1]
  proof
    let k be Nat such that
A25: G[k];
    defpred Gk[set] means ex o being Element of dom the charact of A st
    ex p being Element of (the carrier of A)*
    st $1 = Den(o,A).p & p in dom Den(o,A) & rng p c= G|^k;
    let a1,a2 be set;
    assume
A26: a1 in G|^(k+1) & a2 in G|^(k+1) & h.a1 = h.a2;
    per cases by A26,Th23;
    suppose
A27:  a1 in G & a2 in G;
      then h.a1 = g.a1 & h.a2 = g.a2 by A9,FUNCT_1:72;
      then h.a1 = F(a1) & h.a2 = F(a2) by A27,A4;
      then [0,a1] = [0,a2] by A26,TREES_4:4;
      hence a1 = a2 by ZFMISC_1:33;
    end;
    suppose
A28:  Gk[a1] & Gk[a2];
      then consider b1 being (Element of dom the charact of A),
      q1 being Element of (the carrier of A)* such that
A29:  a1 = Den(b1,A).q1 & q1 in dom Den(b1,A) & rng q1 c= G|^k;
      consider b2 being (Element of dom the charact of A),
      q2 being Element of (the carrier of A)* such that
A30:  a2 = Den(b2,A).q2 & q2 in dom Den(b2,A) & rng q2 c= G|^k by A28;
      b1-tree(h*q1) = h.a1 by A13,A29
        .= b2-tree(h*q2) by A13,A30,A26;
      then
A31:  b1 = b2 & h*q1 = h*q2 by TREES_4:15;
      len q1 = S.b1 & len q2 = S.b2 by A29,A30,A13;
      then
A32:  dom q1 = Seg len q1 & dom q2 = Seg len q1 by A31,FINSEQ_1:def 3;
      now
        let j be Nat;
        assume
A33:    j in dom q1;
        then q1.j in rng q1 & q2.j in rng q2 by A32,FUNCT_1:12;
        then q1.j in G|^k & q2.j in G|^k & h.(q1.j) = (h*q1).j &
        h.(q2.j) = (h*q2).j by A29,A30,A32,A33,FUNCT_1:23;
        hence q1.j = q2.j by A25,A31;
      end;
      hence a1 = a2 by A29,A30,A31,A32,FINSEQ_1:17;
    end;
    suppose a1 in G & Gk[a2] or Gk[a1] & a2 in G;
      hence a1 = a2 by A26,A20;
    end;
  end;
A34: for k being Nat holds G[k] from NAT_1:sch 2(A18,A24);
  reconsider q1 = p1, q2 = p2 as FinSequence of A by A1,FINSEQ_1:def 11;
  o1-tree(h*q1) = h.(Den(o1,A).p1) by A1,A13
    .= o2-tree(h*q2) by A2,A1,A13;
  then
A35: h*p1 = h*p2 by TREES_4:15;
  len q1 = S.o1 & len q2 = S.o2 by A1,A13;
  then
A36: dom q1 = Seg len q1 & dom q2 = Seg len q1 by A3,FINSEQ_1:def 3;
  now
    let j be Nat;
    assume
A37: j in dom q1;
    then
A38: q1.j in rng q1 & q2.j in rng q2 by A36,FUNCT_1:12;
    then consider n1 being Nat such that
A39: q1.j in G|^n1 by Th30;
    consider n2 being Nat such that
A40: q2.j in G|^n2 by A38,Th30;
    reconsider k = max(n1,n2) as Nat;
    G|^n1 c= G|^k & G|^n2 c= G|^k by Th21,XXREAL_0:25;
    then q1.j in G|^k & q2.j in G|^k & h.(q1.j) = (h*q1).j &
    h.(q2.j) = (h*q2).j & G[k] by A34,A39,A40,A36,A37,FUNCT_1:23;
    hence q1.j = q2.j by A35;
  end;
  hence p1 = p2 by A36,FINSEQ_1:17;
end;

theorem
  for A being free Universal_Algebra for o1,o2 being Element of Operations A
  for p1,p2 being FinSequence st p1 in dom o1 & p2 in dom o2
  holds o1.p1 = o2.p2 implies o1 = o2 & p1 = p2
proof
  let A be free Universal_Algebra;
  let o1,o2 be Element of Operations A;
  consider a1 being set such that
A1: a1 in dom the charact of A & o1 = (the charact of A).a1 by FUNCT_1:def 5;
  consider a2 being set such that
A2: a2 in dom the charact of A & o2 = (the charact of A).a2 by FUNCT_1:def 5;
  reconsider a1,a2 as OperSymbol of A by A1,A2;
A3: o1 = Den(a1,A) & o2 = Den(a2,A) by A1,A2;
  let p1,p2 be FinSequence;
  assume p1 in dom o1 & p2 in dom o2 & o1.p1 = o2.p2;
  hence thesis by A3,Th36;
end;

theorem Th38:
  for A being free Universal_Algebra for o being OperSymbol of A
  for p being FinSequence st p in dom Den(o,A) for a being set st a in rng p
  holds a <> Den(o,A).p
proof
  let A be free Universal_Algebra;
  let o be OperSymbol of A;
  let p be FinSequence such that
A1: p in dom Den(o,A);
  let a be set such that
A2: a in rng p & a = Den(o,A).p;
  reconsider p as FinSequence of A by A1,FINSEQ_1:def 11;
  a in rng p by A2;
  then reconsider a as Element of A;
  set G = Generators A;
  consider n being Nat such that
A3: a in G|^n by Th30;
  reconsider n as Element of NAT by ORDINAL1:def 13;
  defpred P[Nat] means ex a being (Element of A), o being OperSymbol of A st
  ex p being FinSequence of A st
  p in dom Den(o,A) & a in rng p & a = Den(o,A).p & a in G|^$1;
  a in rng p & a in G|^n by A2,A3;
  then
A4: ex n being Nat st P[n] by A1,A2;
  consider n being Nat such that
A5: P[n] & for m being Nat st P[m] holds n <= m from NAT_1:sch 5(A4);
  consider a being (Element of A), o being OperSymbol of A,
  p being FinSequence of A such that
A6: p in dom Den(o,A) & a in rng p & a = Den(o,A).p & a in G|^n by A5;
  reconsider op = Den(o,A) as Element of Operations A;
  a in rng op by A6,FUNCT_1:12;
  then a nin G by Th26;
  then n <> 0 by A6,Th18;
  then consider k being Nat such that
A7: n = k+1 by NAT_1:6;
  reconsider k as Element of NAT by ORDINAL1:def 13;
A8: k < n by A7,NAT_1:13;
  then a nin G|^k by A5,A6;
  then consider o' being (Element of dom the charact of A),
  p' being Element of (the carrier of A)* such that
A9: a = Den(o',A).p' & p' in dom Den(o',A) & rng p' c= G|^k by A6,A7,Th20;
  p' = p by A6,A9,Th36;
  hence contradiction by A5,A6,A9,A8;
end;

theorem Th39:
  for A being free Universal_Algebra for G being GeneratorSet of A
  for o being OperSymbol of A
  st for o' being OperSymbol of A, p being FinSequence
  st p in dom Den(o',A) & Den(o',A).p in G holds o' <> o
  for p being FinSequence st p in dom Den(o,A)
  for n being Nat st Den(o,A).p in G|^(n+1) holds rng p c= G|^n
proof
  let A be free Universal_Algebra;
  let G be GeneratorSet of A;
  let o be OperSymbol of A such that
A1: for o' being OperSymbol of A, p being FinSequence
  st p in dom Den(o',A) & Den(o',A).p in G holds o' <> o;
  let p be FinSequence such that
A2: p in dom Den(o,A);
  let n be Nat such that
A3: Den(o,A).p in G|^(n+1) & not rng p c= G|^n;
  reconsider p as FinSequence of A by A2,FINSEQ_1:def 11;
  defpred P[Nat] means ex p being FinSequence of A st
  p in dom Den(o,A) & Den(o,A).p in G|^($1+1) & not rng p c= G|^$1;
  p is FinSequence of A & n is Element of NAT by ORDINAL1:def 13;
  then
A4: ex n being Nat st P[n] by A2,A3;
  consider n being Nat such that
A5: P[n] & for m being Nat st P[m] holds n <= m from NAT_1:sch 5(A4);
  consider p being FinSequence of A such that
A6: p in dom Den(o,A) & Den(o,A).p in G|^(n+1) & not rng p c= G|^n by A5;
  set a = Den(o,A).p;
  now
    assume
A7: a in G|^n;
    a nin G by A1,A6;
    then n <> 0 by A7,Th18;
    then consider k being Nat such that
A8: n = k+1 by NAT_1:6;
    reconsider k as Element of NAT by ORDINAL1:def 13;
A9: k < n by A8,NAT_1:13;
    then G|^k c= G|^n by Th21;
    then not rng p c= G|^k by A6,XBOOLE_1:1;
    hence contradiction by A5,A6,A7,A8,A9;
  end;
  then ex o' being (Element of dom the charact of A),
  p' being Element of (the carrier of A)* st
  a = Den(o',A).p' & p' in dom Den(o',A) & rng p' c= G|^n by A6,Th20;
  hence contradiction by A6,Th36;
end;

theorem
  for A being free Universal_Algebra for o being OperSymbol of A
  for p being FinSequence st p in dom Den(o,A)
  for n being Nat st Den(o,A).p in (Generators A)|^(n+1)
  holds rng p c= (Generators A)|^n
proof
  let A be free Universal_Algebra;
  set G = Generators A;
  let o be OperSymbol of A;
  now
    let o' be OperSymbol of A, p be FinSequence;
    reconsider op = Den(o',A) as Element of Operations A;
    assume p in dom Den(o',A);
    then op.p in rng op by FUNCT_1:12;
    hence Den(o',A).p in G implies o' <> o by Th26;
  end;
  hence thesis by Th39;
end;

begin :: If-while Algebra

definition
  let S be non empty UAStr;
  attr S is with_empty-instruction means
  : Def10:
  1 in dom the charact of S &
  (the charact of S).1 is nullary (non empty homogeneous
  quasi_total PartFunc of (the carrier of S)*, the carrier of S);
  attr S is with_catenation means
  : Def11:
  2 in dom the charact of S &
  (the charact of S).2 is binary (non empty homogeneous
  quasi_total PartFunc of (the carrier of S)*, the carrier of S);
  attr S is with_if-instruction means
  : Def12:
  3 in dom the charact of S &
  (the charact of S).3 is ternary (non empty homogeneous
  quasi_total PartFunc of (the carrier of S)*, the carrier of S);
  attr S is with_while-instruction means
  : Def13:
  4 in dom the charact of S &
  (the charact of S).4 is binary (non empty homogeneous
  quasi_total PartFunc of (the carrier of S)*, the carrier of S);
  attr S is associative means
  :
  Def14: (the charact of S).2 is binary associative (non empty homogeneous
  quasi_total PartFunc of (the carrier of S)*, the carrier of S);
end;

definition
  let S be non-empty UAStr;
  attr S is unital means
  : Def15:
  ex f being binary (non empty homogeneous
  quasi_total PartFunc of (the carrier of S)*, the carrier of S)
  st f = (the charact of S).2 &
  Den(In(1, dom the charact of S), S).({}) is_a_unity_wrt f;
end;

theorem Th41:
  for X being non empty set, x being Element of X
  for c being binary associative unital
  (non empty quasi_total homogeneous PartFunc of X*, X) st x is_a_unity_wrt c
  for i being ternary (non empty quasi_total homogeneous PartFunc of X*, X)
  for w being binary (non empty quasi_total homogeneous PartFunc of X*, X)
  ex S being non-empty strict UAStr st the carrier of S = X &
  the charact of S = <*(0-tuples_on X)-->x,c*>^<*i,w*> &
  S is with_empty-instruction with_catenation unital associative
  with_if-instruction with_while-instruction quasi_total partial
proof
  let X be non empty set;
  let x be Element of X;
  let c be binary associative unital (non empty quasi_total homogeneous
  PartFunc of X*, X);
  assume
A1: x is_a_unity_wrt c;
  let i be ternary (non empty quasi_total homogeneous PartFunc of X*, X);
  let w be binary (non empty quasi_total homogeneous PartFunc of X*, X);
  set Y = 0-tuples_on X;
  set e = Y --> x;
  reconsider e as nullary
  (non empty quasi_total homogeneous PartFunc of X*, X);
  set char = <*e,c*>^<*i,w*>;
  reconsider ec = <*e,c*> as non empty FinSequence;
  char is PFuncFinSequence of X
  proof
    let a be set;
    assume a in rng char;
    then a in rng <*e,c*> \/ rng <*i,w*> by FINSEQ_1:44;
    then a in rng <*e,c*> or a in rng <*i,w*> by XBOOLE_0:def 2;
    then a in {e,c} or a in {i,w} by FINSEQ_2:147;
    then a = e or a = c or a = i or a = w by TARSKI:def 2;
    hence a in PFuncs(X*, X) by PARTFUN1:119;
  end;
  then reconsider char as non empty non-empty PFuncFinSequence of X;
  reconsider S = UAStr(#X, char#) as non-empty strict UAStr by UNIALG_1:def 9;
  take S;
  thus the carrier of S = X;
  thus the charact of S = <*(0-tuples_on X)-->x,c*>^<*i,w*>;
A3: len <*e,c*> = 2 & len <*i,w*> = 2 by FINSEQ_1:61;
  then len char = 2+2 by FINSEQ_1:35;
  then
A4: dom char = Seg 4 by FINSEQ_1:def 3;
  reconsider e as nullary (non empty homogeneous
  PartFunc of (the carrier of S)*, the carrier of S);
  reconsider c as binary associative (non empty homogeneous
  quasi_total PartFunc of (the carrier of S)*, the carrier of S);
A5: <*e,c*>.1 = e & <*e,c*>.2 = c & <*i,w*>.1 = i & <*i,w*>.2 = w
  by FINSEQ_1:61;
  thus 1 in dom the charact of S by A4;
  dom <*e,c*> = Seg 2 by FINSEQ_3:29;
  then
A6: 1 in dom <*e,c*> & 2 in dom <*e,c*>;
  then
A7: e = (the charact of S).1 & c = (the charact of S).2 by A5,FINSEQ_1: def 7;
  thus (the charact of S).1 is nullary (non empty homogeneous
  quasi_total PartFunc of (the carrier of S)*, the carrier of S)
  by A5,A6,FINSEQ_1:def 7;
  thus 2 in dom the charact of S by A4;
  thus (the charact of S).2 is binary (non empty homogeneous
  quasi_total PartFunc of (the carrier of S)*, the carrier of S)
  by A6,A5,FINSEQ_1:def 7;
  thus S is unital
  proof
    take c;
    thus c = (the charact of S).2 by A6,A5,FINSEQ_1:def 7;
    1 in dom the charact of S by A4;
    then Y = {{}} & In(1, dom the charact of S) = 1
    by FUNCT_7:def 1,COMPUT_1:8;
    then {} in Y & e = Den(In(1, dom the charact of S),S)
    by A6,A5,FINSEQ_1:def 7,TARSKI:def 1;
    hence Den(In(1, dom the charact of S),S).({}) is_a_unity_wrt c
    by A1,FUNCOP_1:13;
  end;
  thus (the charact of S).2 is binary associative (non empty homogeneous
  quasi_total PartFunc of (the carrier of S)*, the carrier of S)
  by A6,A5,FINSEQ_1:def 7;
  thus 3 in dom the charact of S by A4;
  dom <*i,w*> = Seg 2 by FINSEQ_3:29;
  then 1 in dom <*i,w*> & 2 in dom <*i,w*>;
  then
A8: char.(2+1) = i & char.(2+2) = w by A3,A5,FINSEQ_1:def 7;
  hence (the charact of S).3 is ternary (non empty homogeneous
  quasi_total PartFunc of (the carrier of S)*, the carrier of S);
  thus 4 in dom the charact of S by A4;
  thus (the charact of S).4 is binary (non empty homogeneous
  quasi_total PartFunc of (the carrier of S)*, the carrier of S) by A8;
  thus S is quasi_total
  proof
    let i be Nat, h be PartFunc of (the carrier of S)*, the carrier of S;
    assume i in dom the charact of S;
    hence thesis by A7,A8,A4,FINSEQ_3:2,ENUMSET1:def 2;
  end;
  let i be Nat, h be PartFunc of (the carrier of S)*, the carrier of S;
  assume
A9: i in dom the charact of S & h = (the charact of S).i;
  let p1,p2 be FinSequence;
  i = 1 or i = 2 or i = 3 or i = 4 by A4,A9,FINSEQ_3:2,ENUMSET1:def 2;
  hence thesis by A7,A8,A9,UNIALG_1:def 1;
end;

registration
  cluster with_empty-instruction with_catenation with_if-instruction
    with_while-instruction unital associative
    (quasi_total partial non-empty strict UAStr);
  existence
  proof
    consider X being non empty set;
    consider c being binary associative unital
    (non empty quasi_total homogeneous PartFunc of X*, X);
    consider a being Element of X;
    consider x being set such that
A1: x is_a_unity_wrt c by Def3;
    arity c = 2 by COMPUT_1:def 26;
    then
A2: dom c = 2-tuples_on X by COMPUT_1:25;
    then <*a,a*> in dom c by CATALG_1:10;
    then <*a,x*> in dom c by A1,Def1;
    then reconsider x as Element of X by A2,CATALG_1:11;
    consider i being ternary
    (non empty quasi_total homogeneous PartFunc of X*, X);
    consider w being binary
    (non empty quasi_total homogeneous PartFunc of X*, X);
    ex S being non-empty strict UAStr st the carrier of S = X &
    the charact of S = <*(0-tuples_on X)-->x,c*>^<*i,w*> &
    S is with_empty-instruction with_catenation unital associative
    with_if-instruction with_while-instruction quasi_total partial by A1,Th41;
    hence thesis;
  end;
end;

definition
  mode preIfWhileAlgebra is with_empty-instruction
    with_catenation with_if-instruction with_while-instruction
    Universal_Algebra;
end;

reserve A for preIfWhileAlgebra,
  C,I,J for Element of A;

reserve S for non empty set,
  T for Subset of S,
  s for Element of S;

definition
  let A be non empty UAStr;
  mode Algorithm of A is Element of A;
end;

theorem Th42:
  for A being with_empty-instruction (non-empty UAStr)
  holds dom Den(In(1, dom the charact of A), A) = {{}}
proof
  let A be with_empty-instruction (non-empty UAStr);
  reconsider e = (the charact of A).1 as nullary (non empty homogeneous
  quasi_total PartFunc of (the carrier of A)*, the carrier of A) by Def10;
  consider a being Element of A;
  1 in dom the charact of A by Def10;
  then
A1: Den(In(1, dom the charact of A), A) = e by FUNCT_7:def 1;
  arity e = 0 by COMPUT_1:def 24;
  then dom e = 0-tuples_on the carrier of A by COMPUT_1:25;
  hence dom Den(In(1, dom the charact of A), A) = {{}} by A1,COMPUT_1:8;
end;

definition
  let A be with_empty-instruction (non-empty UAStr);
  func EmptyIns A -> Algorithm of A equals
  Den(In(1, dom the charact of A), A).{};
  coherence
  proof
    reconsider e = (the charact of A).1 as nullary (non empty homogeneous
    quasi_total PartFunc of (the carrier of A)*, the carrier of A) by Def10;
    consider a being Element of A;
    1 in dom the charact of A by Def10;
    then
A1: Den(In(1, dom the charact of A), A) = e by FUNCT_7:def 1;
    then dom e = {{}} by Th42;
    then {} in dom e by TARSKI:def 1;
    hence thesis by A1,PARTFUN1:27;
  end;
end;

theorem
  for A being with_empty-instruction Universal_Algebra
  for o being Element of Operations A
  st o = Den(In(1, dom the charact of A), A)
  holds arity o = 0 & EmptyIns A in rng o
proof
  let A be with_empty-instruction Universal_Algebra;
  let o be Element of Operations A such that
A1: o = Den(In(1, dom the charact of A), A);
A2: dom Den(In(1, dom the charact of A), A) = {{}} by Th42;
A3: <*>the carrier of A in {{}} by TARSKI:def 1;
  hence arity o = len (<*>the carrier of A) by A1,A2,UNIALG_1:def 10
    .= 0;
  thus thesis by A1,A2,A3,FUNCT_1:def 5;
end;

theorem Th44:
  for A being with_catenation (non-empty UAStr)
  holds dom Den(In(2, dom the charact of A), A) = 2-tuples_on the carrier of A
proof
  let A be with_catenation (non-empty UAStr);
  reconsider f = (the charact of A).2 as binary (non empty homogeneous
  quasi_total PartFunc of (the carrier of A)*, the carrier of A) by Def11;
  2 in dom the charact of A by Def11;
  then
A1: Den(In(2, dom the charact of A), A) = f by FUNCT_7:def 1;
  arity f = 2 by COMPUT_1:def 26;
  hence thesis by A1,COMPUT_1:25;
end;

definition
  let A be with_catenation (non-empty UAStr);
  let I1,I2 be Algorithm of A;
  func I1 \; I2 -> Algorithm of A equals
  Den(In(2, dom the charact of A), A).<*I1,I2*>;
  coherence
  proof
    reconsider f = (the charact of A).2 as binary (non empty homogeneous
    quasi_total PartFunc of (the carrier of A)*, the carrier of A) by Def11;
    2 in dom the charact of A by Def11;
    then
A1: Den(In(2, dom the charact of A), A) = f by FUNCT_7:def 1;
    then dom f = 2-tuples_on the carrier of A by Th44;
    then <*I1,I2*> in dom f by CATALG_1:10;
    hence thesis by A1,PARTFUN1:27;
  end;
end;

theorem
  for A being with_empty-instruction with_catenation unital (non-empty UAStr)
  for I being Element of A holds EmptyIns A\;I = I & I\;EmptyIns A = I
proof
  let A be with_empty-instruction with_catenation unital (non-empty UAStr);
  let I be Element of A;
  consider f being binary (non empty homogeneous
  quasi_total PartFunc of (the carrier of A)*, the carrier of A) such that
A1: f = (the charact of A).2 and
A2: Den(In(1, dom the charact of A), A).({}) is_a_unity_wrt f by Def15;
  2 in dom the charact of A & arity f = 2 by Def11,COMPUT_1:def 26;
  then dom f = 2-tuples_on the carrier of A & In(2, dom the charact of A) = 2
  by COMPUT_1:25,FUNCT_7:def 1;
  then EmptyIns A\;I = f.(<*EmptyIns A, I*>) & <*I,I*> in dom f &
  I\;EmptyIns A = f.(<*I, EmptyIns A*>) by A1,CATALG_1:10;
  hence thesis by A2,Def1;
end;

theorem
  for A being associative with_catenation (non-empty UAStr)
  for I1,I2,I3 being Element of A holds (I1\;I2)\;I3 = I1\;(I2\;I3)
proof
  let A be associative with_catenation (non-empty UAStr);
  let I1,I2,I3 be Element of A;
  reconsider f = (the charact of A).2 as
  binary associative (non empty homogeneous
  quasi_total PartFunc of (the carrier of A)*, the carrier of A) by Def14;
  2 in dom the charact of A & arity f = 2 by Def11,COMPUT_1:def 26;
  then dom f = 2-tuples_on the carrier of A & In(2, dom the charact of A) = 2
  by COMPUT_1:25,FUNCT_7:def 1;
  then I1\;I2 = f.(<*I1,I2*>) & I2\;I3 = f.(<*I2,I3*>) &
  (I1\;I2)\;I3 = f.(<*I1\;I2,I3*>) & I1\;(I2\;I3) = f.(<*I1,I2\;I3*>) &
  <*I1,I2*> in dom f & <*I2,I3*> in dom f & <*I1,I2\;I3*> in dom f &
  <*I1\;I2,I3*> in dom f by CATALG_1:10;
  hence (I1\;I2)\;I3 = I1\;(I2\;I3) by Def2;
end;

theorem Th47:
  for A being with_if-instruction (non-empty UAStr)
  holds dom Den(In(3, dom the charact of A), A) = 3-tuples_on the carrier of A
proof
  let A be with_if-instruction (non-empty UAStr);
  reconsider f = (the charact of A).3 as ternary (non empty homogeneous
  quasi_total PartFunc of (the carrier of A)*, the carrier of A) by Def12;
  3 in dom the charact of A & 3 in Seg 3 by Def12;
  then
A1: Den(In(3, dom the charact of A), A) = f by FUNCT_7:def 1;
  arity f = 3 by COMPUT_1:def 27;
  hence thesis by A1,COMPUT_1:25;
end;

definition
  let A be with_if-instruction (non-empty UAStr);
  let C,I1,I2 be Algorithm of A;
  func if-then-else(C,I1,I2) -> Algorithm of A equals
  Den(In(3, dom the charact of A), A).<*C,I1,I2*>;
  coherence
  proof
    reconsider f = (the charact of A).3 as ternary (non empty homogeneous
    quasi_total PartFunc of (the carrier of A)*, the carrier of A) by Def12;
    3 in dom the charact of A & 3 in Seg 3 by Def12;
    then
A1: Den(In(3, dom the charact of A), A) = f by FUNCT_7:def 1;
    arity f = 3 by COMPUT_1:def 27;
    then dom f = 3-tuples_on the carrier of A by COMPUT_1:25;
    then <*C,I1,I2*> in dom f by CATALG_1:12;
    hence thesis by A1,PARTFUN1:27;
  end;
end;

definition
  let A be with_empty-instruction with_if-instruction (non-empty UAStr);
  let C,I be Algorithm of A;
  func if-then(C,I) -> Algorithm of A equals

  if-then-else(C,I,EmptyIns A);
  coherence;
end;

theorem Th48:
  for A being with_while-instruction (non-empty UAStr)
  holds dom Den(In(4, dom the charact of A), A) = 2-tuples_on the carrier of A
proof
  let A be with_while-instruction (non-empty UAStr);
  reconsider f = (the charact of A).4 as binary (non empty homogeneous
  quasi_total PartFunc of (the carrier of A)*, the carrier of A) by Def13;
  4 in dom the charact of A by Def13;
  then
A1: Den(In(4, dom the charact of A), A) = f by FUNCT_7:def 1;
  arity f = 2 by COMPUT_1:def 26;
  hence thesis by A1,COMPUT_1:25;
end;

definition
  let A be with_while-instruction (non-empty UAStr);
  let C,I be Algorithm of A;
  func while(C,I) -> Algorithm of A equals
  Den(In(4, dom the charact of A), A).<*C,I*>;
  coherence
  proof
    reconsider f = (the charact of A).4 as binary (non empty homogeneous
    quasi_total PartFunc of (the carrier of A)*, the carrier of A) by Def13;
    4 in dom the charact of A by Def13;
    then
A1: Den(In(4, dom the charact of A), A) = f by FUNCT_7:def 1;
    arity f = 2 by COMPUT_1:def 26;
    then dom f = 2-tuples_on the carrier of A by COMPUT_1:25;
    then <*C,I*> in dom f by CATALG_1:10;
    hence thesis by A1,PARTFUN1:27;
  end;
end;

definition
  let A be preIfWhileAlgebra;
  let I0,C,I,J be Element of A;
  func for-do(I0,C,J,I) -> Element of A equals

  I0\;while(C,I\;J);
  coherence;
end;

definition
  let A be preIfWhileAlgebra;
  func ElementaryInstructions A -> Subset of A equals

  (the carrier of A)
  \ {EmptyIns A} \ rng Den(In(3, dom the charact of A), A)
  \ rng Den(In(4, dom the charact of A), A)
  \ {I1 \; I2 where I1,I2 is Algorithm of A: I1 <> I1\;I2 & I2 <> I1\;I2};
  coherence;
end;

theorem Th49:
  for A being preIfWhileAlgebra holds EmptyIns A nin ElementaryInstructions A
proof
  let A be preIfWhileAlgebra;
  set I = EmptyIns A;
  I in {I} by TARSKI:def 1;
  then I nin (the carrier of A)\{I} by XBOOLE_0:def 4;
  then I nin (the carrier of A) \ {EmptyIns A}
  \ rng Den(In(3, dom the charact of A), A) by XBOOLE_0:def 4;
  then I nin (the carrier of A) \ {EmptyIns A}
  \ rng Den(In(3, dom the charact of A), A)
  \ rng Den(In(4, dom the charact of A), A) by XBOOLE_0:def 4;
  hence I nin ElementaryInstructions A by XBOOLE_0:def 4;
end;

theorem Th50:
  for A being preIfWhileAlgebra
  for I1,I2 being Element of A st I1 <> I1\;I2 & I2 <> I1\;I2
  holds I1\;I2 nin ElementaryInstructions A
proof
  let A be preIfWhileAlgebra;
  let I1,I2 be Element of A;
  assume I1 <> I1\;I2 & I2 <> I1\;I2;
  then I1\;I2 in {J1 \; J2 where J1,J2 is Algorithm of A:
  J1 <> J1\;J2 & J2 <> J1\;J2};
  hence I1\;I2 nin ElementaryInstructions A by XBOOLE_0:def 4;
end;

theorem Th51:
  for A being preIfWhileAlgebra for C,I1,I2 being Element of A
  holds if-then-else(C,I1,I2) nin ElementaryInstructions A
proof
  let A be preIfWhileAlgebra;
  let C,I1,I2 be Element of A;
  set I = if-then-else(C,I1,I2);
  reconsider f = (the charact of A).3 as ternary (non empty homogeneous
  quasi_total PartFunc of (the carrier of A)*, the carrier of A) by Def12;
  3 in dom the charact of A by Def12;
  then In(3, dom the charact of A) = 3 by FUNCT_7:def 1;
  then dom Den(In(3, dom the charact of A), A)
  = (arity f)-tuples_on the carrier of A by COMPUT_1:25
    .= 3-tuples_on the carrier of A by COMPUT_1:def 27;
  then <*C,I1,I2*> in dom Den(In(3, dom the charact of A), A) by CATALG_1:12;
  then I in rng Den(In(3, dom the charact of A), A) by FUNCT_1:def 5;
  then I nin (the carrier of A) \ {EmptyIns A}
  \ rng Den(In(3, dom the charact of A), A) by XBOOLE_0:def 4;
  then I nin (the carrier of A) \ {EmptyIns A}
  \ rng Den(In(3, dom the charact of A), A)
  \ rng Den(In(4, dom the charact of A), A) by XBOOLE_0:def 4;
  hence if-then-else(C,I1,I2) nin ElementaryInstructions A by XBOOLE_0:def 4;
end;

theorem Th52:
  for A being preIfWhileAlgebra for C,I being Element of A
  holds while(C,I) nin ElementaryInstructions A
proof
  let A be preIfWhileAlgebra;
  let C,I1 be Element of A;
  set I = while(C,I1);
  reconsider f = (the charact of A).4 as binary (non empty homogeneous
  quasi_total PartFunc of (the carrier of A)*, the carrier of A) by Def13;
  4 in dom the charact of A by Def13;
  then In(4, dom the charact of A) = 4 by FUNCT_7:def 1;
  then dom Den(In(4, dom the charact of A), A)
  = (arity f)-tuples_on the carrier of A by COMPUT_1:25
    .= 2-tuples_on the carrier of A by COMPUT_1:def 26;
  then <*C,I1*> in dom Den(In(4, dom the charact of A), A) by CATALG_1:10;
  then I in rng Den(In(4, dom the charact of A), A) by FUNCT_1:def 5;
  then I nin (the carrier of A) \ {EmptyIns A}
  \ rng Den(In(3, dom the charact of A), A)
  \ rng Den(In(4, dom the charact of A), A) by XBOOLE_0:def 4;
  hence I nin ElementaryInstructions A by XBOOLE_0:def 4;
end;

theorem Th53:
  for A being preIfWhileAlgebra for I being Element of A
  st I nin ElementaryInstructions A holds I = EmptyIns A or
  (ex I1,I2 being Element of A st I = I1\;I2 & I1 <> I1\;I2 & I2 <> I1\;I2) or
  (ex C,I1,I2 being Element of A st I = if-then-else(C,I1,I2)) or
  (ex C,J being Element of A st I = while(C,J))
proof
  let A be preIfWhileAlgebra;
  let I be Element of A such that
A1: I nin ElementaryInstructions A and
A2: I <> EmptyIns A and
A3: for I1,I2 being Element of A st I = I1\;I2 & I1 <> I1\;I2 holds
  I2 = I1\;I2 and
A4: for C,I1,I2 being Element of A holds I <> if-then-else(C,I1,I2) and
A5: for C,J being Element of A holds I <> while(C,J);
A6: now
    assume I in rng Den(In(3, dom the charact of A), A);
    then consider x being set such that
A7: x in dom Den(In(3, dom the charact of A), A) &
    I = Den(In(3, dom the charact of A), A).x by FUNCT_1:def 5;
    reconsider f = (the charact of A).3 as ternary (non empty homogeneous
    quasi_total PartFunc of (the carrier of A)*, the carrier of A) by Def12;
    3 in dom the charact of A by Def12;
    then In(3, dom the charact of A) = 3 by FUNCT_7:def 1;
    then dom Den(In(3, dom the charact of A), A)
    = (arity f)-tuples_on the carrier of A by COMPUT_1:25
      .= 3-tuples_on the carrier of A by COMPUT_1:def 27;
    then consider C,I1,I2 be set such that
A8: C in the carrier of A & I1 in the carrier of A & I2 in the carrier of A &
    x = <*C,I1,I2*> by A7,CATALG_1:12;
    reconsider C,I1,I2 as Element of A by A8;
    I = if-then-else(C,I1,I2) by A7,A8;
    hence contradiction by A4;
  end;
A9: now
    assume I in rng Den(In(4, dom the charact of A), A);
    then consider x being set such that
A10: x in dom Den(In(4, dom the charact of A), A) &
    I = Den(In(4, dom the charact of A), A).x by FUNCT_1:def 5;
    reconsider f = (the charact of A).4 as binary (non empty homogeneous
    quasi_total PartFunc of (the carrier of A)*, the carrier of A) by Def13;
    4 in dom the charact of A by Def13;
    then In(4, dom the charact of A) = 4 by FUNCT_7:def 1;
    then dom Den(In(4, dom the charact of A), A)
    = (arity f)-tuples_on the carrier of A by COMPUT_1:25
      .= 2-tuples_on the carrier of A by COMPUT_1:def 26;
    then consider C,J be set such that
A11: C in the carrier of A & J in the carrier of A &
    x = <*C,J*> by A10,CATALG_1:10;
    reconsider C,J as Element of A by A11;
    I = while(C,J) by A10,A11;
    hence contradiction by A5;
  end;
A12: I nin {I1\;I2 where I1,I2 is Algorithm of A: I1 <> I1\;I2 & I2 <> I1\;I2}
  by A3;
  I in (the carrier of A) \ {EmptyIns A} by A2,ZFMISC_1:64;
  then I in (the carrier of A) \ {EmptyIns A}
  \ rng Den(In(3, dom the charact of A), A) by A6,XBOOLE_0:def 4;
  then I in (the carrier of A) \ {EmptyIns A}
  \ rng Den(In(3, dom the charact of A), A)
  \ rng Den(In(4, dom the charact of A), A) by A9,XBOOLE_0:def 4;
  hence contradiction by A1,A12,XBOOLE_0:def 4;
end;

definition
  let A be preIfWhileAlgebra;
  attr A is infinite means
  : Def23:
  ElementaryInstructions A is infinite;
  attr A is degenerated means
  : Def24:
  (ex I1,I2 being Element of A st
  I1 <> EmptyIns A & I1\;I2 = I2 or I2 <> EmptyIns A & I1\;I2 = I1 or
  (I1 <> EmptyIns A or I2 <> EmptyIns A) & I1\;I2 = EmptyIns A) or
  (ex C,I1,I2 being Element of A st if-then-else(C,I1,I2) = EmptyIns A) or
  (ex C,I being Element of A st while(C,I) = EmptyIns A) or
  (ex I1,I2,C,J1,J2 being Element of A st I1 <> EmptyIns A & I2 <> EmptyIns A &
  I1\;I2 = if-then-else(C,J1,J2)) or
  (ex I1,I2,C,J being Element of A st I1 <> EmptyIns A & I2 <> EmptyIns A &
  I1\;I2 = while(C,J)) or (ex C1,I1,I2,C2,J being Element of A st
  if-then-else(C1,I1,I2) = while(C2,J));
  attr A is well_founded means
  :
  Def25: ElementaryInstructions A is GeneratorSet of A;
end;

definition
  func ECIW-signature -> non empty FinSequence of NAT equals
  <*0, 2*>^<*3, 2*>;
  coherence;
end;

theorem Th54:
  len ECIW-signature = 4 & dom ECIW-signature = Seg 4 &
  ECIW-signature.1 = 0 & ECIW-signature.2 = 2 &
  ECIW-signature.3 = 3 & ECIW-signature.4 = 2
proof
  set S = ECIW-signature;
A1: len <*0,2*> = 2 & len <*3,2*> = 2 by FINSEQ_1:61;
  then
A2: len S = 2+2 & dom <*0,2*> = Seg 2 & dom <*3,2*> = Seg 2
  by FINSEQ_1:def 3,35;
  then
A3: 1 in dom <*3,2*> & <*3,2*>.1 = 3 & 2 in dom <*3,2*> & <*3,2*>.2 = 2 &
  2+1 = 3 & 2+2 = 4 by FINSEQ_1:61;
  1 in dom <*0,2*> & <*0,2*>.1 = 0 & 2 in dom <*0,2*> & <*0,2*>.2 = 2
  by A2,FINSEQ_1:61;
  hence thesis by A1,FINSEQ_1:35,A3,FINSEQ_1:def 7;
end;

definition
  let A be partial non-empty non empty UAStr;
  attr A is ECIW-strict means
  : Def27:
  signature A = ECIW-signature;
end;

theorem Th55:
  for A being partial non-empty non empty UAStr st A is ECIW-strict
  for o being OperSymbol of A holds o = 1 or o = 2 or o = 3 or o = 4
proof
  let A be partial non-empty non empty UAStr;
  assume signature A = ECIW-signature;
  then 4 = len the charact of A by Th54,UNIALG_1:def 11;
  then dom the charact of A = Seg 4 by FINSEQ_1:def 3;
  hence thesis by ENUMSET1:def 2,FINSEQ_3:2;
end;

registration
  let X be disjoint_with_NAT non empty set;
  cluster FreeUnivAlgNSG(ECIW-signature,X) -> with_empty-instruction
    with_catenation with_if-instruction with_while-instruction;
  coherence
  proof
    set S = FreeUnivAlgNSG(ECIW-signature,X);
    set char = ECIW-signature;
A1: len <*0,2*> = 2 & len <*3,2*> = 2 by FINSEQ_1:61;
    then
A2: len char = 2+2 & len the charact of S = len char & dom <*0,2*> = Seg 2 &
    dom <*3,2*> = Seg 2 by FINSEQ_1:def 3,35,FREEALG:def 12;
    then
A3: dom the charact of S = Seg 4 & dom char = Seg 4 by FINSEQ_1:def 3;
    hence 1 in dom the charact of S;
    then
A4: (the charact of S).1 = FreeOpNSG(1,char,X) by FREEALG:def 12;
A5: 1 in dom char & 2 in dom char & 3 in dom char & 4 in dom char by A3;
    reconsider D = TS(DTConUA(char,X)) as non empty set;
    reconsider char as non empty FinSequence of omega;
    set o = FreeOpNSG(1,char,X);
A6: 1 in dom <*0,2*> & <*0,2*>.1 = 0 & 2 in dom <*0,2*> & <*0,2*>.2 = 2
    by A2,FINSEQ_1:61;
    then char.1 = 0 by FINSEQ_1:def 7;
    then char/.1 = 0 & the carrier of S = D by A5,PARTFUN1:def 8;
    then
A7: dom o = 0-tuples_on the carrier of S by A5,FREEALG:def 11;
    reconsider o as homogeneous non empty quasi_total PartFunc of D*, D;
    arity o = 0 by A7,COMPUT_1:28;
    hence (the charact of S).1 is nullary (non empty homogeneous
    quasi_total PartFunc of (the carrier of S)*, the carrier of S)
    by A4,COMPUT_1:def 24;
    thus 2 in dom the charact of S by A3;
    then
A8: (the charact of S).2 = FreeOpNSG(2,char,X) by FREEALG:def 12;
    set o = FreeOpNSG(2,char,X);
    char.2 = 2 by A6,FINSEQ_1:def 7;
    then (char qua FinSequence of omega)/.2 = 2 by A5,PARTFUN1:def 8;
    then
A9: dom o = 2-tuples_on the carrier of S by A5,FREEALG:def 11;
    reconsider o as homogeneous non empty quasi_total PartFunc of D*, D;
    arity o = 2 by A9,COMPUT_1:28;
    hence (the charact of S).2 is binary (non empty homogeneous
    quasi_total PartFunc of (the carrier of S)*, the carrier of S)
    by A8,COMPUT_1:def 26;
    thus 3 in dom the charact of S by A3;
    then
A10: (the charact of S).3 = FreeOpNSG(3,char,X) by FREEALG:def 12;
    set o = FreeOpNSG(3,char,X);
A11: 1 in dom <*3,2*> & <*3,2*>.1 = 3 & 2 in dom <*3,2*> & <*3,2*>.2 = 2
    by A2,FINSEQ_1:61;
    then char.(2+1) = 3 by A1,FINSEQ_1:def 7;
    then (char qua FinSequence of omega)/.3 = 3 by A5,PARTFUN1:def 8;
    then
A12: dom o = 3-tuples_on the carrier of S by A5,FREEALG:def 11;
    reconsider o as homogeneous non empty quasi_total PartFunc of D*, D;
    arity o = 3 by A12,COMPUT_1:28;
    hence (the charact of S).3 is ternary (non empty homogeneous
    quasi_total PartFunc of (the carrier of S)*, the carrier of S)
    by A10,COMPUT_1:def 27;
    thus 4 in dom the charact of S by A3;
    then
A13: (the charact of S).4 = FreeOpNSG(4,char,X) by FREEALG:def 12;
    set o = FreeOpNSG(4,char,X);
    char.(2+2) = 2 by A1,A11,FINSEQ_1:def 7;
    then (char qua FinSequence of omega)/.4 = 2 by A5,PARTFUN1:def 8;
    then
A14: dom o = 2-tuples_on the carrier of S by A5,FREEALG:def 11;
    reconsider o as homogeneous non empty quasi_total PartFunc of D*, D;
    arity o = 2 by A14,COMPUT_1:28;
    hence (the charact of S).4 is binary (non empty homogeneous
    quasi_total PartFunc of (the carrier of S)*, the carrier of S)
    by A13,COMPUT_1:def 26;
  end;
end;

theorem Th56:
  for X being disjoint_with_NAT non empty set
  for I being Element of FreeUnivAlgNSG(ECIW-signature,X) holds
  (ex x being Element of X st I = root-tree x) or
  (ex n being Nat, p being FinSequence of FreeUnivAlgNSG(ECIW-signature,X)
  st n in Seg 4 & I = n-tree p & len p = ECIW-signature.n)
proof
  let X be disjoint_with_NAT non empty set;
  set S = ECIW-signature;
  set G = DTConUA(S,X);
  let I be Element of FreeUnivAlgNSG(S,X) such that
A1: not ex x being Element of X st I = root-tree x;
  Terminals DTConUA(S,X) = X by FREEALG:3;
  then not ex d being Symbol of G st d in Terminals G & I = root-tree d by A1;
  then consider o being Symbol of G, p being FinSequence of TS G such that
A2: o ==> roots p & I = o-tree p by Th16;
A3: NonTerminals G = {s where s is Symbol of G:
  ex n being FinSequence st s ==> n} by LANG1:def 3;
  then
A4: o in NonTerminals G by A2;
A5: NonTerminals G = Seg 4 by Th54,FREEALG:2;
  then reconsider n = o as Element of NAT by A4;
  reconsider p as FinSequence of FreeUnivAlgNSG(ECIW-signature,X);
  take n, p;
  thus n in Seg 4 by A2,A3,A5;
  thus I = n-tree p by A2;
A6: [n, roots p] in the Rules of G by A2,LANG1:def 1;
  then
A7: roots p in (the carrier of G)* by ZFMISC_1:106;
  dom p = dom roots p by TREES_3:def 18;
  hence len p = Card dom roots p by PRE_CIRC:21
    .= len roots p by PRE_CIRC:21
    .= S.n by A6,A7,FREEALG:def 8;
end;

theorem Th57:
  for X being disjoint_with_NAT non empty set
  holds EmptyIns FreeUnivAlgNSG(ECIW-signature,X) = 1-tree {}
proof
  let X be disjoint_with_NAT non empty set;
  set S = ECIW-signature;
  reconsider s = S as non empty FinSequence of omega;
  set A = FreeUnivAlgNSG(S,X);
A1: 1 in dom the charact of A by Def10;
  reconsider f = (the charact of A).1 as nullary (non empty homogeneous
  quasi_total PartFunc of (the carrier of A)*, the carrier of A) by Def10;
A2: f = FreeOpNSG(1,S,X) by A1,FREEALG:def 12;
A3: 1 in dom S by Th54;
  then
A4: s/.1 = S.1 by PARTFUN1:def 8;
A5: dom FreeOpNSG(1,S,X) = (s/.1)-tuples_on TS(DTConUA(S,X))
  by A3,FREEALG:def 11
    .= {{}} by A4,Th54,COMPUT_1:8;
A6: {} in {{}} & {} = <*> TS(DTConUA(S,X)) by TARSKI:def 1;
  thus EmptyIns A = f.{} by A1,FUNCT_7:def 1
    .= Sym(1,S,X)-tree({}) by A2,A5,A6,A3,FREEALG:def 11
    .= 1-tree {} by A3,FREEALG:def 10;
end;

theorem Th58:
  for X being disjoint_with_NAT non empty set
  for p being FinSequence of FreeUnivAlgNSG(ECIW-signature,X)
  st 1-tree p is Element of FreeUnivAlgNSG(ECIW-signature,X) holds p = {}
proof
  let X be disjoint_with_NAT non empty set;
  set S = ECIW-signature;
  set G = DTConUA(S,X);
  set A = FreeUnivAlgNSG(S,X);
  let p be FinSequence of A;
  assume 1-tree p is Element of A;
  then reconsider I = 1-tree p as Element of A;
  per cases by Th56;
  suppose ex x being Element of X st I = root-tree x;
    then consider x being Element of X such that
A1: 1-tree p = root-tree x;
    1-tree p = x-tree(<*>TS G) by A1,TREES_4:20;
    hence thesis by TREES_4:15;
  end;
  suppose ex n being Nat, p being FinSequence of A
    st n in Seg 4 & I = n-tree p & len p = S.n;
    then consider n being Nat, q being FinSequence of A such that
A2: n in Seg 4 & I = n-tree q & len q = S.n;
    n = 1 & q = p by A2,TREES_4:15;
    hence p = {} by A2,Th54;
  end;
end;

theorem Th59:
  for X being disjoint_with_NAT non empty set
  for I1,I2 being Element of FreeUnivAlgNSG(ECIW-signature,X)
  holds I1\;I2 = 2-tree(I1,I2)
proof
  let X be disjoint_with_NAT non empty set;
  set S = ECIW-signature;
  reconsider s = S as non empty FinSequence of omega;
  set A = FreeUnivAlgNSG(S,X);
  let I1,I2 be Element of A;
A1: 2 in dom the charact of A by Def11;
  reconsider f = (the charact of A).2 as binary (non empty homogeneous
  quasi_total PartFunc of (the carrier of A)*, the carrier of A) by Def11;
A2: f = FreeOpNSG(2,S,X) by A1,FREEALG:def 12;
A3: 2 in dom S by Th54;
  then s/.2 = S.2 by PARTFUN1:def 8;
  then
A4: dom FreeOpNSG(2,S,X) = 2-tuples_on TS(DTConUA(S,X))
  by A3,Th54,FREEALG:def 11;
A5: <*I1,I2*> in 2-tuples_on TS(DTConUA(S,X)) by CATALG_1:10;
  thus I1\;I2 = f.<*I1,I2*> by A1,FUNCT_7:def 1
    .= Sym(2,S,X)-tree(<*I1,I2*>) by A2,A4,A5,A3,FREEALG:def 11
    .= 2-tree (I1,I2) by A3,FREEALG:def 10;
end;

theorem Th60:
  for X being disjoint_with_NAT non empty set
  for p being FinSequence of FreeUnivAlgNSG(ECIW-signature,X)
  st 2-tree p is Element of FreeUnivAlgNSG(ECIW-signature,X)
  ex I1,I2 being Element of FreeUnivAlgNSG(ECIW-signature,X) st p = <*I1,I2*>
proof
  let X be disjoint_with_NAT non empty set;
  set S = ECIW-signature;
  set G = DTConUA(S,X);
  set A = FreeUnivAlgNSG(S,X);
  let p be FinSequence of A;
  assume 2-tree p is Element of A;
  then reconsider I = 2-tree p as Element of A;
  per cases by Th56;
  suppose ex x being Element of X st I = root-tree x;
    then consider x being Element of X such that
A1: 2-tree p = root-tree x;
    2-tree p = x-tree(<*>TS G) by A1,TREES_4:20;
    then 2 = x by TREES_4:15;
    then X meets NAT by XBOOLE_0:3;
    hence thesis by FREEALG:def 1;
  end;
  suppose ex n being Nat, p being FinSequence of A
    st n in Seg 4 & I = n-tree p & len p = S.n;
    then consider n being Nat, q being FinSequence of A such that
A2: n in Seg 4 & I = n-tree q & len q = S.n;
A3: n = 2 & q = p by A2,TREES_4:15;
    then p = <*p.1,p.2*> by A2,Th54,FINSEQ_1:61;
    then rng p = {p.1,p.2} by FINSEQ_2:147;
    then reconsider I1 = p.1, I2 = p.2 as Element of A by ZFMISC_1:38;
    take I1,I2; thus thesis by A3,A2,Th54,FINSEQ_1:61;
  end;
end;

theorem Th61:
  for X being disjoint_with_NAT non empty set
  for I1,I2 being Element of FreeUnivAlgNSG(ECIW-signature,X)
  holds I1\;I2 <> I1 & I1\;I2 <> I2
proof
  let X be disjoint_with_NAT non empty set;
  set S = ECIW-signature;
  set G = DTConUA(S,X);
  set A = FreeUnivAlgNSG(S,X);
  let I1,I2 be Element of A;
  set p = <*I1,I2*>;
  rng p c= FinTrees the carrier of G by XBOOLE_1:1;
  then
A1: p is FinSequence of FinTrees the carrier of G by FINSEQ_1:def 4;
  rng p = {I1,I2} by FINSEQ_2:147;
  then
A2: I1 in rng p & I2 in rng p by TARSKI:def 2;
  I1\;I2 = 2-tree(I1,I2) by Th59
    .= 2-tree<*I1,I2*>;
  hence thesis by A1,A2,Th3;
end;

theorem
  for X being disjoint_with_NAT non empty set
  for I1,I2,J1,J2 being Element of FreeUnivAlgNSG(ECIW-signature,X)
  holds I1\;I2 = J1\;J2 implies I1 = J1 & I2 = J2
proof
  let X be disjoint_with_NAT non empty set;
  set S = ECIW-signature;
  set A = FreeUnivAlgNSG(S,X);
  let I1,I2,J1,J2 be Element of A;
  I1\;I2 = 2-tree(I1,I2) & J1\;J2 = 2-tree(J1,J2) by Th59;
  then I1\;I2 = J1\;J2 implies <*I1,I2*> = <*J1,J2*> by TREES_4:15;
  hence thesis by GROUP_7:2;
end;

theorem Th63:
  for X being disjoint_with_NAT non empty set
  for C,I1,I2 being Element of FreeUnivAlgNSG(ECIW-signature,X)
  holds if-then-else(C,I1,I2) = 3-tree<*C,I1,I2*>
proof
  let X be disjoint_with_NAT non empty set;
  set S = ECIW-signature;
  reconsider s = S as non empty FinSequence of omega;
  set A = FreeUnivAlgNSG(S,X);
  let C,I1,I2 be Element of A;
A1: 3 in dom the charact of A by Def12;
  reconsider f = (the charact of A).3 as ternary (non empty homogeneous
  quasi_total PartFunc of (the carrier of A)*, the carrier of A) by Def12;
A2: f = FreeOpNSG(3,S,X) by A1,FREEALG:def 12;
A3: 3 in dom S by Th54;
  then s/.3 = S.3 by PARTFUN1:def 8;
  then
A4: dom FreeOpNSG(3,S,X) = 3-tuples_on TS(DTConUA(S,X))
  by A3,Th54,FREEALG:def 11;
A5: <*C,I1,I2*> in 3-tuples_on TS(DTConUA(S,X)) by CATALG_1:12;
  thus if-then-else(C,I1,I2) = f.<*C,I1,I2*> by A1,FUNCT_7:def 1
    .= Sym(3,S,X)-tree(<*C,I1,I2*>) by A2,A4,A5,A3,FREEALG:def 11
    .= 3-tree <*C,I1,I2*> by A3,FREEALG:def 10;
end;

theorem Th64:
  for X being disjoint_with_NAT non empty set
  for p being FinSequence of FreeUnivAlgNSG(ECIW-signature,X)
  st 3-tree p is Element of FreeUnivAlgNSG(ECIW-signature,X)
  ex C,I1,I2 being Element of FreeUnivAlgNSG(ECIW-signature,X)
  st p = <*C,I1,I2*>
proof
  let X be disjoint_with_NAT non empty set;
  set S = ECIW-signature;
  set G = DTConUA(S,X);
  set A = FreeUnivAlgNSG(S,X);
  let p be FinSequence of A;
  assume 3-tree p is Element of A;
  then reconsider I = 3-tree p as Element of A;
  per cases by Th56;
  suppose ex x being Element of X st I = root-tree x;
    then consider x being Element of X such that
A1: 3-tree p = root-tree x;
    3-tree p = x-tree(<*>TS G) by A1,TREES_4:20;
    then 3 = x by TREES_4:15;
    then X meets NAT by XBOOLE_0:3;
    hence thesis by FREEALG:def 1;
  end;
  suppose ex n being Nat, p being FinSequence of A
    st n in Seg 4 & I = n-tree p & len p = S.n;
    then consider n being Nat, q being FinSequence of A such that
A2: n in Seg 4 & I = n-tree q & len q = S.n;
A3: n = 3 & q = p by A2,TREES_4:15;
    then p =<*p.1,p.2,p.3*> by A2,Th54,FINSEQ_1:62;
    then rng p = {p.1,p.2,p.3} by FINSEQ_2:148;
    then p.1 in {p.1,p.2,p.3} & p.2 in {p.1,p.2,p.3} & p.3 in {p.1,p.2,p.3} &
    {p.1,p.2,p.3} c= the carrier of A by ENUMSET1:def 1;
    then reconsider C = p.1, I1 = p.2, I2 = p.3 as Element of A;
    take C,I1,I2; thus thesis by A3,A2,Th54,FINSEQ_1:62;
  end;
end;

theorem
  for X being disjoint_with_NAT non empty set
  for C1,C2,I1,I2,J1,J2 being Element of FreeUnivAlgNSG(ECIW-signature,X)
  st if-then-else(C1,I1,I2) = if-then-else(C2,J1,J2)
  holds C1 = C2 & I1 = J1 & I2 = J2
proof
  let X be disjoint_with_NAT non empty set;
  set S = ECIW-signature;
  set A = FreeUnivAlgNSG(S,X);
  let C1,C2,I1,I2,J1,J2 be Element of A;
  if-then-else(C1,I1,I2) = 3-tree<*C1,I1,I2*> &
  if-then-else(C2,J1,J2) = 3-tree<*C2,J1,J2*> by Th63;
  then if-then-else(C1,I1,I2) = if-then-else(C2,J1,J2)
  implies <*C1,I1,I2*> = <*C2,J1,J2*> by TREES_4:15;
  hence thesis by GROUP_7:3;
end;

theorem Th66:
  for X being disjoint_with_NAT non empty set
  for C,I being Element of FreeUnivAlgNSG(ECIW-signature,X)
  holds while(C,I) = 4-tree(C,I)
proof
  let X be disjoint_with_NAT non empty set;
  set S = ECIW-signature;
  reconsider s = S as non empty FinSequence of omega;
  set A = FreeUnivAlgNSG(S,X);
  let C,I be Element of A;
A1: 4 in dom the charact of A by Def13;
  reconsider f = (the charact of A).4 as binary (non empty homogeneous
  quasi_total PartFunc of (the carrier of A)*, the carrier of A) by Def13;
A2: f = FreeOpNSG(4,S,X) by A1,FREEALG:def 12;
A3: 4 in dom S by Th54;
  then s/.4 = S.4 by PARTFUN1:def 8;
  then
A4: dom FreeOpNSG(4,S,X) = 2-tuples_on TS(DTConUA(S,X))
  by A3,Th54,FREEALG:def 11;
A5: <*C,I*> in 2-tuples_on TS(DTConUA(S,X)) by CATALG_1:10;
  thus while(C,I) = f.<*C,I*> by A1,FUNCT_7:def 1
    .= Sym(4,S,X)-tree(<*C,I*>) by A2,A4,A5,A3,FREEALG:def 11
    .= 4-tree(C,I) by A3,FREEALG:def 10;
end;

theorem Th67:
  for X being disjoint_with_NAT non empty set
  for p being FinSequence of FreeUnivAlgNSG(ECIW-signature,X)
  st 4-tree p is Element of FreeUnivAlgNSG(ECIW-signature,X)
  ex C,I being Element of FreeUnivAlgNSG(ECIW-signature,X) st p = <*C,I*>
proof
  let X be disjoint_with_NAT non empty set;
  set S = ECIW-signature;
  set G = DTConUA(S,X);
  set A = FreeUnivAlgNSG(S,X);
  let p be FinSequence of A;
  assume 4-tree p is Element of A;
  then reconsider I = 4-tree p as Element of A;
  per cases by Th56;
  suppose ex x being Element of X st I = root-tree x;
    then consider x being Element of X such that
A1: 4-tree p = root-tree x;
    4-tree p = x-tree(<*>TS G) by A1,TREES_4:20;
    then 4 = x by TREES_4:15;
    then X meets NAT by XBOOLE_0:3;
    hence thesis by FREEALG:def 1;
  end;
  suppose ex n being Nat, p being FinSequence of A
    st n in Seg 4 & I = n-tree p & len p = S.n;
    then consider n being Nat, q being FinSequence of A such that
A2: n in Seg 4 & I = n-tree q & len q = S.n;
A3: n = 4 & q = p by A2,TREES_4:15;
    then p = <*p.1,p.2*> by A2,Th54,FINSEQ_1:61;
    then rng p = {p.1,p.2} by FINSEQ_2:147;
    then reconsider I1 = p.1, I2 = p.2 as Element of A by ZFMISC_1:38;
    take I1,I2; thus thesis by A3,A2,Th54,FINSEQ_1:61;
  end;
end;

theorem Th68:
  for X being disjoint_with_NAT non empty set
  for I being Element of FreeUnivAlgNSG(ECIW-signature,X)
  st I in ElementaryInstructions FreeUnivAlgNSG(ECIW-signature,X)
  ex x being Element of X st I = x-tree {}
proof
  let X be disjoint_with_NAT non empty set;
  set S = ECIW-signature;
  set A = FreeUnivAlgNSG(S, X);
  let I be Element of FreeUnivAlgNSG(ECIW-signature,X) such that
A1: I in ElementaryInstructions FreeUnivAlgNSG(ECIW-signature,X);
  per cases by Th56;
  suppose ex x being Element of X st I = root-tree x;
    then consider x being Element of X such that
A2: I = root-tree x;
    root-tree x = x-tree {} by TREES_4:20;
    hence thesis by A2;
  end;
  suppose
    ex n being Nat, p being FinSequence of FreeUnivAlgNSG(ECIW-signature,X)
    st n in Seg 4 & I = n-tree p & len p = S.n;
    then consider n being Nat,
    p being FinSequence of FreeUnivAlgNSG(ECIW-signature,X) such that
A3: n in Seg 4 & I = n-tree p & len p = S.n;
    per cases by A3,FINSEQ_3:2,ENUMSET1:def 2;
    suppose
A4:   n = 1;
      then p = {} by A3,Th58;
      then I = EmptyIns A by A3,A4,Th57;
      hence thesis by A1,Th49;
    end;
    suppose
A5:   n = 2;
      then consider I1,I2 being Element of A such that
A6:   p = <*I1,I2*> by A3,Th60;
A7:   I = n-tree(I1,I2) by A3,A6
        .= I1\;I2 by A5,Th59;
      then I <> I1 & I <> I2 by Th61;
      hence thesis by A1,A7,Th50;
    end;
    suppose
A8:   n = 3;
      then consider C,I1,I2 being Element of A such that
A9:   p = <*C,I1,I2*> by A3,Th64;
      I = if-then-else(C,I1,I2) by A3,A8,A9,Th63;
      hence thesis by A1,Th51;
    end;
    suppose
A10:  n = 4;
      then consider C,I' being Element of A such that
A11:  p = <*C,I'*> by A3,Th67;
      I = n-tree(C,I') by A3,A11
        .= while(C,I') by A10,Th66;
      hence thesis by A1,Th52;
    end;
  end;
end;

theorem
  for X being disjoint_with_NAT non empty set
  for p being FinSequence of FreeUnivAlgNSG(ECIW-signature,X)
  for x being Element of X
  st x-tree p is Element of FreeUnivAlgNSG(ECIW-signature,X) holds p = {}
proof
  let X be disjoint_with_NAT non empty set;
  set S = ECIW-signature;
  set A = FreeUnivAlgNSG(S, X);
  let p be FinSequence of FreeUnivAlgNSG(ECIW-signature,X);
  let x be Element of X;
  assume x-tree p is Element of FreeUnivAlgNSG(ECIW-signature,X);
  then reconsider I = x-tree p as Element of A;
  now
    given n being Nat, p being FinSequence of A such that
A1: n in Seg 4 & I = n-tree p & len p = ECIW-signature.n;
    x = n & X misses NAT & n in NAT by A1,TREES_4:15,FREEALG:def 1;
    hence contradiction by XBOOLE_0:3;
  end;
  then consider y being Element of X such that
A2: I = root-tree y by Th56;
  x-tree p = y-tree {} & {} is DTree-yielding by A2,TREES_4:20,TREES_3:23;
  hence p = {} by TREES_4:15;
end;

theorem Th70:
  for X being disjoint_with_NAT non empty set
  holds ElementaryInstructions FreeUnivAlgNSG(ECIW-signature,X) =
  FreeGenSetNSG(ECIW-signature,X) &
  Card X = Card FreeGenSetNSG(ECIW-signature,X)
proof
  let X be disjoint_with_NAT non empty set;
  set S = ECIW-signature;
  set G = DTConUA(S,X);
A1: X = Terminals G by FREEALG:3;
  set A = FreeUnivAlgNSG(S, X);
  thus ElementaryInstructions A = FreeGenSetNSG(S, X)
  proof
    thus ElementaryInstructions A c= FreeGenSetNSG(S, X)
    proof
      let x be set;
      assume x in ElementaryInstructions A;
      then consider y being Element of X such that
A2:   x = y-tree {} by Th68;
      reconsider y as Symbol of G by XBOOLE_0:def 2;
      x = root-tree y by A2,TREES_4:20;
      hence thesis by A1;
    end;
    let x be set;
    assume
A3: x in FreeGenSetNSG(S,X);
    then reconsider I = x as Element of A;
    consider y being Symbol of G such that
A4: x = root-tree y & y in Terminals G by A3;
A5: x = y-tree {} & {} is DTree-yielding by A4,TREES_3:23,TREES_4:20;
    assume
A6: x nin ElementaryInstructions A;
    per cases by A6,Th53;
    suppose I = EmptyIns A;
      then x = 1-tree {} by Th57;
      then y = 1 & X misses NAT by FREEALG:def 1,A5,TREES_4:15;
      hence thesis by A1,A4,XBOOLE_0:3;
    end;
    suppose ex I1,I2 being Element of A st
      I = I1\;I2 & I1 <> I1\;I2 & I2 <> I1\;I2;
      then consider I1,I2 be Element of A such that
A7:   I = I1\;I2;
      x = 2-tree(I1,I2) by A7,Th59
        .= 2-tree<*I1,I2*>;
      hence thesis by A5,TREES_4:15;
    end;
    suppose ex C,I1,I2 being Element of A st I = if-then-else(C,I1,I2);
      then consider C,I1,I2 be Element of A such that
A8:   I = if-then-else(C,I1,I2);
      x = 3-tree<*C,I1,I2*> by A8,Th63;
      hence thesis by A5,TREES_4:15;
    end;
    suppose ex C,J being Element of A st I = while(C,J);
      then consider C,J be Element of A such that
A9:   I = while(C,J);
      x = 4-tree(C,J) by A9,Th66
        .= 4-tree<*C,J*>;
      hence thesis by A5,TREES_4:15;
    end;
  end;
  deffunc F(set) = root-tree $1;
  consider f being Function such that
A10: dom f = X & for x being Element of X holds f.x = F(x) from FUNCT_1:sch 4;
A11: rng f = FreeGenSetNSG(S,X)
  proof
    thus rng f c= FreeGenSetNSG(S,X)
    proof
      let a be set;
      assume a in rng f;
      then consider x being set such that
A12:  x in X & a = f.x by A10,FUNCT_1:def 5;
      reconsider s = x as Symbol of G by A12,XBOOLE_0:def 2;
      s in X & a = F(x) by A10,A12;
      hence thesis by A1;
    end;
    let a be set;
    assume a in FreeGenSetNSG(S,X);
    then consider s being Symbol of G such that
A13: a = root-tree s & s in X by A1;
    reconsider s as Element of X by A13;
    f.s = a by A10,A13;
    hence thesis by A10,FUNCT_1:def 5;
  end;
  f is one-to-one
  proof
    let a,b be set;
    assume a in dom f & b in dom f;
    then reconsider x = a, y = b as Element of X by A10;
    assume f.a = f.b;
    then F(x) = f.b by A10
      .= F(y) by A10;
    hence thesis by TREES_4:4;
  end;
  then X, FreeGenSetNSG(S,X) are_equipotent by A10,A11,WELLORD2:def 4;
  hence Card X = Card FreeGenSetNSG(S,X) by CARD_1:21;
end;

registration
  cluster infinite disjoint_with_NAT set;
  existence
  proof
    take X = [:NAT,{0}:];
    thus X is infinite;
    now
      let x be set;
      assume x in X;
      then consider a,b being set such that
A1:   a in NAT & b in {0} & x = [a,b] by ZFMISC_1:def 2;
      assume x in NAT;
      then x is Element of NAT & [a,b] is pair;
      hence contradiction by A1;
    end;
    hence X misses NAT by XBOOLE_0:3;
  end;
end;

registration
  let X be infinite disjoint_with_NAT set;
  cluster FreeUnivAlgNSG(ECIW-signature,X) -> infinite;
  coherence
  proof
    ElementaryInstructions FreeUnivAlgNSG(ECIW-signature,X) =
    FreeGenSetNSG(ECIW-signature,X) &
    Card X = Card FreeGenSetNSG(ECIW-signature,X) by Th70;
    then Card ElementaryInstructions FreeUnivAlgNSG(ECIW-signature,X) is
    infinite by CARD_4:1;
    hence ElementaryInstructions FreeUnivAlgNSG(ECIW-signature,X) is infinite;
  end;
end;

registration
  let X be disjoint_with_NAT non empty set;
  cluster FreeUnivAlgNSG(ECIW-signature,X) -> ECIW-strict;
  coherence
  proof
    thus signature FreeUnivAlgNSG(ECIW-signature,X) = ECIW-signature
    by FREEALG:4;
  end;
end;

theorem Th71:
  for A being preIfWhileAlgebra holds Generators A c= ElementaryInstructions A
proof
  let A be preIfWhileAlgebra;
  let x be set;
  assume
A1: x in Generators A & x nin ElementaryInstructions A;
  then reconsider x as Element of A;
  dom Den(In(1, dom the charact of A), A) = {{}} by Th42;
  then
A2: {} in dom Den(In(1, dom the charact of A),A) by TARSKI:def 1;
  per cases by A1,Th53;
  suppose x = EmptyIns A;
    then x in rng Den(In(1, dom the charact of A), A) by A2,FUNCT_1:12;
    hence contradiction by A1,Th26;
  end;
  suppose
    ex I1,I2 being Element of A st x = I1\;I2 & I1 <> I1\;I2 & I2 <> I1\;I2;
    then consider I1,I2 being Element of A such that
A3: x = I1\;I2 & I1 <> I1\;I2 & I2 <> I1\;I2;
    dom Den(In(2, dom the charact of A), A) = 2-tuples_on the carrier of A
    by Th44;
    then <*I1,I2*> in dom Den(In(2, dom the charact of A),A) by CATALG_1:10;
    then x in rng Den(In(2, dom the charact of A),A) by A3,FUNCT_1:12;
    hence contradiction by A1,Th26;
  end;
  suppose ex C,I1,I2 being Element of A st x = if-then-else(C,I1,I2);
    then consider C,I1,I2 being Element of A such that
A4: x = if-then-else(C,I1,I2);
    dom Den(In(3, dom the charact of A), A) = 3-tuples_on the carrier of A
    by Th47;
    then <*C,I1,I2*> in dom Den(In(3, dom the charact of A),A) by CATALG_1:12;
    then x in rng Den(In(3, dom the charact of A),A) by A4,FUNCT_1:12;
    hence contradiction by A1,Th26;
  end;
  suppose ex C,J being Element of A st x = while(C,J);
    then consider C,J being Element of A such that
A5: x = while(C,J);
    dom Den(In(4, dom the charact of A), A) = 2-tuples_on the carrier of A
    by Th48;
    then <*C,J*> in dom Den(In(4, dom the charact of A),A) by CATALG_1:10;
    then x in rng Den(In(4, dom the charact of A),A) by A5,FUNCT_1:12;
    hence contradiction by A1,Th26;
  end;
end;

theorem Th72:
  for A being preIfWhileAlgebra st A is free for C,I1,I2 being Element of A
  holds EmptyIns A <> I1\;I2 & EmptyIns A <> if-then-else(C,I1,I2) &
  EmptyIns A <> while(C,I1)
proof
  let A be preIfWhileAlgebra such that
A1: A is free;
  let C,I1,I2 be Element of A;
  1 in dom the charact of A by Def10;
  then
A2: dom Den(In(1, dom the charact of A), A) = {{}} &
  In(1, dom the charact of A) = 1 by Th42,FUNCT_7:def 1;
  2 in dom the charact of A by Def11;
  then
A3: dom Den(In(2, dom the charact of A), A) = 2-tuples_on the carrier of A &
  In(2, dom the charact of A) = 2 by Th44,FUNCT_7:def 1;
  3 in dom the charact of A by Def12;
  then
A4: dom Den(In(3, dom the charact of A), A) = 3-tuples_on the carrier of A &
  In(3, dom the charact of A) = 3 by Th47,FUNCT_7:def 1;
  4 in dom the charact of A by Def13;
  then
A5: dom Den(In(4, dom the charact of A), A) = 2-tuples_on the carrier of A &
  In(4, dom the charact of A) = 4 by Th48,FUNCT_7:def 1;
A6: {} in {{}} by TARSKI:def 1;
  <*I1,I2*> in 2-tuples_on the carrier of A by CATALG_1:10;
  hence EmptyIns A <> I1\;I2 by A1,A2,A3,A6,Th36;
  <*C,I1,I2*> in 3-tuples_on the carrier of A by CATALG_1:12;
  hence EmptyIns A <> if-then-else(C,I1,I2) by A1,A2,A4,A6,Th36;
  <*C,I1*> in 2-tuples_on the carrier of A by CATALG_1:10;
  hence EmptyIns A <> while(C,I1) by A1,A2,A5,A6,Th36;
end;

theorem Th73:
  for A being preIfWhileAlgebra st A is free
  for I1,I2,C,J1,J2 being Element of A holds I1\;I2 <> I1 & I1\;I2 <> I2 &
  (I1\;I2 = J1\;J2 implies I1 = J1 & I2 = J2) &
  I1\;I2 <> if-then-else(C,J1,J2) & I1\;I2 <> while(C,J1)
proof
  let A be preIfWhileAlgebra such that
A1: A is free;
  let I1,I2,C,J1,J2 be Element of A;
  2 in dom the charact of A by Def11;
  then
A2: dom Den(In(2, dom the charact of A), A) = 2-tuples_on the carrier of A &
  In(2, dom the charact of A) = 2 by Th44,FUNCT_7:def 1;
  3 in dom the charact of A by Def12;
  then
A3: dom Den(In(3, dom the charact of A), A) = 3-tuples_on the carrier of A &
  In(3, dom the charact of A) = 3 by Th47,FUNCT_7:def 1;
  4 in dom the charact of A by Def13;
  then
A4: dom Den(In(4, dom the charact of A), A) = 2-tuples_on the carrier of A &
  In(4, dom the charact of A) = 4 by Th48,FUNCT_7:def 1;
A5: <*I1,I2*> in 2-tuples_on the carrier of A &
  <*J1,J2*> in 2-tuples_on the carrier of A by CATALG_1:10;
  rng <*I1,I2*> = {I1,I2} by FINSEQ_2:147;
  then I1 in rng <*I1,I2*> & I2 in rng <*I1,I2*> by TARSKI:def 2;
  hence I1\;I2 <> I1 & I1\;I2 <> I2 by A1,A2,A5,Th38;
  hereby
    assume I1\;I2 = J1\;J2;
    then <*I1,I2*> = <*J1,J2*> by A1,A2,A5,Th36;
    hence I1 = J1 & I2 = J2 by GROUP_7:2;
  end;
  <*C,J1,J2*> in 3-tuples_on the carrier of A by CATALG_1:12;
  hence I1\;I2 <> if-then-else(C,J1,J2) by A1,A2,A3,A5,Th36;
  <*C,J1*> in 2-tuples_on the carrier of A by CATALG_1:10;
  hence I1\;I2 <> while(C,J1) by A1,A2,A4,A5,Th36;
end;

theorem Th74:
  for A being preIfWhileAlgebra st A is free
  for C,I1,I2,D,J1,J2 being Element of A
  holds if-then-else(C,I1,I2) <> C & if-then-else(C,I1,I2) <> I1 &
  if-then-else(C,I1,I2) <> I2 & if-then-else(C,I1,I2) <> while(D,J1) &
  (if-then-else(C,I1,I2) = if-then-else(D,J1,J2) implies C=D & I1=J1 & I2=J2)
proof
  let A be preIfWhileAlgebra such that
A1: A is free;
  let C,I1,I2,D,J1,J2 be Element of A;
  3 in dom the charact of A by Def12;
  then
A2: dom Den(In(3, dom the charact of A), A) = 3-tuples_on the carrier of A &
  In(3, dom the charact of A) = 3 by Th47,FUNCT_7:def 1;
  4 in dom the charact of A by Def13;
  then
A3: dom Den(In(4, dom the charact of A), A) = 2-tuples_on the carrier of A &
  In(4, dom the charact of A) = 4 by Th48,FUNCT_7:def 1;
A4: <*C,I1,I2*> in 3-tuples_on the carrier of A &
  <*D,J1,J2*> in 3-tuples_on the carrier of A by CATALG_1:12;
  rng <*C,I1,I2*> = {C,I1,I2} by FINSEQ_2:148;
  then C in rng <*C,I1,I2*> & I1 in rng <*C,I1,I2*> & I2 in rng <*C,I1,I2*>
  by ENUMSET1:def 1;
  hence if-then-else(C,I1,I2) <> C & if-then-else(C,I1,I2) <> I1 &
  if-then-else(C,I1,I2) <> I2 by A1,A2,A4,Th38;
  <*D,J1*> in 2-tuples_on the carrier of A by CATALG_1:10;
  hence if-then-else(C,I1,I2) <> while(D,J1) by A1,A2,A3,A4,Th36;
  assume if-then-else(C,I1,I2) = if-