:: ALGSEQ_1 semantic presentation

definition

let c₁ be Nat;
func PSeg c₁ -> set equals :: ALGSEQ_1:def 1
{ b₁ where B is Nat : b₁ < a₁ } ;
coherence ;

end;

:: deftheorem Def1 defines PSeg ALGSEQ_1:def 1 :

definition

let c₁ be Nat;
redefine func PSeg as PSeg c₁ -> Subset of NAT ;
coherence

proof end;

end;

Lemma1: for b₁ being Nat
for b₂ being set st b₂ in PSeg b₁ holds
b₂ is Nat
;

theorem Th1: :: ALGSEQ_1:1

canceled;

theorem Th2: :: ALGSEQ_1:2

canceled;

theorem Th3: :: ALGSEQ_1:3

canceled;

theorem Th4: :: ALGSEQ_1:4

canceled;

theorem Th5: :: ALGSEQ_1:5

canceled;

theorem Th6: :: ALGSEQ_1:6

canceled;

theorem Th7: :: ALGSEQ_1:7

canceled;

theorem Th8: :: ALGSEQ_1:8

canceled;

theorem Th9: :: ALGSEQ_1:9

canceled;

theorem Th10: :: ALGSEQ_1:10

for b₁, b₂ being Nat holds
( b₁ in PSeg b₂ iff b₁ < b₂ )

proof end;

theorem Th11: :: ALGSEQ_1:11

( PSeg 0 = {} & PSeg 1 = {0} & PSeg 2 = {0,1} )

proof end;

theorem Th12: :: ALGSEQ_1:12

for b₁ being Nat holds b₁ in PSeg (b₁ + 1)

proof end;

theorem Th13: :: ALGSEQ_1:13

for b₁, b₂ being Nat holds
( b₁ <= b₂ iff PSeg b₁ c= PSeg b₂ )

proof end;

theorem Th14: :: ALGSEQ_1:14

for b₁, b₂ being Nat st PSeg b₁ = PSeg b₂ holds
b₁ = b₂

proof end;

theorem Th15: :: ALGSEQ_1:15

for b₁, b₂ being Nat st b₁ <= b₂ holds
( PSeg b₁ = (PSeg b₁) /\ (PSeg b₂) & PSeg b₁ = (PSeg b₂) /\ (PSeg b₁) )

proof end;

theorem Th16: :: ALGSEQ_1:16

for b₁, b₂ being Nat st ( PSeg b₁ = (PSeg b₁) /\ (PSeg b₂) or PSeg b₁ = (PSeg b₂) /\ (PSeg b₁) ) holds
b₁ <= b₂

proof end;

theorem Th17: :: ALGSEQ_1:17

for b₁ being Nat holds (PSeg b₁) \/ {b₁} = PSeg (b₁ + 1)

proof end;

definition

let c₁ be non empty ZeroStr ;
let c₂ be sequence of c₁;
attr a₂ is finite-Support means :Def2: :: ALGSEQ_1:def 2
ex b₁ being Nat st
for b₂ being Nat st b₂ >= b₁ holds
a₂ . b₂ = 0. a₁;

end;

:: deftheorem Def2 defines finite-Support ALGSEQ_1:def 2 :

registration

let c₁ be non empty ZeroStr ;
cluster finite-Support M5( NAT ,the carrier of a₁);
existence

proof end;

end;

definition

let c₁ be non empty ZeroStr ;
mode AlgSequence of a₁ is finite-Support sequence of a₁;

end;

definition

let c₁ be non empty ZeroStr ;
let c₂ be AlgSequence of c₁;
let c₃ be Nat;
pred c₃ is_at_least_length_of c₂ means :Def3: :: ALGSEQ_1:def 3
for b₁ being Nat st b₁ >= a₃ holds
a₂ . b₁ = 0. a₁;

end;

:: deftheorem Def3 defines is_at_least_length_of ALGSEQ_1:def 3 :

Lemma10: for b₁ being non empty ZeroStr
for b₂ being AlgSequence of b₁ ex b₃ being Nat st b₃ is_at_least_length_of b₂

proof end;

Lemma11: for b₁ being non empty ZeroStr
for b₂ being AlgSequence of b₁ ex b₃ being Nat st
( b₃ is_at_least_length_of b₂ & ( for b₄ being Nat st b₄ is_at_least_length_of b₂ holds
b₃ <= b₄ ) )

proof end;

Lemma12: for b₁, b₂ being Nat
for b₃ being non empty ZeroStr
for b₄ being AlgSequence of b₃ st b₁ is_at_least_length_of b₄ & ( for b₅ being Nat st b₅ is_at_least_length_of b₄ holds
b₁ <= b₅ ) & b₂ is_at_least_length_of b₄ & ( for b₅ being Nat st b₅ is_at_least_length_of b₄ holds
b₂ <= b₅ ) holds
b₁ = b₂

proof end;

definition

let c₁ be non empty ZeroStr ;
let c₂ be AlgSequence of c₁;
func len c₂ -> Nat means :Def4: :: ALGSEQ_1:def 4
( a₃ is_at_least_length_of a₂ & ( for b₁ being Nat st b₁ is_at_least_length_of a₂ holds
a₃ <= b₁ ) );
existence by Lemma11;
uniqueness by Lemma12;

end;

:: deftheorem Def4 defines len ALGSEQ_1:def 4 :

theorem Th18: :: ALGSEQ_1:18

canceled;

theorem Th19: :: ALGSEQ_1:19

canceled;

theorem Th20: :: ALGSEQ_1:20

canceled;

theorem Th21: :: ALGSEQ_1:21

canceled;

theorem Th22: :: ALGSEQ_1:22

for b₁ being Nat
for b₂ being non empty ZeroStr
for b₃ being AlgSequence of b₂ st b₁ >= len b₃ holds
b₃ . b₁ = 0. b₂

proof end;

theorem Th23: :: ALGSEQ_1:23

canceled;

theorem Th24: :: ALGSEQ_1:24

for b₁ being Nat
for b₂ being non empty ZeroStr
for b₃ being AlgSequence of b₂ st ( for b₄ being Nat st b₄ < b₁ holds
b₃ . b₄ <> 0. b₂ ) holds
len b₃ >= b₁

proof end;

theorem Th25: :: ALGSEQ_1:25

for b₁ being Nat
for b₂ being non empty ZeroStr
for b₃ being AlgSequence of b₂ st len b₃ = b₁ + 1 holds
b₃ . b₁ <> 0. b₂

proof end;

definition

let c₁ be non empty ZeroStr ;
let c₂ be AlgSequence of c₁;
func support c₂ -> Subset of NAT equals :: ALGSEQ_1:def 5
PSeg (len a₂);
coherence ;

end;

:: deftheorem Def5 defines support ALGSEQ_1:def 5 :

theorem Th26: :: ALGSEQ_1:26

canceled;

theorem Th27: :: ALGSEQ_1:27

for b₁ being Nat
for b₂ being non empty ZeroStr
for b₃ being AlgSequence of b₂ holds
( b₁ = len b₃ iff PSeg b₁ = support b₃ ) by Th14;

scheme :: ALGSEQ_1:sch 1
s1{ F₁() -> non empty ZeroStr , F₂() -> Nat, F₃( Nat) -> Element of F₁() } :

ex b₁ being AlgSequence of F₁() st
( len b₁ <= F₂() & ( for b₂ being Nat st b₂ < F₂() holds
b₁ . b₂ = F₃(b₂) ) )

proof end;

theorem Th28: :: ALGSEQ_1:28

for b₁ being non empty ZeroStr
for b₂, b₃ being AlgSequence of b₁ st len b₂ = len b₃ & ( for b₄ being Nat st b₄ < len b₂ holds
b₂ . b₄ = b₃ . b₄ ) holds
b₂ = b₃

proof end;

theorem Th29: :: ALGSEQ_1:29

for b₁ being non empty ZeroStr st the carrier of b₁ <> {(0. b₁)} holds
for b₂ being Nat ex b₃ being AlgSequence of b₁ st len b₃ = b₂

proof end;

definition

let c₁ be non empty ZeroStr ;
let c₂ be Element of c₁;
func <%c₂%> -> AlgSequence of a₁ means :Def6: :: ALGSEQ_1:def 6
( len a₃ <= 1 & a₃ . 0 = a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines <% ALGSEQ_1:def 6 :

Lemma19: for b₁ being non empty ZeroStr
for b₂ being AlgSequence of b₁ st b₂ = <%(0. b₁)%> holds
len b₂ = 0

proof end;

theorem Th30: :: ALGSEQ_1:30

canceled;

theorem Th31: :: ALGSEQ_1:31

for b₁ being non empty ZeroStr
for b₂ being AlgSequence of b₁ holds
( b₂ = <%(0. b₁)%> iff len b₂ = 0 )

proof end;

theorem Th32: :: ALGSEQ_1:32

for b₁ being non empty ZeroStr
for b₂ being AlgSequence of b₁ holds
( b₂ = <%(0. b₁)%> iff support b₂ = {} )

proof end;

theorem Th33: :: ALGSEQ_1:33

for b₁ being Nat
for b₂ being non empty ZeroStr holds <%(0. b₂)%> . b₁ = 0. b₂

proof end;

theorem Th34: :: ALGSEQ_1:34

for b₁ being non empty ZeroStr
for b₂ being AlgSequence of b₁ holds
( b₂ = <%(0. b₁)%> iff rng b₂ = {(0. b₁)} )

proof end;