:: PRE_CIRC semantic presentation

scheme :: PRE_CIRC:sch 1
FraenkelFinIm{ F₁() -> non empty finite set , F₂( set ) -> set , P₁[ set ] } :

{ F₂(x) where x is Element of F₁() : P₁[x] } is finite

proof end;

theorem :: PRE_CIRC:1

canceled;

theorem :: PRE_CIRC:2

for f being Function
for x, y being set st dom f = {x} & rng f = {y} holds
f = {[x,y]}

proof end;

theorem Th3: :: PRE_CIRC:3

for f, g, h being Function st f c= g holds
f +* h c= g +* h

proof end;

theorem :: PRE_CIRC:4

for f, g, h being Function st f c= g & dom f misses dom h holds
f c= g +* h

proof end;

registration

cluster non empty finite natural-membered set ;
existence

proof end;

end;

notation

let A be non empty finite real-membered set ;
synonym max A for upper_bound A;

end;

definition

let A be non empty finite real-membered set ;
:: original: max
redefine func max A -> real number means :Def1: :: PRE_CIRC:def 1
( it in A & ( for k being real number st k in A holds
k <= it ) );
compatibility

proof end;

coherence ;

end;

:: deftheorem Def1 defines max PRE_CIRC:def 1 :

registration

let X be non empty finite natural-membered set ;
cluster max X -> natural ;
coherence

proof end;

end;

theorem :: PRE_CIRC:5

for I being set
for MSS being ManySortedSet of I holds (MSS # ) . (<*> I) = {{} }

proof end;

scheme :: PRE_CIRC:sch 2
MSSLambda2Part{ F₁() -> set , P₁[ set ], F₂( set ) -> set , F₃( set ) -> set } :

ex f being ManySortedSet of F₁() st
for i being Element of F₁() st i in F₁() holds
( ( P₁[i] implies f . i = F₂(i) ) & ( P₁[i] implies f . i = F₃(i) ) )

proof end;

definition

let I be set ;
let IT be ManySortedSet of I;
canceled;
attr IT is locally-finite means :: PRE_CIRC:def 3
for i being set st i in I holds
IT . i is finite;

end;

:: deftheorem PRE_CIRC:def 2 :

:: deftheorem defines locally-finite PRE_CIRC:def 3 :

registration

let I be set ;
cluster V2 locally-finite ManySortedSet of I;
existence

proof end;

end;

definition

let I, A be set ;
:: original: -->
redefine func I --> A -> ManySortedSet of I;
coherence

proof end;

end;

definition

let I be set ;
let M be ManySortedSet of I;
let A be Subset of I;
:: original: |
redefine func M | A -> ManySortedSet of A;
coherence

proof end;

end;

registration

let M be non-empty Function;
let A be set ;
cluster M | A -> non-empty ;
coherence

proof end;

end;

theorem Th6: :: PRE_CIRC:6

for I being non empty set
for B being V2 ManySortedSet of I holds not union (rng B) is empty

proof end;

theorem Th7: :: PRE_CIRC:7

for I being set holds uncurry (I --> {} ) = {}

proof end;

theorem :: PRE_CIRC:8

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

proof end;

scheme :: PRE_CIRC:sch 3
LambdaRecCorrD{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃( Nat, Element of F₁()) -> Element of F₁() } :

( ex f being Function of NAT ,F₁() st
( f . 0 = F₂() & ( for i being Nat holds f . (i + 1) = F₃(i,(f . i)) ) ) & ( for f1, f2 being Function of NAT ,F₁() st f1 . 0 = F₂() & ( for i being Nat holds f1 . (i + 1) = F₃(i,(f1 . i)) ) & f2 . 0 = F₂() & ( for i being Nat holds f2 . (i + 1) = F₃(i,(f2 . i)) ) holds
f1 = f2 ) )

proof end;

scheme :: PRE_CIRC:sch 4
LambdaMSFD{ F₁() -> non empty set , F₂() -> Subset of F₁(), F₃() -> ManySortedSet of F₂(), F₄() -> ManySortedSet of F₂(), F₅( set ) -> set } :

ex f being ManySortedFunction of F₃(),F₄() st
for i being Element of F₁() st i in F₂() holds
f . i = F₅(i)

provided

A1: for i being Element of F₁() st i in F₂() holds
F₅(i) is Function of F₃() . i,F₄() . i

proof end;

registration

let F be non-empty Function;
let f be Function;
cluster f * F -> non-empty ;
coherence

proof end;

end;

theorem :: PRE_CIRC:9

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

proof end;

theorem :: PRE_CIRC:10

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 )

proof end;

theorem :: PRE_CIRC:11

for I being set
for M being ManySortedSet of I
for x, g being Function st x in product M holds
x * g in product (M * g)

proof end;

theorem :: PRE_CIRC:12

for n being Nat
for a being set holds product (n |-> {a}) = {(n |-> a)}

proof end;

registration

let D be non empty set ;
cluster -> finite Element of FinTrees D;
coherence

proof end;

end;

registration

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

proof end;

end;

theorem Th13: :: PRE_CIRC:13

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

proof end;

registration

let T be finite DecoratedTree;
let t be Element of dom T;
let T1 be finite DecoratedTree;
cluster T with-replacement t,T1 -> finite ;
coherence

proof end;

end;

theorem Th14: :: PRE_CIRC:14

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 }

proof end;

theorem Th15: :: PRE_CIRC:15

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

proof end;

theorem Th16: :: PRE_CIRC:16

for p being Tree-yielding FinSequence
for k being Nat st k + 1 in dom p holds
(tree p) | <*k*> = p . (k + 1)

proof end;

theorem :: PRE_CIRC:17

for q being DTree-yielding FinSequence
for k being Nat st k + 1 in dom q holds
<*k*> in tree (doms q)

proof end;

theorem Th18: :: PRE_CIRC:18

for p, q being Tree-yielding FinSequence
for k being 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:19

for e1, e2 being finite DecoratedTree
for x being set
for k being 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 :: PRE_CIRC:20