:: Preliminaries to Circuits, I
:: by Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec and Pauline N. Kawamoto
::
:: Received November 17, 1994
:: Copyright (c) 1994-2012 Association of Mizar Users


begin

scheme :: PRE_CIRC:sch 1
FraenkelFinIm{ F1() ->  non empty finite set , F2( set ) ->  set , P1[ set ] } :
  {  F2(x) where x is Element of F1() : P1[x]  }  is finite
proofend;

theorem :: PRE_CIRC:1
for f being Function
for x, y being set st dom f = {x} & rng f = {y} holds
f = {[x,y]}
proofend;

begin

::---------------------------------------------------------------------------
:: Many Sorted Sets and Functions
::---------------------------------------------------------------------------
theorem :: PRE_CIRC:2
for I being set
for MSS being ManySortedSet of I holds (MSS #) . (<*> I) = {{}}
proofend;

scheme :: PRE_CIRC:sch 2
MSSLambda2Part{ F1() ->  set , P1[ set ], F2( set ) ->  set , F3( set ) ->  set } :
 ex f being ManySortedSet of F1() st
for i being Element of F1() st i in F1() holds
( ( P1[i] implies f . i = F2(i) ) &amp; ( P1[i] implies f . i = F3(i) ) )
proofend;

registration
let I be set ;
cluster Relation-like V2() I -defined Function-like total V41() for set ;
existence
 ex b1 being ManySortedSet of I st
( b1 is V2() &amp; b1 is V41() )
proofend;
end;

registration
let I be set ;
let M be ManySortedSet of I;
let A be Subset of I;
clusterM | A -> A -defined total for A -defined Function;
coherence
 for b1 being A -defined Function st b1 = M | A holds
b1 is total
proofend;
end;

registration
let I be set ;
let M be ManySortedSet of I;
let A be Subset of I;
clusterM | A ->  total ;
coherence
 M | A is total ;
end;

registration
let M be non-empty Function;
let A be set ;
clusterM | A ->  non-empty ;
coherence
 M | A is non-empty
proofend;
end;

theorem Th3: :: PRE_CIRC:3
for I being non empty set
for B being V2() ManySortedSet of I holds not union (rng B) is empty
proofend;

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

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

scheme :: PRE_CIRC:sch 3
LambdaRecCorrD{ F1() ->  non empty set , F2() ->  Element of F1(), F3( Nat, Element of F1()) ->  Element of F1() } :
 ( ex f being Function of NAT,F1() st
( f . 0 = F2() &amp; ( for i being Nat holds f . (i + 1) = F3(i,(f . i)) ) ) &amp; ( for f1, f2 being Function of NAT,F1() st f1 . 0 = F2() &amp; ( for i being Nat holds f1 . (i + 1) = F3(i,(f1 . i)) ) &amp; f2 . 0 = F2() &amp; ( for i being Nat holds f2 . (i + 1) = F3(i,(f2 . i)) ) holds
f1 = f2 ) )
proofend;

scheme :: PRE_CIRC:sch 4
LambdaMSFD{ F1() ->  non empty set , F2() ->  Subset of F1(), F3() ->  ManySortedSet of F2(), F4() ->  ManySortedSet of F2(), F5( set ) ->  set } :
 ex f being ManySortedFunction of F3(),F4() st
for i being Element of F1() st i in F2() holds
f . i = F5(i)
provided
A1: for i being Element of F1() st i in F2() holds
F5(i) is Function of (F3() . i),(F4() . i)
proofend;

theorem :: PRE_CIRC:6
for I being set
for f being V2() ManySortedSet of I
for g being Function
for s being Element of product f st dom g c= dom f &amp; ( for x being set st x in dom g holds
g . x in f . x ) holds
s +* g is Element of product f
proofend;

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

theorem :: PRE_CIRC:8
for n being Element of NAT
for a being set holds product (n |-> {a}) = {(n |-> a)}
proofend;

begin

registration
let D be non empty set ;
cluster  ->  finite for Element of FinTrees D;
coherence
 for b1 being Element of FinTrees D holds b1 is finite
proofend;
end;

registration
let T be finite DecoratedTree;
let t be Element of dom T;
clusterT | t ->  finite ;
coherence
 T | t is finite
proofend;
end;

theorem Th9: :: PRE_CIRC:9
for T being finite Tree
for p being Element of T holds T | p, {  t where t is Element of T : p is_a_prefix_of t  }  are_equipotent
proofend;

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

theorem Th10: :: PRE_CIRC:10
for T, T1 being finite Tree
for p being Element of T holds T with-replacement (p,T1) =  {  t where t is Element of T : not p is_a_prefix_of t  }  \/  {  (p ^ t1) where t1 is Element of T1 : verum  }
proofend;

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

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

theorem :: PRE_CIRC:13
for q being DTree-yielding FinSequence
for k being Element of NAT st k + 1 in dom q holds
<*k*> in tree (doms q)
proofend;

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

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

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

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

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

registration
let x be set ;
cluster root-tree x ->  finite ;
coherence
 root-tree x is finite
proofend;
end;

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

begin

:: from AMISTD_2
theorem :: PRE_CIRC:20
for F being non empty finite set holds (card F) - 1 = (card F) -' 1
proofend;

:: 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 )
proofend;

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

:: from SCMPDS_9. 2008.05.06, A.T.
theorem :: PRE_CIRC:23
for n being Nat holds  {  k where k is Element of NAT : k > n  }  is infinite
proofend;