:: Preliminaries to Circuits, I
::  by Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec and Pauline N. Kawamoto
::
:: Received November 17, 1994
:: Copyright (c) 1994-2021 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 NUMBERS, FINSET_1, XBOOLE_0, SUBSET_1, TARSKI, FUNCT_1, RELAT_1,
      FUNCOP_1, FUNCT_4, PBOOLE, FINSEQ_1, CARD_3, PARTFUN1, FUNCT_5, FUNCT_2,
      ZFMISC_1, FUNCT_6, NAT_1, CARD_1, ARYTM_3, MCART_1, FINSEQ_2, TREES_1,
      TREES_3, TREES_2, ORDINAL4, TREES_A, XXREAL_0, TREES_4, ARYTM_1, REAL_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, XREAL_0, XTUPLE_0,
      MCART_1, CARD_1, RELAT_1, FUNCT_1, FINSET_1, PARTFUN1, FUNCT_2, ORDINAL1,
      NUMBERS, XXREAL_0, XXREAL_2, BINOP_1, FUNCOP_1, FUNCT_4, FUNCT_7, CARD_3,
      TREES_2, TREES_1, TREES_3, TREES_4, FUNCT_5, FUNCT_6, PBOOLE, FINSEQ_1,
      FINSEQ_2, NAT_1, NAT_D;
 constructors WELLORD2, BINOP_1, FUNCT_4, SETWISEO, XXREAL_0, NAT_1, FUNCT_5,
      CARD_3, SEQ_4, PBOOLE, TREES_4, BINARITH, INT_1, XXREAL_2, PARTFUN1,
      RELSET_1, FUNCT_7, XTUPLE_0, NAT_D;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
      FINSET_1, XREAL_0, MEMBERED, FINSEQ_1, CARD_3, PBOOLE, TREES_2, TREES_3,
      XXREAL_2, CARD_1, RELSET_1, TREES_1, XTUPLE_0, NAT_1;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin

scheme :: PRE_CIRC:sch 1
  FraenkelFinIm{ A() -> finite non empty set, F(set) -> set, P[set] }: { F(x)
  where x is Element of A() : P[x] } is finite;

begin

::---------------------------------------------------------------------------
:: Many Sorted Sets and Functions
::---------------------------------------------------------------------------

::$CT

theorem :: PRE_CIRC:2
  for I being set, MSS being ManySortedSet of I holds MSS#.<*>I = {{}};

reserve i,j,x,y for object,
  f,g for Function;

scheme :: PRE_CIRC:sch 2
  MSSLambda2Part { I() -> set, P [object], F, G (object) -> object }:
  ex f being
  ManySortedSet of I() st for i being Element of I() st i in I() holds (P[i]
  implies f.i = F(i)) & (not P[i] implies f.i = G(i));

registration
  let I be set;
  cluster non-empty finite-yielding for ManySortedSet of I;
end;

registration
  let I be set, M be ManySortedSet of I, A be Subset of I;
  cluster M | A -> total for A-defined Function;
end;

registration
  let I be set, M be ManySortedSet of I, A be Subset of I;
  cluster M | A -> total;
end;

registration
  let M be non-empty Function, A be set;
  cluster M | A -> non-empty;
end;

theorem :: PRE_CIRC:3
  for I being non empty set, B being non-empty ManySortedSet of I
  holds union rng B is non empty;

theorem :: PRE_CIRC:4
  for I being set holds uncurry (I --> {}) = {};

theorem :: PRE_CIRC:5
  for I being non empty set, A being set, B being non-empty
ManySortedSet of I, F being ManySortedFunction of (I --> A qua total I-defined
  Function), B holds dom commute F = A;

scheme :: PRE_CIRC:sch 3
  LambdaRecCorrD {D() -> non empty set, A() -> Element of D(), F(Nat, Element
  of D()) -> Element of D() } : (ex f being sequence of  D() st f.0 = A() &
for i being Nat holds f.(i+1) = F(i, f.i)) & for f1, f2 being sequence of
D() st (f1.0 = A() & for i being Nat holds f1.(i+1) = F(i, f1.i)) & (f2.0 = A()
  & for i being Nat holds f2.(i+1) = F(i,f2.i)) holds f1 = f2;

scheme :: PRE_CIRC:sch 4
  LambdaMSFD{J() -> non empty set, I() -> Subset of J(), A, B() ->
ManySortedSet of I(), F(object) -> set } :
ex f being ManySortedFunction of A(), B
  () st for i being Element of J() st i in I() holds f.i = F(i)
provided
 for i being Element of J() st i in I() holds F(i) is Function of A()
.i, B().i;

theorem :: PRE_CIRC:6
  for I being set, f being non-empty ManySortedSet of I, g being
Function , s being Element of product f st dom g c= dom f & for x being set st
  x in dom g holds g.x in f.x holds s+*g is Element of product f;

theorem :: PRE_CIRC:7
  for A, B being non empty set, C being non-empty ManySortedSet of A,
  InpFs being ManySortedFunction of A --> B, C, b being Element of B ex c being
  ManySortedSet of A st c = (commute InpFs).b & c in C;

theorem :: PRE_CIRC:8
  for n being Nat, a being set holds product ( n |-> {a} ) =
  { n |-> a };

begin

::---------------------------------------------------------------------------
:: Trees
::---------------------------------------------------------------------------

reserve T,T1 for finite Tree,
  t,p for Element of T,
  t1 for Element of T1;

registration
  let D be non empty set;
  cluster -> finite for Element of FinTrees D;
end;

registration
  let T be finite DecoratedTree;
  let t be Element of dom T;
  cluster T|t -> finite;
end;

theorem :: PRE_CIRC:9
  T|p,{ t : p is_a_prefix_of t } are_equipotent;

registration
  let T be finite DecoratedTree-like Function;
  let t be Element of dom T;
  let T1 be finite DecoratedTree;
  cluster T with-replacement (t,T1) -> finite;
end;

theorem :: PRE_CIRC:10
  T with-replacement (p,T1) = { t : not p is_a_prefix_of t } \/ the set of all
  p^t1;

theorem :: PRE_CIRC:11
  for f being FinSequence of NAT st f in T with-replacement (p,T1)
  & p is_a_prefix_of f ex t1 st f = p^t1;

theorem :: PRE_CIRC:12
  for p being Tree-yielding FinSequence, k being Element of NAT st
  k+1 in dom p holds (tree p)|<*k*> = p.(k+1);

theorem :: PRE_CIRC:13
  for q being DTree-yielding FinSequence, k being Nat st k+1
  in dom q holds <*k*> in tree doms q;

theorem :: PRE_CIRC:14
  for p,q being Tree-yielding FinSequence, k being Element of NAT
st len p = len q & k+1 in dom p & for i being Nat st i in dom p & i
<> k+1 holds p.i = q.i for t being Tree st q.(k+1) = t holds tree(q) = tree(p)
  with-replacement (<*k*>, t);

theorem :: PRE_CIRC:15
  for e1,e2 being finite DecoratedTree, x being set, k being Element of
NAT, p being DTree-yielding FinSequence st <*k*> in dom e1 & e1 = x-tree p ex q
being DTree-yielding FinSequence st e1 with-replacement (<*k*>,e2) = x-tree q &
len q = len p & q.(k+1) = e2 & for i being Nat st i in dom p & i <>
  k+1 holds q.i = p.i;

theorem :: PRE_CIRC:16
  for T being finite Tree, p being Element of T st p <> {} holds card (T
  |p) < card T;

theorem :: PRE_CIRC:17
  for T, T1 being finite Tree, p being Element of T holds card(T
  with-replacement (p,T1)) + card (T|p) = card T + card T1;

theorem :: PRE_CIRC:18
  for T, T1 being finite DecoratedTree, p being Element of dom T holds
  card(T with-replacement (p,T1)) + card (T|p) = card T + card T1;

registration
  let x be object;
  cluster root-tree x -> finite;
end;

theorem :: PRE_CIRC:19
  for x being set holds card root-tree x = 1;

begin :: Addenda
:: from AMISTD_2

theorem :: PRE_CIRC:20
  for F being non empty finite set holds card F - 1 = card F -' 1;

:: from AMISTD_2, 2006.03.26, A.T.

theorem :: PRE_CIRC:21
  for f, g being Function holds dom f,dom g are_equipotent iff f,g
  are_equipotent;

theorem :: PRE_CIRC:22
  for f, g being finite Function st dom f misses dom g holds card (f +*
  g) = card f + card g;

:: from SCMPDS_9. 2008.05.06, A.T.

theorem :: PRE_CIRC:23
  for n being Nat holds
  {k where k is Nat: k > n} is infinite;

theorem :: PRE_CIRC:24
  for D being finite set, k being Nat st card D = k+1
  ex x being Element of D,C being Subset of D st D = C \/ { x } & card C = k;

theorem :: PRE_CIRC:25
  for D being finite set st card D = 1 holds ex x being Element of D st D={x};

reserve k for Nat;

scheme :: PRE_CIRC:sch 5
  MinValue { D() -> non empty finite set, F(Element of D())-> Real}:
    ex x being Element of D() st for y being Element of D() holds F(x) <= F(y);