:: Preliminaries to the Lambek Calculus
::  by Wojciech Zielonka
::
:: Received February 13, 1991
:: Copyright (c) 1991-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, STRUCT_0, BINOP_1, SUBSET_1, FINSEQ_1, FUNCT_1,
      VALUED_1, RELAT_1, FINSET_1, TREES_2, ZFMISC_1, NUMBERS, CARD_1, MCART_1,
      ORDINAL4, FUNCOP_1, TARSKI, ORDINAL1, XXREAL_0, ARYTM_3, CARD_3, NAT_1,
      REAL_1, FUNCT_5, PRELAMB;
 notations TARSKI, XBOOLE_0, ZFMISC_1,
      XTUPLE_0, SUBSET_1, CARD_1, NUMBERS, REAL_1,
      BINOP_1, RELSET_1, FINSEQ_1, FINSEQ_2, FINSET_1, MCART_1, STRUCT_0,
      RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, FUNCT_5, RVSUM_1, XCMPLX_0,
      ORDINAL1, NAT_1, TREES_1, TREES_2, XXREAL_0;
 constructors BINOP_1, FUNCT_3, XXREAL_0, NAT_1, RVSUM_1, TREES_2, MIDSP_1,
      FUNCT_5, RELSET_1, BINOP_2, FUNCOP_1, REAL_1, XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1,
      NUMBERS, MEMBERED, FINSEQ_1, TREES_2, STRUCT_0, VALUED_0, RELSET_1,
      CARD_1, XTUPLE_0;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, STRUCT_0, XBOOLE_0, BINOP_1, XTUPLE_0;
 theorems FINSEQ_1, ZFMISC_1, TREES_2, FUNCOP_1, FUNCT_2, TARSKI, MCART_1,
      CARD_1, TREES_1, NAT_1, CARD_2, RVSUM_1, RELAT_1, XBOOLE_1, FINSEQ_2;
 schemes FUNCT_2, FINSEQ_2;

begin :: Proofs and cut-freedom

definition
  struct (1-sorted) typealg
        (#carrier -> set,
    left_quotient, right_quotient, inner_product -> BinOp of the carrier #);
end;

registration
  cluster non empty strict for typealg;
  existence
  proof
    set l = the BinOp of {{}};
    take typealg(#{{}},l,l,l#);
    thus the carrier of typealg(#{{}},l,l,l#) is non empty;
    thus thesis;
  end;
end;

definition
  let s be non empty typealg;
  mode type of s is Element of s;
end;

reserve s for non empty typealg,
  T,X,Y,T9,X9,Y9 for FinSequence of s,
  x,y,z,y9,z9 for type of s;

definition
  let s,x,y;
  func x\y -> type of s equals
  (the left_quotient of s).(x,y);
  coherence;
  func x/"y -> type of s equals
  (the right_quotient of s).(x,y);
  coherence;
  func x*y -> type of s equals
  (the inner_product of s).(x,y);
  coherence;
end;

definition
  let s;
  mode PreProof of s is finite DecoratedTree of [:[: (the carrier of s)*,
    the carrier of s :], NAT :];
end;

reserve Tr for PreProof of s;

definition
  let s, Tr;
  let v be Element of dom Tr;

  attr v is correct means
  :Def4:
  branchdeg v = 0 & ex x st (Tr.v)`1 = [<*x*>,x] if (Tr.v)`2 = 0,
  branchdeg v = 1 & ex T,x,y st (Tr.v)`1 = [T,x/"y] & (Tr.(v^<*0*>))`1 =
  [T^<*y*>,x] if (Tr.v)`2 = 1,
  branchdeg v = 1 & ex T,x,y st (Tr.v)`1 = [T,y\x] & (Tr.(v^<*0*>))`1 =
  [<*y*>^T,x] if (Tr.v)`2 = 2,
  branchdeg v = 2 & ex T,X,Y,x,y,z st (Tr.v)`1 = [X^<*x/"y*>^T^Y,z] &
  (Tr.(v^<*0*>))`1 = [T,y] & (Tr.(v^<*1*>))`1 = [X^<*x*>^Y,z] if (Tr.v)`2 = 3,
  branchdeg v = 2 & ex T,X,Y,x,y,z st (Tr.v)`1 = [X^T^<*y\x*>^Y,z] &
  (Tr.(v^<*0*>))`1 = [T,y] & (Tr.(v^<*1*>))`1 = [X^<*x*>^Y,z] if (Tr.v)`2 = 4,
  branchdeg v = 1 & ex X,x,y,Y st (Tr.v)`1 = [X^<*x*y*>^Y,z] &
  (Tr.(v^<*0*>))`1 = [X^<*x*>^<*y*>^Y,z] if (Tr.v)`2 = 5,
  branchdeg v = 2 & ex X,Y,x,y st (Tr.v)`1 = [X^Y,x*y] & (Tr.(v^<*0*>))`1 =
  [X,x] & (Tr.(v^<*1*>))`1 = [Y,y] if (Tr.v)`2 = 6,
  branchdeg v = 2 & ex T,X,Y,y,z st (Tr.v)`1 = [X^T^Y,z] &
  (Tr.(v^<*0*>))`1 = [T,y] & (Tr.(v^<*1*>))`1 = [X^<*y*>^Y,z] if (Tr.v)`2 = 7
  otherwise contradiction;
  correctness;
end;

definition
  let s;
  let IT be type of s;
  attr IT is left means
  ex x,y st IT = x\y;
  attr IT is right means
  ex x,y st IT = x/"y;
  attr IT is middle means
  ex x,y st IT = x*y;
end;

definition
  let s;
  let IT be type of s;
  attr IT is primitive means
  not (IT is left or IT is right or IT is middle);
end;

definition
  let s;
  let Tr be finite DecoratedTree of the carrier of s;
  let v be Element of dom Tr;
  redefine func Tr.v -> type of s;
  coherence
  proof
    reconsider Tr as DecoratedTree of the carrier of s;
    reconsider v as Element of dom Tr;
    Tr.v is type of s;
    hence thesis;
  end;
end;

definition
  let s;
  let Tr be finite DecoratedTree of the carrier of s, x;
  pred Tr represents x means
  dom Tr is finite &
  for v being Element of dom Tr holds (branchdeg v = 0 or branchdeg v = 2)
  & (branchdeg v = 0 implies Tr.v is primitive) & (branchdeg v = 2 implies
  ex y,z st (Tr.v = y/"z or Tr.v = y\z or Tr.v = y*z) &
  Tr.(v^<*0*>) = y & Tr.(v^<*1*>)= z);
end;

notation
  let s;
  let Tr be finite DecoratedTree of the carrier of s, x;
  antonym Tr does_not_represent x for Tr represents x;
end;

definition
  let IT be non empty typealg;
  attr IT is free means
  :Def10:
  not (ex x being type of IT st x is left right
  or x is left middle or x is right middle) & for x being type of IT ex Tr
  being finite DecoratedTree of the carrier of IT st
  for Tr1 being finite DecoratedTree of
  the carrier of IT holds Tr1 represents x iff Tr = Tr1;
end;

definition
  let s,x such that
A1: s is free;
  func repr_of x -> finite DecoratedTree of the carrier of s means
  for Tr being finite DecoratedTree of the carrier of s holds
    Tr represents x iff it = Tr;
  existence by A1,Def10;
  uniqueness
  proof
    let tr1, tr2 be finite DecoratedTree of the carrier of s such that
A1: for Tr being finite DecoratedTree of
    the carrier of s holds Tr represents x iff tr1 = Tr and
A2: for Tr being finite DecoratedTree of
    the carrier of s holds Tr represents x iff tr2 = Tr;
    tr1 represents x by A1;
    hence thesis by A2;
  end;
end;

deffunc PAIRSOF(typealg) = [: (the carrier of $1)*, the carrier of $1 :];

definition
  let s;
  let f be FinSequence of s;
  let t be type of s;
  redefine func [f,t] -> Element of [:(the carrier of s)*, the carrier of s:];
  coherence
  proof
    f in (the carrier of s)* by FINSEQ_1:def 11;
    hence thesis by ZFMISC_1:87;
  end;
end;

definition
  let s;
  mode Proof of s -> PreProof of s means
    :Def12:
    dom it is finite & for v being Element of dom it holds v is correct;
  existence
  proof
    set x = the type of s;
    set Tr = {{}} --> [[<*x*>,x],0];
A1: dom Tr = {{}} by FUNCOP_1:13;
    reconsider Tr as finite DecoratedTree
    by TREES_1:23;
A2: [[<*x*>,x],0] in [:PAIRSOF(s), NAT:] by ZFMISC_1:87;
    {[[<*x*>,x],0]} = rng Tr by FUNCOP_1:8;
    then rng Tr c= [:PAIRSOF(s), NAT:] by A2,ZFMISC_1:31;
    then reconsider Tr as PreProof of s by RELAT_1:def 19;
    take Tr;
    thus dom Tr is finite;
    let v be Element of dom Tr;
A3: v = {} by A1,TARSKI:def 1;
A4: now set x = the Element of dom Tr-level 1;
      assume dom Tr-level 1 <> {};
      then x in dom Tr-level 1;
      then x in {w where w is Element of dom Tr: len w = 1} by TREES_2:def 6;
      then ex w being Element of dom Tr st ( x = w)&( len w = 1);
      hence contradiction by A1,CARD_1:27,TARSKI:def 1;
    end;
A5: branchdeg v = card succ v by TREES_2:def 12
      .= 0 by A3,A4,CARD_1:27,TREES_2:13;
A6: Tr.v = [[<*x*>,x],0] by A1,FUNCOP_1:7;
    then
A7: (Tr.v)`1 = [<*x*>,x] by MCART_1:7;
    (Tr.v)`2 = 0 by A6,MCART_1:7;
    hence thesis by A5,A7,Def4;
  end;
end;

reserve p for Proof of s,
  v for Element of dom p;

theorem Th1:
  branchdeg v = 1 implies v^<*0*> in dom p
proof
  assume branchdeg v = 1;
  then
A1: succ v <> {} by CARD_1:27,TREES_2:def 12;
  set x = the Element of succ v;
  x in succ v by A1;
  then x in {v^<*n*> where n is Element of NAT: v^<*n*> in dom p}
  by TREES_2:def 5;
  then consider n being Element of NAT such that x = v^<*n*> and
A2: v^<*n*> in dom p;
  0 <= n by NAT_1:2;
  hence thesis by A2,TREES_1:def 3;
end;

theorem Th2:
  branchdeg v = 2 implies v^<*0*> in dom p & v^<*1*> in dom p
proof
A1: succ v = {v^<*n*> where n is Element of NAT: v^<*n*> in dom p}
  by TREES_2:def 5;
  assume branchdeg v = 2;
  then card succ v = 2 by TREES_2:def 12;
  then consider x,y being set such that
A2: x <> y and
A3: succ v = {x,y} by CARD_2:60;
  x in succ v by A3,TARSKI:def 2;
  then consider n being Element of NAT such that
A4: x = v^<*n*> and
A5: v^<*n*> in dom p by A1;
  y in succ v by A3,TARSKI:def 2;
  then consider k being Element of NAT such that
A6: y = v^<*k*> and
A7: v^<*k*> in dom p by A1;
  n <> 0 or k <> 0 by A2,A4,A6;
  then
A8: n > 0 or k > 0 by NAT_1:3;
  hence v^<*0*> in dom p by A5,A7,TREES_1:def 3;
  n >= 0+1 or k >= 0+1 by A8,NAT_1:13;
  hence thesis by A5,A7,TREES_1:def 3;
end;

theorem
  (p.v)`2 = 0 implies ex x st (p.v)`1 = [<*x*>,x]
proof
  v is correct by Def12;
  hence thesis by Def4;
end;

theorem
  (p.v)`2 = 1 implies ex w being Element of dom p, T,x,y st w = v^<*0*> &
  (p.v)`1 = [T,x/"y] & (p.w)`1 = [T^<*y*>,x]
proof
A1: v is correct by Def12;
  assume
A2: (p.v)`2 = 1;
  then
A3: ex T,x,y st (p.v)`1 = [T,x/"y] & (p.(v^<*0*>))`1 = [T^<*y*>,x] by A1,Def4;
  branchdeg v = 1 by A1,A2,Def4;
  then v^<*0*> in dom p by Th1;
  hence thesis by A3;
end;

theorem
  (p.v)`2 = 2 implies ex w being Element of dom p, T,x,y st w = v^<*0*> &
  (p.v)`1 = [T,y\x] & (p.w)`1 = [<*y*>^T,x]
proof
A1: v is correct by Def12;
  assume
A2: (p.v)`2 = 2;
  then
A3: ex T,x,y st (p.v)`1 = [T,y\x] & (p.(v^<*0*>))`1 = [<*y*>^T,x] by A1,Def4;
  branchdeg v = 1 by A1,A2,Def4;
  then v^<*0*> in dom p by Th1;
  hence thesis by A3;
end;

theorem
  (p.v)`2 = 3 implies ex w,u being Element of dom p, T,X,Y,x,y,z st
  w = v^<*0*> & u = v^<*1*> & (p.v)`1 = [X^<*x/"y*>^T^Y,z] &
  (p.w)`1 = [T,y] & (p.u)`1 = [X^<*x*>^Y,z]
proof
A1: v is correct by Def12;
  assume
A2: (p.v)`2 = 3;
  then
A3: ex T,X,Y,x,y,z st (p.v)`1 = [X^<*x/"y*>^T^Y,z] &
  (p.(v^<*0*>))`1 = [T,y] & (p.(v^<*1*>))`1 = [X^<*x*>^Y,z] by A1,Def4;
A4: branchdeg v = 2 by A1,A2,Def4;
  then
A5: v^<*0*> in dom p by Th2;
  v^<*1*> in dom p by A4,Th2;
  hence thesis by A3,A5;
end;

theorem
  (p.v)`2 = 4 implies ex w,u being Element of dom p, T,X,Y,x,y,z st
  w = v^<*0*> & u = v^<*1*> & (p.v)`1 = [X^T^<*y\x*>^Y,z] &
  (p.w)`1 = [T,y] & (p.u)`1 = [X^<*x*>^Y,z]
proof
A1: v is correct by Def12;
  assume
A2: (p.v)`2 = 4;
  then
A3: ex T,X,Y,x,y,z st (p.v)`1 = [X^T^<*y\x*>^Y,z] &
  (p.(v^<*0*>))`1 = [T,y] & (p.(v^<*1*>))`1 = [X^<*x*>^Y,z] by A1,Def4;
A4: branchdeg v = 2 by A1,A2,Def4;
  then
A5: v^<*0*> in dom p by Th2;
  v^<*1*> in dom p by A4,Th2;
  hence thesis by A3,A5;
end;

theorem
  (p.v)`2 = 5 implies ex w being Element of dom p, X,x,y,Y st w = v^<*0*> &
  (p.v)`1 = [X^<*x*y*>^Y,z] & (p.w)`1 = [X^<*x*>^<*y*>^Y,z]
proof
A1: v is correct by Def12;
  assume
A2: (p.v)`2 = 5;
  then
A3: ex X,x,y,Y st (p.v)`1 = [X^<*x*y*>^Y,z] & (p.(v^<*0*>))`1 =
  [X^<*x*>^<*y*>^Y,z] by A1,Def4;
  branchdeg v = 1 by A1,A2,Def4;
  then v^<*0*> in dom p by Th1;
  hence thesis by A3;
end;

theorem
  (p.v)`2 = 6 implies ex w,u being Element of dom p, X,Y,x,y st w = v^<*0*> &
  u = v^<*1*> & (p.v)`1 = [X^Y,x*y] & (p.w)`1 = [X,x] & (p.u)`1 = [Y,y]
proof
A1: v is correct by Def12;
  assume
A2: (p.v)`2 = 6;
  then
A3: ex X,Y,x,y st (p.v)`1 = [X^Y,x*y] & (p.(v^<*0*>))`1 = [X,x] &
  (p.(v^<*1*>))`1 = [Y,y] by A1,Def4;
A4: branchdeg v = 2 by A1,A2,Def4;
  then
A5: v^<*0*> in dom p by Th2;
  v^<*1*> in dom p by A4,Th2;
  hence thesis by A3,A5;
end;

theorem Th10:
  (p.v)`2 = 7 implies ex w,u being Element of dom p, T,X,Y,y,z st w = v^<*0 *>
  & u = v^<*1*> & (p.v)`1 = [X^T^Y,z] & (p.w)`1 = [T,y] & (p.u)`1 =
  [X^<*y*>^Y,z]
proof
A1: v is correct by Def12;
  assume
A2: (p.v)`2 = 7;
  then
A3: ex T,X,Y,y,z st (p.v)`1 = [X^T^Y,z] & (p.(v^<*0*>))`1 = [T,y] &
  (p.(v^<*1*>))`1 = [X^<*y*>^Y,z] by A1,Def4;
A4: branchdeg v = 2 by A1,A2,Def4;
  then
A5: v^<*0*> in dom p by Th2;
  v^<*1*> in dom p by A4,Th2;
  hence thesis by A3,A5;
end;

theorem
  (p.v)`2 = 0 or (p.v)`2 = 1 or (p.v)`2 = 2 or (p.v)`2 = 3 or (p.v)`2 = 4 or
  (p.v)`2 = 5 or (p.v)`2 = 6 or (p.v)`2 = 7
proof
  v is correct by Def12;
  hence thesis by Def4;
end;

definition
  let s;
  let IT be PreProof of s;
  attr IT is cut-free means
  for v being Element of dom IT holds (IT.v)`2 <> 7;
end;

definition
  let s;
  func size_w.r.t. s -> Function of the carrier of s, NAT means
  for x holds it.x = card dom repr_of x;
  existence
  proof
    deffunc F(type of s) = card dom repr_of $1;
    thus ex S be Function of the carrier of s, NAT st
    for x holds S.x = F(x) from FUNCT_2:sch 4;
  end;
  uniqueness
  proof
    let f,g be Function of the carrier of s, NAT;
    deffunc F(type of s) = card dom repr_of $1;
    assume that
A1: f.x = F(x) and
A2: g.x = F(x);
    now
      let c be Element of s;
      thus f.c = F(c) by A1
        .= g.c by A2;
    end;
    hence f = g by FUNCT_2:63;
  end;
end;

definition
  let D be non empty set, T be FinSequence of D, f be Function of D,NAT;
  redefine func f*T -> FinSequence of REAL;
  coherence
proof
A1: f*T is FinSequence of NAT by FINSEQ_2:32;
  rng (f*T) c= REAL;
  hence thesis by A1,FINSEQ_1:def 4;
end;
end;

Lm1: for D being non empty set, T being FinSequence of D
for f being Function of D, NAT holds Sum(f*T) is Nat
proof
  let D be non empty set, T be FinSequence of D;
  let f be Function of D, NAT;
  defpred P[FinSequence of REAL] means
  $1 is FinSequence of NAT implies Sum $1 is Nat;
A1: P[<*>REAL] by RVSUM_1:72;
A2: for p be FinSequence of REAL, x be Real st P[p] holds P[p^<*x*>]
  proof
    let p be FinSequence of REAL, x be Real;
    assume
A3: P[p];
    assume p^<*x*> is FinSequence of NAT;
    then
A4: rng (p^<*x*>) c= NAT by FINSEQ_1:def 4;
    rng p c= rng (p^<*x*>) by FINSEQ_1:29;
    then
A5: rng p c= NAT by A4,XBOOLE_1:1;
    rng <*x*> c= rng (p^<*x*>) by FINSEQ_1:30;
    then
A6: rng <*x*> c= NAT by A4,XBOOLE_1:1;
    rng <*x*> = {x} by FINSEQ_1:38;
    then reconsider n=x as Element of NAT by A6,ZFMISC_1:31;
    reconsider s = Sum p as Nat by A3,A5,FINSEQ_1:def 4;
    Sum(p^<*x*>) = s + n by RVSUM_1:74;
    hence thesis;
  end;
A7: for p being FinSequence of REAL holds P[p] from FINSEQ_2:sch 2(A1,A2);
  f*T is FinSequence of NAT by FINSEQ_2:32;
  hence thesis by A7;
end;

definition
  let s;
  let p be Proof of s;
  func cutdeg p -> Nat means
  ex T,X,Y,y,z st (p.{})`1 = [X^T^Y,z] & (p.<*0*>)`1 = [T,y] &
  (p.<*1*>)`1 = [X^<*y*>^Y,z] & it = (size_w.r.t. s).y + (size_w.r.t. s).z
  + Sum((size_w.r.t. s)*(X^T^Y)) if (p.{})`2 = 7 otherwise it = 0;
  existence
  proof
    thus (p.{})`2 = 7 implies ex r being Nat st
    ex T,X,Y,y,z st (p.{})`1 = [X^T^Y,z] & (p.<*0*>)`1 = [T,y] &
    (p.<*1*>)`1 = [X^<*y*>^Y,z] & r = (size_w.r.t. s).y + (size_w.r.t. s).z
    + Sum((size_w.r.t. s)*(X^T^Y))
    proof
A1:   {}^<*0*> = <*0*> by FINSEQ_1:34;
A2:   {}^<*1*> = <*1*> by FINSEQ_1:34;
      reconsider v = {} as Element of dom p by TREES_1:22;
      assume (p.{})`2 = 7;
      then consider w,u being Element of dom p, T,X,Y,y,z such that
A3:   w = v^<*0*> and
A4:   u = v^<*1*> and
A5:   (p.v)`1 = [X^T^Y,z] and
A6:   (p.w)`1 = [T,y] and
A7:   (p.u)`1 = [X^<*y*>^Y,z] by Th10;
      reconsider a = Sum((size_w.r.t. s)*(X^T^Y)) as Nat by Lm1;
      take (size_w.r.t. s).y + (size_w.r.t. s).z + a;
      thus thesis by A1,A2,A3,A4,A5,A6,A7;
    end;
    thus thesis;
  end;
  uniqueness
  proof
    let r1,r2 be Nat;
    thus (p.{})`2 = 7 &
    (ex T,X,Y,y,z st (p.{})`1 = [X^T^Y,z] & (p.<*0*>)`1 = [T,y] &
    (p.<*1*>)`1 = [X^<*y*>^Y,z] & r1 = (size_w.r.t. s).y + (size_w.r.t. s).z
    + Sum((size_w.r.t. s)*(X^T^Y)))
    & (ex T,X,Y,y,z st (p.{})`1 = [X^T^Y,z] & (p.<*0*>)`1 = [T,y] &
    (p.<*1*>)`1 = [X^<*y*>^Y,z] & r2 = (size_w.r.t. s).y + (size_w.r.t. s).z
    + Sum((size_w.r.t. s)*(X^T^Y))) implies r1 = r2
    proof
      assume (p.{})`2 = 7;
      given T,X,Y,y,z such that
A8:   (p.{})`1 = [X^T^Y,z] and
A9:   (p.<*0*>)`1 = [T,y] and (p.<*1*>)`1 = [X^<*y*>^Y,z] and
A10:  r1 = (size_w.r.t. s).y + (size_w.r.t. s).z + Sum((size_w.r.t. s)*(X
      ^T^Y));
      given T9,X9,Y9,y9,z9 such that
A11:  (p.{})`1 = [X9^T9^Y9,z9] and
A12:  (p.<*0*>)`1 = [T9,y9] and (p.<*1*>)`1 = [X9^<*y9*>^Y9,z9] and
A13:  r2 = (size_w.r.t. s).y9 + (size_w.r.t. s).z9 + Sum((size_w.r.t. s)*
      (X9^T9^Y9));
A14:  X^T^Y = [X^T^Y,z]`1
        .= X9^T9^Y9 by A8,A11,MCART_1:7;
A15:  y = [T,y]`2
        .= y9 by A9,A12,MCART_1:7;
      z = [X^T^Y,z]`2
        .= z9 by A8,A11,MCART_1:7;
      hence thesis by A10,A13,A14,A15;
    end;
    thus thesis;
  end;
  consistency;
end;

:: Models for the Lambek calculus

reserve A for non empty set,
  a,a1,a2,b for Element of A*;

definition
  let s,A;
  mode Model of s,A -> Function of the carrier of s, bool (A*) means
    for x,y holds it.(x*y) = { a ^ b : a in it.x & b in it.y } &
    it.(x/"y) = { a1 : for b st b in it.y holds a1 ^ b in it.x } &
    it.(y\x) = {a2: for b st b in it.y holds b ^ a2 in it.x };
  existence
  proof
    {} in A* by FINSEQ_1:49;
    then {{}} c= A* by ZFMISC_1:31;
    then reconsider f = (the carrier of s) --> {{}}
    as Function of the carrier of s, bool (A*) by FUNCOP_1:45;
A1: for t being set st t in f.x holds t = {}
    proof
      let t be set;
      assume t in f.x;
      then t in {{}} by FUNCOP_1:7;
      hence thesis by TARSKI:def 1;
    end;
A2: {} in f.x
    proof
      f.x = {{}} by FUNCOP_1:7;
      hence thesis by TARSKI:def 1;
    end;
A3: {} is Element of A* by FINSEQ_1:49;
    take f;
    let x,y;
    thus f.(x*y) = { a ^ b : a in f.x & b in f.y }
    proof
      thus f.(x*y) c= { a ^ b : a in f.x & b in f.y }
      proof
        let t be set;
        assume t in f.(x*y);
        then
A4:       t = {} by A1;
A5:      {}^{} = {} by FINSEQ_1:34;
A6:     t = {}^{} by A4,A5;
A7:     {} in f.x by A2;
        {} in f.y by A2;
        hence thesis by A6,A7;
      end;
      let t be set;
      assume t in { a ^ b : a in f.x & b in f.y };
      then consider a,b such that
A8:   t = a ^ b and
A9:   a in f.x and
A10:   b in f.y;
A11:   a = {} by A1,A9;
      b = {} by A1,A10;
      then a ^ b = {} by A11,FINSEQ_1:34;
      hence thesis by A2,A8;
    end;
    thus f.(x/"y) = { a : for b st b in f.y holds a ^ b in f.x }
    proof
      thus f.(x/"y) c= { a : for b st b in f.y holds a ^ b in f.x }
      proof
        let t be set;
        assume t in f.(x/"y);
        then
A12:    t = {} by A1;
        now
          let b;
          assume b in f.y;
          then b = {} by A1;
          then {} ^ b = {} by FINSEQ_1:34;
          hence {} ^ b in f.x by A2;
        end;
        hence thesis by A3,A12;
      end;
      let t be set;
      assume t in { a : for b st b in f.y holds a ^ b in f.x };
      then consider a such that
A13:  t = a and
A14:  for b st b in f.y holds a ^ b in f.x;
      {} in f.y by A2;
      then a ^ {} in f.x by A14;
      then a = {} by A1;
      hence thesis by A2,A13;
    end;
    thus f.(y\x) = { a : for b st b in f.y holds b ^ a in f.x }
    proof
      thus f.(y\x) c= { a : for b st b in f.y holds b ^ a in f.x }
      proof
        let t be set;
        assume t in f.(y\x);
        then
A15:    t = {} by A1;
        now
          let b;
          assume b in f.y;
          then b = {} by A1;
          then b ^ {} = {} by FINSEQ_1:34;
          hence b ^ {} in f.x by A2;
        end;
        hence thesis by A3,A15;
      end;
      let t be set;
      assume t in { a : for b st b in f.y holds b ^ a in f.x };
      then consider a such that
A16:  t = a and
A17:  for b st b in f.y holds b ^ a in f.x;
      {} in f.y by A2;
      then {} ^ a in f.x by A17;
      then a = {} by A1;
      hence thesis by A2,A16;
    end;
  end;
end;

:: Axioms, rules, and some of their consequences

definition
  struct(typealg) typestr (# carrier -> set,
    left_quotient, right_quotient, inner_product -> BinOp of the carrier,
    derivability -> Relation of (the carrier)*,the carrier #);
end;

registration
  cluster non empty strict for typestr;
  existence
  proof
    set l = the BinOp of {{}},d = the Relation of {{}}*,{{}};
    take typestr(#{{}},l,l,l,d#);
    thus the carrier of typestr(#{{}},l,l,l,d#) is non empty;
    thus thesis;
  end;
end;

reserve s for non empty typestr,
  x for type of s;

definition
  let s;
  let f be FinSequence of s, x;
  pred f ==>. x means
  :Def17:
  [f,x] in the derivability of s;
end;

definition
  let IT be non empty typestr;
  attr IT is SynTypes_Calculus-like means
  :Def18:
  (for x being type of IT holds <*x*> ==>. x) &
  (for T being FinSequence of IT, x,y being type of IT
  st T^<*y*> ==>. x holds T ==>. x/"y) &
  (for T being FinSequence of IT, x,y being type of IT
  st <*y*>^T ==>. x holds T ==>. y\x) &
  (for T,X,Y being FinSequence of IT, x,y,z being type of IT
  st T ==>. y & X^<*x*>^Y ==>. z holds X^<*x/"y*>^T^Y ==>. z) &
  (for T,X,Y being FinSequence of IT, x,y,z being type of IT
  st T ==>. y & X^<*x*>^Y ==>. z holds X^T^<*y\x*>^Y ==>. z) &
  (for X,Y being FinSequence of IT, x,y,z being type of IT
  st X^<*x*>^<*y*>^Y ==>. z holds X^<*x*y*>^Y ==>.z) &
  for X,Y being FinSequence of IT, x,y being type of IT
  st X ==>. x & Y ==>. y holds X^Y ==>. x*y;
end;

registration
  cluster SynTypes_Calculus-like for non empty typestr;
  existence
  proof
    [:1*,1:] c= [:1*,1:];
    then reconsider DER = [:1*,1:] as non empty Relation of 1*,1;
    reconsider EM = typestr (#1,op2,op2,op2,DER#) as non empty typestr;
    take EM;
A1: for x being type of EM, X being FinSequence of EM holds X ==>. x
    proof
      let x be type of EM, X be FinSequence of EM;
      [X,x] in [:1*,1:];
      hence thesis by Def17;
    end;
    hence for x being type of EM holds <*x*> ==>. x;
    thus thesis by A1;
  end;
end;

definition
  mode SynTypes_Calculus is SynTypes_Calculus-like non empty typestr;
end;

reserve s for SynTypes_Calculus,
  T,X,Y for FinSequence of s,
  x,y,z for type of s;

deffunc e(typestr) = <*>the carrier of $1;

Lm2: T ==>. y & X^<*x*> ==>. z implies X^<*x/"y*>^T ==>. z
proof
  assume that
A1: T ==>. y and
A2: X^<*x*> ==>. z;
  X^<*x*>^e(s) ==>. z by A2,FINSEQ_1:34;
  then X^<*x/"y*>^T^e(s) ==>. z by A1,Def18;
  hence thesis by FINSEQ_1:34;
end;

Lm3: T ==>. y & <*x*>^Y ==>. z implies <*x/"y*>^T^Y ==>. z
proof
  assume that
A1: T ==>. y and
A2: <*x*>^Y ==>. z;
  e(s)^<*x*>^Y ==>. z by A2,FINSEQ_1:34;
  then e(s)^<*x/"y*>^T^Y ==>. z by A1,Def18;
  hence thesis by FINSEQ_1:34;
end;

Lm4: T ==>. y & <*x*> ==>. z implies <*x/"y*>^T ==>. z
proof
  assume that
A1: T ==>. y and
A2: <*x*> ==>. z;
  e(s)^<*x*> ==>. z by A2,FINSEQ_1:34;
  then e(s)^<*x/"y*>^T ==>. z by A1,Lm2;
  hence thesis by FINSEQ_1:34;
end;

Lm5: T ==>. y & X^<*x*> ==>. z implies X^T^<*y\x*> ==>. z
proof
  assume that
A1: T ==>. y and
A2: X^<*x*> ==>. z;
  X^<*x*>^e(s) ==>. z by A2,FINSEQ_1:34;
  then X^T^<*y\x*>^e(s) ==>. z by A1,Def18;
  hence thesis by FINSEQ_1:34;
end;

Lm6: T ==>. y & <*x*>^Y ==>. z implies T^<*y\x*>^Y ==>. z
proof
  assume that
A1: T ==>. y and
A2: <*x*>^Y ==>. z;
  e(s)^<*x*>^Y ==>. z by A2,FINSEQ_1:34;
  then e(s)^T^<*y\x*>^Y ==>. z by A1,Def18;
  hence thesis by FINSEQ_1:34;
end;

Lm7: T ==>. y & <*x*> ==>. z implies T^<*y\x*> ==>. z
proof
  assume that
A1: T ==>. y and
A2: <*x*> ==>. z;
  e(s)^<*x*> ==>. z by A2,FINSEQ_1:34;
  then e(s)^T^<*y\x*> ==>. z by A1,Lm5;
  hence thesis by FINSEQ_1:34;
end;

Lm8: <*x*>^<*y*>^Y ==>. z implies <*x*y*>^Y ==>. z
proof
  assume <*x*>^<*y*>^Y ==>. z;
  then e(s)^<*x*>^<*y*>^Y ==>. z by FINSEQ_1:34;
  then e(s)^<*x*y*>^Y ==>. z by Def18;
  hence thesis by FINSEQ_1:34;
end;

Lm9: X^<*x*>^<*y*> ==>. z implies X^<*x*y*> ==>. z
proof
  assume X^<*x*>^<*y*> ==>. z;
  then X^<*x*>^<*y*>^e(s) ==>. z by FINSEQ_1:34;
  then X^<*x*y*>^e(s) ==>. z by Def18;
  hence thesis by FINSEQ_1:34;
end;

Lm10: <*x*>^<*y*> ==>. z implies <*x*y*> ==>. z
proof
  assume <*x*>^<*y*> ==>. z;
  then e(s)^<*x*>^<*y*> ==>. z by FINSEQ_1:34;
  then e(s)^<*x*y*> ==>. z by Lm9;
  hence thesis by FINSEQ_1:34;
end;

theorem Th12:
  <*x/"y*>^<*y*> ==>. x & <*y*>^<*y\x*> ==>. x
proof
A1: <*x*> ==>. x by Def18;
  <*y*> ==>. y by Def18;
  hence thesis by A1,Lm4,Lm7;
end;

theorem Th13:
  <*x*> ==>. y/"(x\y) & <*x*> ==>. (y/"x)\y
proof
A1: <*y/"x*>^<*x*> ==>. y by Th12;
  <*x*>^<*x\y*> ==>. y by Th12;
  hence thesis by A1,Def18;
end;

theorem Th14:
  <*x/"y*> ==>. (x/"z)/"(y/"z)
proof
A1: <*x/"y*>^<*y*> ==>. x by Th12;
  <*z*> ==>. z by Def18;
  then <*x/"y*>^<*y/"z*>^<*z*> ==>. x by A1,Lm2;
  then <*x/"y*>^<*y/"z*> ==>. x/"z by Def18;
  hence thesis by Def18;
end;

theorem Th15:
  <*y\x*> ==>. (z\y)\(z\x)
proof
A1: <*y*>^<*y\x*> ==>. x by Th12;
  <*z*> ==>. z by Def18;
  then <*z*>^<*z\y*>^<*y\x*> ==>. x by A1,Lm6;
  then <*z*>^(<*z\y*>^<*y\x*>) ==>. x by FINSEQ_1:32;
  then <*z\y*>^<*y\x*> ==>. z\x by Def18;
  hence thesis by Def18;
end;

theorem
  <*x*> ==>. y implies <*x/"z*> ==>. y/"z & <*z\x*> ==>. z\y
proof
  assume
A1: <*x*> ==>. y;
A2: <*z*> ==>. z by Def18;
  then
A3: <*x/"z*>^<*z*> ==>. y by A1,Lm4;
  <*z*>^<*z\x*> ==>. y by A1,A2,Lm7;
  hence thesis by A3,Def18;
end;

theorem Th17:
  <*x*> ==>. y implies <*z/"y*> ==>. z/"x & <*y\z*> ==>. x\z
proof
  assume
A1: <*x*> ==>. y;
A2: <*z*> ==>. z by Def18;
  then
A3: <*z/"y*>^<*x*> ==>. z by A1,Lm4;
  <*x*>^<*y\z*> ==>. z by A1,A2,Lm7;
  hence thesis by A3,Def18;
end;

theorem Th18:
  <*y/"((y/"x)\y)*> ==>. y/"x
proof
  <*x*> ==>. (y/"x)\y by Th13;
  hence thesis by Th17;
end;

theorem Th19:
  <*x*> ==>. y implies
  <*>the carrier of s ==>. y/"x & <*>the carrier of s ==>. x\y
proof
  assume
A1: <*x*> ==>. y;
A2: e(s)^<*x*> = <*x*> by FINSEQ_1:34;
  <*x*>^e(s) = <*x*> by FINSEQ_1:34;
  hence thesis by A1,A2,Def18;
end;

theorem Th20:
  <*>the carrier of s ==>. x/"x & <*>the carrier of s ==>. x\x
proof
  <*x*> ==>. x by Def18;
  hence thesis by Th19;
end;

theorem
  <*>the carrier of s ==>. (y/"(x\y))/"x &
  <*>the carrier of s ==>. x\((y/"x)\ y )
proof
A1: <*x*> ==>. y/"(x\y) by Th13;
  <*x*> ==>. (y/"x)\y by Th13;
  hence thesis by A1,Th19;
end;

theorem
  <*>the carrier of s ==>. ((x/"z)/"(y/"z))/"(x/"y) &
  <*>the carrier of s ==>. (y\x)\((z\y)\(z\x))
proof
A1: <*x/"y*> ==>. (x/"z)/"(y/"z) by Th14;
  <*y\x*> ==>. (z\y)\(z\x) by Th15;
  hence thesis by A1,Th19;
end;

theorem
  <*>the carrier of s ==>. x implies
  <*>the carrier of s ==>. y/"(y/"x) & <*>the carrier of s ==>. (x\y)\y
proof
A1: <*y*> ==>. y by Def18;
  then
A2: e(s)^<*y*> ==>. y by FINSEQ_1:34;
A3: <*y*>^e(s) ==>. y by A1,FINSEQ_1:34;
  assume
A4: e(s) ==>. x;
  then
A5: e(s)^<*y/"x*>^e(s) ==>. y by A2,Lm2;
A6: e(s)^<*x\y*>^e(s) ==>. y by A3,A4,Lm6;
A7: e(s)^<*y/"x*> ==>. y by A5,FINSEQ_1:34;
  <*x\y*>^e(s) ==>. y by A6,FINSEQ_1:34;
  hence thesis by A7,Def18;
end;

theorem
  <*x/"(y/"y)*> ==>. x
proof
  <*x*> ==>. x by Def18;
  then <*x/"(y/"y)*>^e(s) ==>. x by Lm4,Th20;
  hence thesis by FINSEQ_1:34;
end;

definition
  let s,x,y;
  pred x <==>. y means
  :Def19:
  <*x*> ==>. y & <*y*> ==>. x;
  reflexivity by Def18;
  symmetry;
end;

theorem
  x/"y <==>. x/"((x/"y)\x)
proof
A1: <*x/"y*> ==>. x/"((x/"y)\x) by Th13;
  <*x/"((x/"y)\x)*> ==>. x/"y by Th18;
  hence thesis by A1,Def19;
end;

theorem
  x/"(z*y) <==>. (x/"y)/"z
proof
A1: <*z*> ==>. z by Def18;
A2: <*y*> ==>. y by Def18;
A3: <*x*> ==>. x by Def18;
  <*z*>^<*y*> ==>. z*y by A1,A2,Def18;
  then <*x/"(z*y)*>^(<*z*>^<*y*>) ==>. x by A3,Lm4;
  then <*x/"(z*y)*>^<*z*>^<*y*> ==>. x by FINSEQ_1:32;
  then <*x/"(z*y)*>^<*z*> ==>. x/"y by Def18;
  then
A4: <*x/"(z*y)*> ==>. (x/"y)/"z by Def18;
  <*x/"y*>^<*y*> ==>. x by A2,A3,Lm4;
  then <*(x/"y)/"z*>^<*z*>^<*y*> ==>. x by A1,Lm3;
  then <*(x/"y)/"z*>^<*z*y*> ==>. x by Lm9;
  then <*(x/"y)/"z*> ==>. x/"(z*y) by Def18;
  hence thesis by A4,Def19;
end;

theorem
  <*x*(y/"z)*> ==>. (x*y)/"z :: and analogously <*z\y*x*> > z\(y*x)
proof
A1: <*x*> ==>. x by Def18;
  <*y*> ==>. y by Def18; then
A2: <*x*>^<*y*> ==>. x*y by A1,Def18;
  <*z*> ==>. z by Def18;
  then <*x*>^<*y/"z*>^<*z*> ==>. x*y by A2,Lm2;
  then <*x*(y/"z)*>^<*z*> ==>. x*y by Lm8;
  hence thesis by Def18;
end;

theorem
  <*x*> ==>. (x*y)/"y & <*x*> ==>. y\(y*x)
proof
A1: <*x*> ==>.x by Def18;
A2: <*y*> ==>.y by Def18;
  then
A3: <*x*>^<*y*> ==>. x*y by A1,Def18;
  <*y*>^<*x*> ==>. y*x by A1,A2,Def18;
  hence thesis by A3,Def18;
end;

theorem
  x*y*z <==>. x*(y*z)
proof
A1: <*x*> ==>. x by Def18;
A2: <*y*> ==>. y by Def18;
A3: <*z*> ==>. z by Def18;
  <*x*>^<*y*> ==>. x*y by A1,A2,Def18;
  then <*x*>^<*y*>^<*z*> ==>. (x*y)*z by A3,Def18;
  then <*x*>^<*y*z*> ==>. (x*y)*z by Lm9;
  then
A4: <*x*(y*z)*> ==>. (x*y)*z by Lm10;
  <*y*>^<*z*> ==>. y*z by A2,A3,Def18;
  then <*x*>^(<*y*>^<*z*>) ==>. x*(y*z) by A1,Def18;
  then <*x*>^<*y*>^<*z*> ==>. x*(y*z) by FINSEQ_1:32;
  then <*x*y*>^<*z*> ==>. x*(y*z) by Lm8;
  then <*x*y*z*> ==>. x*(y*z) by Lm10;
  hence thesis by A4,Def19;
end;