:: by Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec and Pauline N. Kawamoto

::

:: Received November 17, 1994

:: Copyright (c) 1994-2021 Association of Mizar Users

scheme :: PRE_CIRC:sch 2

MSSLambda2Part{ F_{1}() -> set , P_{1}[ object ], F_{2}( object ) -> object , F_{3}( object ) -> object } :

MSSLambda2Part{ F

ex f being ManySortedSet of F_{1}() st

for i being Element of F_{1}() st i in F_{1}() holds

( ( P_{1}[i] implies f . i = F_{2}(i) ) & ( P_{1}[i] implies f . i = F_{3}(i) ) )

for i being Element of F

( ( P

proof end;

registration

let I be set ;

existence

ex b_{1} being ManySortedSet of I st

( b_{1} is V2() & b_{1} is V44() )

end;
existence

ex b

( b

proof end;

registration

let I be set ;

let M be ManySortedSet of I;

let A be Subset of I;

coherence

for b_{1} being A -defined Function st b_{1} = M | A holds

b_{1} is total

end;
let M be ManySortedSet of I;

let A be Subset of I;

coherence

for b

b

proof end;

registration
end;

registration
end;

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

for A being set

for B being V2() ManySortedSet of I

for F being ManySortedFunction of I --> A,B holds dom (commute F) = A

proof end;

scheme :: PRE_CIRC:sch 3

LambdaRecCorrD{ F_{1}() -> non empty set , F_{2}() -> Element of F_{1}(), F_{3}( Nat, Element of F_{1}()) -> Element of F_{1}() } :

LambdaRecCorrD{ F

( ex f being sequence of F_{1}() st

( f . 0 = F_{2}() & ( for i being Nat holds f . (i + 1) = F_{3}(i,(f . i)) ) ) & ( for f1, f2 being sequence of F_{1}() st f1 . 0 = F_{2}() & ( for i being Nat holds f1 . (i + 1) = F_{3}(i,(f1 . i)) ) & f2 . 0 = F_{2}() & ( for i being Nat holds f2 . (i + 1) = F_{3}(i,(f2 . i)) ) holds

f1 = f2 ) )

( f . 0 = F

f1 = f2 ) )

proof end;

scheme :: PRE_CIRC:sch 4

LambdaMSFD{ F_{1}() -> non empty set , F_{2}() -> Subset of F_{1}(), F_{3}() -> ManySortedSet of F_{2}(), F_{4}() -> ManySortedSet of F_{2}(), F_{5}( object ) -> set } :

LambdaMSFD{ F

ex f being ManySortedFunction of F_{3}(),F_{4}() st

for i being Element of F_{1}() st i in F_{2}() holds

f . i = F_{5}(i)

providedfor i being Element of F

f . i = F

A1:
for i being Element of F_{1}() st i in F_{2}() holds

F_{5}(i) is Function of (F_{3}() . i),(F_{4}() . i)

F

proof end;

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 & ( for x being set st x in dom g holds

g . x in f . x ) holds

s +* g is Element of product f

for f being V2() ManySortedSet of I

for g being Function

for 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

proof end;

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 & c in C )

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 & c in C )

proof end;

registration

let D be non empty set ;

coherence

for b_{1} being Element of FinTrees D holds b_{1} is finite

end;
coherence

for b

proof end;

registration
end;

theorem Th8: :: 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

for p being Element of T holds T | p, { t where t is Element of T : p is_a_prefix_of t } are_equipotent

proof end;

registration

let T be finite DecoratedTree-like Function;

let t be Element of dom T;

let T1 be finite DecoratedTree;

coherence

T with-replacement (t,T1) is finite

end;
let t be Element of dom T;

let T1 be finite DecoratedTree;

coherence

T with-replacement (t,T1) is finite

proof end;

theorem Th9: :: 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 }

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 }

proof end;

theorem Th10: :: 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) & p is_a_prefix_of f holds

ex t1 being Element of T1 st f = p ^ t1

for p being Element of T

for f being FinSequence of NAT st f in T with-replacement (p,T1) & p is_a_prefix_of f holds

ex t1 being Element of T1 st f = p ^ t1

proof end;

theorem Th11: :: 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)

for k being Element of NAT st k + 1 in dom p holds

(tree p) | <*k*> = p . (k + 1)

proof end;

theorem :: PRE_CIRC:13

for q being DTree-yielding FinSequence

for k being Nat st k + 1 in dom q holds

<*k*> in tree (doms q)

for k being Nat st k + 1 in dom q holds

<*k*> in tree (doms q)

proof end;

theorem Th13: :: PRE_CIRC:14

for p, q being Tree-yielding FinSequence

for 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 ) holds

for t being Tree st q . (k + 1) = t holds

tree q = (tree p) with-replacement (<*k*>,t)

for 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 ) holds

for t being Tree st q . (k + 1) = t holds

tree q = (tree p) with-replacement (<*k*>,t)

proof end;

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 & e1 = x -tree p holds

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 ) )

for x being set

for k being Element of NAT

for p being DTree-yielding FinSequence st <*k*> in dom e1 & e1 = x -tree p holds

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 ) )

proof end;

theorem Th16: :: 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)

for p being Element of T holds (card (T with-replacement (p,T1))) + (card (T | p)) = (card T) + (card T1)

proof end;

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)

for p being Element of dom T holds (card (T with-replacement (p,T1))) + (card (T | p)) = (card T) + (card T1)

proof end;

registration
end;

:: from AMISTD_2

:: from AMISTD_2, 2006.03.26, A.T.

:: from SCMPDS_9. 2008.05.06, A.T.

theorem Th23: :: PRE_CIRC:24

for D being finite set

for k being Nat st card D = k + 1 holds

ex x being Element of D ex C being Subset of D st

( D = C \/ {x} & card C = k )

for k being Nat st card D = k + 1 holds

ex x being Element of D ex C being Subset of D st

( D = C \/ {x} & card C = k )

proof end;

:: Many Sorted Sets and Functions

::---------------------------------------------------------------------------

::$CT