:: ALGSEQ_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let n be Nat;
func PSeg n -> set equals :: ALGSEQ_1:def 1
{ k where k is Nat : k < n } ;
coherence
{ k where k is Nat : k < n } is set ;
end;

:: deftheorem defines PSeg ALGSEQ_1:def 1 :
for n being Nat holds PSeg n = { k where k is Nat : k < n } ;

definition
let n be Nat;
:: original: PSeg
redefine func PSeg n -> Subset of NAT ;
coherence
PSeg n is Subset of NAT
proof end;
end;

Lm1: for n being Nat
for x being set st x in PSeg n holds
x is Nat
;

theorem :: ALGSEQ_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALGSEQ_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALGSEQ_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALGSEQ_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALGSEQ_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALGSEQ_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALGSEQ_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALGSEQ_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALGSEQ_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th10: :: ALGSEQ_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, n being Nat holds
( k in PSeg n iff k < n )
proof end;

theorem Th11: :: ALGSEQ_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( PSeg 0 = {} & PSeg 1 = {0} & PSeg 2 = {0,1} )
proof end;

theorem Th12: :: ALGSEQ_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds n in PSeg (n + 1)
proof end;

theorem Th13: :: ALGSEQ_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being Nat holds
( n <= m iff PSeg n c= PSeg m )
proof end;

theorem Th14: :: ALGSEQ_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being Nat st PSeg n = PSeg m holds
n = m
proof end;

theorem Th15: :: ALGSEQ_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, n being Nat st k <= n holds
( PSeg k = (PSeg k) /\ (PSeg n) & PSeg k = (PSeg n) /\ (PSeg k) )
proof end;

theorem :: ALGSEQ_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, n being Nat st ( PSeg k = (PSeg k) /\ (PSeg n) or PSeg k = (PSeg n) /\ (PSeg k) ) holds
k <= n
proof end;

theorem :: ALGSEQ_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds (PSeg n) \/ {n} = PSeg (n + 1)
proof end;

definition
let R be non empty ZeroStr ;
let F be sequence of R;
attr F is finite-Support means :Def2: :: ALGSEQ_1:def 2
 ex n being Nat st
for i being Nat st i >= n holds
F . i = 0. R;
end;

:: deftheorem Def2 defines finite-Support ALGSEQ_1:def 2 :
for R being non empty ZeroStr
for F being sequence of R holds
( F is finite-Support iff ex n being Nat st
for i being Nat st i >= n holds
F . i = 0. R );

registration
let R be non empty ZeroStr ;
cluster finite-Support M5( NAT ,the carrier of R);
existence
ex b1 being sequence of R st b1 is finite-Support
proof end;
end;

definition
let R be non empty ZeroStr ;
mode AlgSequence of R is finite-Support sequence of R;
end;

definition
let R be non empty ZeroStr ;
let p be AlgSequence of R;
let k be Nat;
pred k is_at_least_length_of p means :Def3: :: ALGSEQ_1:def 3
for i being Nat st i >= k holds
p . i = 0. R;
end;

:: deftheorem Def3 defines is_at_least_length_of ALGSEQ_1:def 3 :
for R being non empty ZeroStr
for p being AlgSequence of R
for k being Nat holds
( k is_at_least_length_of p iff for i being Nat st i >= k holds
p . i = 0. R );

Lm2: for R being non empty ZeroStr
for p being AlgSequence of R ex m being Nat st m is_at_least_length_of p
proof end;

Lm3: for R being non empty ZeroStr
for p being AlgSequence of R ex k being Nat st
( k is_at_least_length_of p & ( for n being Nat st n is_at_least_length_of p holds
k <= n ) )
proof end;

Lm4: for k, l being Nat
for R being non empty ZeroStr
for p being AlgSequence of R st k is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds
k <= m ) & l is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds
l <= m ) holds
k = l
proof end;

definition
let R be non empty ZeroStr ;
let p be AlgSequence of R;
func len p -> Nat means :Def4: :: ALGSEQ_1:def 4
( it is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds
it <= m ) );
existence
ex b1 being Nat st
( b1 is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds
b1 <= m ) ) by Lm3;
uniqueness
for b1, b2 being Nat st b1 is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds
b1 <= m ) & b2 is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds
b2 <= m ) holds
b1 = b2 by Lm4;
end;

:: deftheorem Def4 defines len ALGSEQ_1:def 4 :
for R being non empty ZeroStr
for p being AlgSequence of R
for b3 being Nat holds
( b3 = len p iff ( b3 is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds
b3 <= m ) ) );

theorem :: ALGSEQ_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALGSEQ_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALGSEQ_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALGSEQ_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th22: :: ALGSEQ_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for R being non empty ZeroStr
for p being AlgSequence of R st i >= len p holds
p . i = 0. R
proof end;

theorem :: ALGSEQ_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th24: :: ALGSEQ_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for R being non empty ZeroStr
for p being AlgSequence of R st ( for i being Nat st i < k holds
p . i <> 0. R ) holds
len p >= k
proof end;

theorem Th25: :: ALGSEQ_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for R being non empty ZeroStr
for p being AlgSequence of R st len p = k + 1 holds
p . k <> 0. R
proof end;

definition
let R be non empty ZeroStr ;
let p be AlgSequence of R;
func support p -> Subset of NAT equals :: ALGSEQ_1:def 5
 PSeg (len p);
coherence
PSeg (len p) is Subset of NAT ;
end;

:: deftheorem defines support ALGSEQ_1:def 5 :
for R being non empty ZeroStr
for p being AlgSequence of R holds support p = PSeg (len p);

theorem :: ALGSEQ_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALGSEQ_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for R being non empty ZeroStr
for p being AlgSequence of R holds
( k = len p iff PSeg k = support p ) by Th14;

scheme :: ALGSEQ_1:sch 1
AlgSeqLambdaF{ F1() -> non empty ZeroStr , F2() -> Nat, F3( Nat) -> Element of F1() } :
ex p being AlgSequence of F1() st
( len p <= F2() & ( for k being Nat st k < F2() holds
p . k = F3(k) ) )
proof end;

theorem Th28: :: ALGSEQ_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty ZeroStr
for p, q being AlgSequence of R st len p = len q & ( for k being Nat st k < len p holds
p . k = q . k ) holds
p = q
proof end;

theorem :: ALGSEQ_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty ZeroStr st the carrier of R <> {(0. R)} holds
for k being Nat ex p being AlgSequence of R st len p = k
proof end;

definition
let R be non empty ZeroStr ;
let x be Element of R;
func <%x%> -> AlgSequence of R means :Def6: :: ALGSEQ_1:def 6
( len it <= 1 & it . 0 = x );
existence
ex b1 being AlgSequence of R st
( len b1 <= 1 & b1 . 0 = x )
proof end;
uniqueness
for b1, b2 being AlgSequence of R st len b1 <= 1 & b1 . 0 = x & len b2 <= 1 & b2 . 0 = x holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines <% ALGSEQ_1:def 6 :
for R being non empty ZeroStr
for x being Element of R
for b3 being AlgSequence of R holds
( b3 = <%x%> iff ( len b3 <= 1 & b3 . 0 = x ) );

Lm5: for R being non empty ZeroStr
for p being AlgSequence of R st p = <%(0. R)%> holds
len p = 0
proof end;

theorem :: ALGSEQ_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th31: :: ALGSEQ_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty ZeroStr
for p being AlgSequence of R holds
( p = <%(0. R)%> iff len p = 0 )
proof end;

theorem :: ALGSEQ_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty ZeroStr
for p being AlgSequence of R holds
( p = <%(0. R)%> iff support p = {} )
proof end;

theorem Th33: :: ALGSEQ_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for R being non empty ZeroStr holds <%(0. R)%> . i = 0. R
proof end;

theorem :: ALGSEQ_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty ZeroStr
for p being AlgSequence of R holds
( p = <%(0. R)%> iff rng p = {(0. R)} )
proof end;