:: PRE_CIRC semantic presentation

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

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

proof end;

theorem Th1: :: PRE_CIRC:1

canceled;

theorem Th2: :: PRE_CIRC:2

for b₁ being Function
for b₂, b₃ being set st dom b₁ = {b₂} & rng b₁ = {b₃} holds
b₁ = {[b₂,b₃]}

proof end;

theorem Th3: :: PRE_CIRC:3

for b₁, b₂, b₃ being Function st b₁ c= b₂ holds
b₁ +* b₃ c= b₂ +* b₃

proof end;

theorem Th4: :: PRE_CIRC:4

for b₁, b₂, b₃ being Function st b₁ c= b₂ & dom b₁ misses dom b₃ holds
b₁ c= b₂ +* b₃

proof end;

registration

cluster non empty finite natural-membered set ;
existence

proof end;

end;

notation

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

end;

definition

let c₁ be non empty finite real-membered set ;
redefine func max as max c₁ -> real number means :Def1: :: PRE_CIRC:def 1
( a₂ in a₁ & ( for b₁ being real number st b₁ in a₁ holds
b₁ <= a₂ ) );
compatibility

proof end;

coherence ;

end;

:: deftheorem Def1 defines max PRE_CIRC:def 1 :

registration

let c₁ be non empty finite natural-membered set ;
cluster max a₁ -> natural ;
coherence

proof end;

end;

theorem Th5: :: PRE_CIRC:5

for b₁ being set
for b₂ being ManySortedSet of b₁ holds (b₂ # ) . (<*> b₁) = {{} }

proof end;

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

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

proof end;

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
canceled;
attr a₂ is locally-finite means :: PRE_CIRC:def 3
for b₁ being set st b₁ in a₁ holds
a₂ . b₁ is finite;

end;

:: deftheorem Def2 PRE_CIRC:def 2 :

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

registration

let c₁ be set ;
cluster V2 locally-finite ManySortedSet of a₁;
existence

proof end;

end;

definition

let c₁, c₂ be set ;
redefine func --> as c₁ --> c₂ -> ManySortedSet of a₁;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
let c₃ be Subset of c₁;
redefine func | as c₂ | c₃ -> ManySortedSet of a₃;
coherence

proof end;

end;

registration

let c₁ be non-empty Function;
let c₂ be set ;
cluster a₁ | a₂ -> non-empty ;
coherence

proof end;

end;

theorem Th6: :: PRE_CIRC:6

for b₁ being non empty set
for b₂ being V2 ManySortedSet of b₁ holds not union (rng b₂) is empty

proof end;

theorem Th7: :: PRE_CIRC:7

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

proof end;

theorem Th8: :: PRE_CIRC:8

for b₁ being non empty set
for b₂ being set
for b₃ being V2 ManySortedSet of b₁
for b₄ being ManySortedFunction of b₁ --> b₂,b₃ holds dom (commute b₄) = b₂

proof end;

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

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

proof end;

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

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

provided

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

proof end;

registration

let c₁ be non-empty Function;
let c₂ be Function;
cluster a₂ * a₁ -> non-empty ;
coherence

proof end;

end;

theorem Th9: :: PRE_CIRC:9

for b₁ being set
for b₂ being V2 ManySortedSet of b₁
for b₃ being Function
for b₄ being Element of product b₂ st dom b₃ c= dom b₂ & ( for b₅ being set st b₅ in dom b₃ holds
b₃ . b₅ in b₂ . b₅ ) holds
b₄ +* b₃ is Element of product b₂

proof end;

theorem Th10: :: PRE_CIRC:10

for b₁, b₂ being non empty set
for b₃ being V2 ManySortedSet of b₁
for b₄ being ManySortedFunction of b₁ --> b₂,b₃
for b₅ being Element of b₂ ex b₆ being ManySortedSet of b₁ st
( b₆ = (commute b₄) . b₅ & b₆ in b₃ )

proof end;

theorem Th11: :: PRE_CIRC:11

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃, b₄ being Function st b₃ in product b₂ holds
b₃ * b₄ in product (b₂ * b₄)

proof end;

theorem Th12: :: PRE_CIRC:12

for b₁ being Nat
for b₂ being set holds product (b₁ |-> {b₂}) = {(b₁ |-> b₂)}

proof end;

registration

let c₁ be non empty set ;
cluster -> finite Element of FinTrees a₁;
coherence

proof end;

end;

registration

let c₁ be finite DecoratedTree;
let c₂ be Element of dom c₁;
cluster a₁ | a₂ -> finite ;
coherence

proof end;

end;

theorem Th13: :: PRE_CIRC:13

for b₁ being finite Tree
for b₂ being Element of b₁ holds b₁ | b₂,{ b₃ where B is Element of b₁ : b₂ is_a_prefix_of b₃ } are_equipotent

proof end;

registration

let c₁ be finite DecoratedTree;
let c₂ be Element of dom c₁;
let c₃ be finite DecoratedTree;
cluster a₁ with-replacement a₂,a₃ -> finite ;
coherence

proof end;

end;

theorem Th14: :: PRE_CIRC:14

for b₁, b₂ being finite Tree
for b₃ being Element of b₁ holds b₁ with-replacement b₃,b₂ = { b₄ where B is Element of b₁ : not b₃ is_a_prefix_of b₄ } \/ { (b₃ ^ b₄) where B is Element of b₂ : verum }

proof end;

theorem Th15: :: PRE_CIRC:15

for b₁, b₂ being finite Tree
for b₃ being Element of b₁
for b₄ being FinSequence of NAT st b₄ in b₁ with-replacement b₃,b₂ & b₃ is_a_prefix_of b₄ holds
ex b₅ being Element of b₂ st b₄ = b₃ ^ b₅

proof end;

theorem Th16: :: PRE_CIRC:16

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

proof end;

theorem Th17: :: PRE_CIRC:17

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

proof end;

theorem Th18: :: PRE_CIRC:18

for b₁, b₂ being Tree-yielding FinSequence
for b₃ being Nat st len b₁ = len b₂ & b₃ + 1 in dom b₁ & ( for b₄ being Nat st b₄ in dom b₁ & b₄ <> b₃ + 1 holds
b₁ . b₄ = b₂ . b₄ ) holds
for b₄ being Tree st b₂ . (b₃ + 1) = b₄ holds
tree b₂ = (tree b₁) with-replacement <*b₃*>,b₄

proof end;

theorem Th19: :: PRE_CIRC:19

for b₁, b₂ being finite DecoratedTree
for b₃ being set
for b₄ being Nat
for b₅ being DTree-yielding FinSequence st <*b₄*> in dom b₁ & b₁ = b₃ -tree b₅ holds
ex b₆ being DTree-yielding FinSequence st
( b₁ with-replacement <*b₄*>,b₂ = b₃ -tree b₆ & len b₆ = len b₅ & b₆ . (b₄ + 1) = b₂ & ( for b₇ being Nat st b₇ in dom b₅ & b₇ <> b₄ + 1 holds
b₆ . b₇ = b₅ . b₇ ) )

proof end;

theorem Th20: :: PRE_CIRC:20

for b₁ being finite Tree
for b₂ being Element of b₁ st b₂ <> {} holds
card (b₁ | b₂) < card b₁

proof end;

theorem Th21: :: PRE_CIRC:21

for b₁ being Function holds Card b₁ = Card (dom b₁)

proof end;

theorem Th22: :: PRE_CIRC:22

for b₁, b₂ being finite Tree
for b₃ being Element of b₁ holds (card (b₁ with-replacement b₃,b₂)) + (card (b₁ | b₃)) = (card b₁) + (card b₂)

proof end;

theorem Th23: :: PRE_CIRC:23

for b₁, b₂ being finite DecoratedTree
for b₃ being Element of dom b₁ holds (card (b₁ with-replacement b₃,b₂)) + (card (b₁ | b₃)) = (card b₁) + (card b₂)

proof end;

registration

let c₁ be set ;
cluster root-tree a₁ -> finite ;
coherence

proof end;

end;

theorem Th24: :: PRE_CIRC:24

for b₁ being set holds card (root-tree b₁) = 1

proof end;