:: SCMFSA_7 semantic presentation

registration

cluster -> finite FinPartState of SCM+FSA ;
coherence by AMI_1:def 24;

end;

registration

let p be FinSequence;
let x, y be set ;
cluster p +* x,y -> FinSequence-like ;
coherence

proof end;

end;

theorem Th1: :: SCMFSA_7:1

for k being natural number holds abs k = k by ABSVALUE:def 1;

Lm1: for a, b, c being Nat st a >= c & b >= c & a -' c = b -' c holds
a = b
by BINARITH:49;

Lm2: for a, b being natural number st a >= b holds
a -' b = a - b
by BINARITH:50;

Lm3: for a, b being Integer st a < b holds
a <= b - 1
by INT_1:79;

scheme :: SCMFSA_7:sch 1
CardMono''{ F₁() -> set , F₂() -> non empty set , F₃( set ) -> set } :

F₁(),{ F₃(d) where d is Element of F₂() : d in F₁() } are_equipotent

provided

A1: F₁() c= F₂() and
A2: for d1, d2 being Element of F₂() st d1 in F₁() & d2 in F₁() & F₃(d1) = F₃(d2) holds
d1 = d2

proof end;

theorem :: SCMFSA_7:2

canceled;

theorem :: SCMFSA_7:3

canceled;

theorem :: SCMFSA_7:4

canceled;

theorem :: SCMFSA_7:5

canceled;

theorem :: SCMFSA_7:6

canceled;

theorem :: SCMFSA_7:7

canceled;

theorem :: SCMFSA_7:8

canceled;

theorem :: SCMFSA_7:9

canceled;

theorem :: SCMFSA_7:10

canceled;

Lm4: for p1, p2, p3 being FinSequence holds
( ((len p1) + (len p2)) + (len p3) = len ((p1 ^ p2) ^ p3) & ((len p1) + (len p2)) + (len p3) = len (p1 ^ (p2 ^ p3)) & (len p1) + ((len p2) + (len p3)) = len (p1 ^ (p2 ^ p3)) & (len p1) + ((len p2) + (len p3)) = len ((p1 ^ p2) ^ p3) )

proof end;

Lm5: for p1, p2, p3, p4 being FinSequence holds
( ((p1 ^ p2) ^ p3) ^ p4 = (p1 ^ p2) ^ (p3 ^ p4) & ((p1 ^ p2) ^ p3) ^ p4 = p1 ^ ((p2 ^ p3) ^ p4) & ((p1 ^ p2) ^ p3) ^ p4 = p1 ^ (p2 ^ (p3 ^ p4)) & ((p1 ^ p2) ^ p3) ^ p4 = (p1 ^ (p2 ^ p3)) ^ p4 )

proof end;

Lm6: for p1, p2, p3, p4, p5 being FinSequence holds
( (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = ((p1 ^ p2) ^ p3) ^ (p4 ^ p5) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ p2) ^ ((p3 ^ p4) ^ p5) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ p2) ^ (p3 ^ (p4 ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (((p2 ^ p3) ^ p4) ^ p5) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ p3) ^ (p4 ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ ((p3 ^ p4) ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ (p3 ^ (p4 ^ p5))) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = ((p1 ^ p2) ^ (p3 ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ ((p2 ^ p3) ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ (p2 ^ (p3 ^ p4))) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ (p3 ^ p4)) ^ p5) )

proof end;

theorem :: SCMFSA_7:11

canceled;

theorem :: SCMFSA_7:12

for p being FinSequence st p <> {} holds
len p in dom p

proof end;

theorem Th13: :: SCMFSA_7:13

for D being set holds FlattenSeq (<*> (D * )) = <*> D

proof end;

theorem Th14: :: SCMFSA_7:14

for D being set
for F, G being FinSequence of D * holds FlattenSeq (F ^ G) = (FlattenSeq F) ^ (FlattenSeq G)

proof end;

theorem :: SCMFSA_7:15

for D being set
for p, q being Element of D * holds FlattenSeq <*p,q*> = p ^ q

proof end;

theorem :: SCMFSA_7:16

for D being set
for p, q, r being Element of D * holds FlattenSeq <*p,q,r*> = (p ^ q) ^ r

proof end;

theorem Th17: :: SCMFSA_7:17

for D being non empty set
for p, q being FinSequence of D st p c= q holds
ex p' being FinSequence of D st p ^ p' = q

proof end;

theorem Th18: :: SCMFSA_7:18

for D being non empty set
for p, q being FinSequence of D
for i being Nat st p c= q & 1 <= i & i <= len p holds
q . i = p . i

proof end;

theorem Th19: :: SCMFSA_7:19

for D being set
for F, G being FinSequence of D * st F c= G holds
FlattenSeq F c= FlattenSeq G

proof end;

theorem Th20: :: SCMFSA_7:20

for p being FinSequence holds p | (Seg 0) = {}

proof end;

theorem Th21: :: SCMFSA_7:21

for f, g being FinSequence holds f | (Seg 0) = g | (Seg 0)

proof end;

theorem Th22: :: SCMFSA_7:22

for D being non empty set
for x being Element of D holds <*x*> is FinSequence of D ;

theorem Th23: :: SCMFSA_7:23

for D being set
for p, q being FinSequence of D holds p ^ q is FinSequence of D ;

deffunc H₁( Nat) -> Element of the Instruction-Locations of SCM+FSA = insloc ($1 -' 1);

definition

let f be FinSequence of the Instructions of SCM+FSA ;
func Load f -> FinPartState of SCM+FSA means :Def1: :: SCMFSA_7:def 1
( dom it = { (insloc (m -' 1)) where m is Nat : m in dom f } & ( for k being Nat st insloc k in dom it holds
it . (insloc k) = f /. (k + 1) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Load SCMFSA_7:def 1 :

theorem :: SCMFSA_7:24

canceled;

theorem :: SCMFSA_7:25

for f being FinSequence of the Instructions of SCM+FSA holds card (Load f) = len f

proof end;

theorem Th26: :: SCMFSA_7:26

for p being FinSequence of the Instructions of SCM+FSA
for k being Nat holds
( insloc k in dom (Load p) iff k + 1 in dom p )

proof end;

theorem :: SCMFSA_7:27

canceled;

theorem Th28: :: SCMFSA_7:28

for k, n being Nat holds
( k < n iff ( 1 <= k + 1 & k + 1 <= n ) )

proof end;

theorem Th29: :: SCMFSA_7:29

for p being FinSequence of the Instructions of SCM+FSA
for k being Nat holds
( insloc k in dom (Load p) iff k < len p )

proof end;

theorem :: SCMFSA_7:30

for f being non empty FinSequence of the Instructions of SCM+FSA holds
( 1 in dom f & insloc 0 in dom (Load f) )

proof end;

theorem Th31: :: SCMFSA_7:31

for p, q being FinSequence of the Instructions of SCM+FSA holds Load p c= Load (p ^ q)

proof end;

theorem :: SCMFSA_7:32

for p, q being FinSequence of the Instructions of SCM+FSA st p c= q holds
Load p c= Load q

proof end;

definition

let a be Int-Location ;
let k be Integer;
func a := k -> FinPartState of SCM+FSA means :Def2: :: SCMFSA_7:def 2
ex k1 being Nat st
( k1 + 1 = k & it = Load ((<*(a := (intloc 0))*> ^ (k1 |-> (AddTo a,(intloc 0)))) ^ <*(halt SCM+FSA )*>) ) if k > 0
otherwise ex k1 being Nat st
( k1 + k = 1 & it = Load ((<*(a := (intloc 0))*> ^ (k1 |-> (SubFrom a,(intloc 0)))) ^ <*(halt SCM+FSA )*>) );
existence

proof end;

uniqueness ;
correctness ;

end;

:: deftheorem Def2 defines := SCMFSA_7:def 2 :

definition

let a be Int-Location ;
let k be Integer;
func aSeq a,k -> FinSequence of the Instructions of SCM+FSA means :Def3: :: SCMFSA_7:def 3
ex k1 being Nat st
( k1 + 1 = k & it = <*(a := (intloc 0))*> ^ (k1 |-> (AddTo a,(intloc 0))) ) if k > 0
otherwise ex k1 being Nat st
( k1 + k = 1 & it = <*(a := (intloc 0))*> ^ (k1 |-> (SubFrom a,(intloc 0))) );
existence

proof end;

uniqueness ;
correctness ;

end;

:: deftheorem Def3 defines aSeq SCMFSA_7:def 3 :

theorem :: SCMFSA_7:33

for a being Int-Location
for k being Integer holds a := k = Load ((aSeq a,k) ^ <*(halt SCM+FSA )*>)

proof end;

definition

let f be FinSeq-Location ;
let p be FinSequence of INT ;
func aSeq f,p -> FinSequence of the Instructions of SCM+FSA means :Def4: :: SCMFSA_7:def 4
ex pp being FinSequence of the Instructions of SCM+FSA * st
( len pp = len p & ( for k being Nat st 1 <= k & k <= len p holds
ex i being Integer st
( i = p . k & pp . k = ((aSeq (intloc 1),k) ^ (aSeq (intloc 2),i)) ^ <*(f,(intloc 1) := (intloc 2))*> ) ) & it = FlattenSeq pp );
existence

proof end;

uniqueness

proof end;

correctness ;

end;

:: deftheorem Def4 defines aSeq SCMFSA_7:def 4 :

definition

let f be FinSeq-Location ;
let p be FinSequence of INT ;
func f := p -> FinPartState of SCM+FSA equals :: SCMFSA_7:def 5
Load ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>);
correctness ;

end;

:: deftheorem defines := SCMFSA_7:def 5 :

theorem :: SCMFSA_7:34

for a being Int-Location holds a := 1 = Load (<*(a := (intloc 0))*> ^ <*(halt SCM+FSA )*>)

proof end;

theorem :: SCMFSA_7:35

for a being Int-Location holds a := 0 = Load ((<*(a := (intloc 0))*> ^ <*(SubFrom a,(intloc 0))*>) ^ <*(halt SCM+FSA )*>)

proof end;

theorem Th36: :: SCMFSA_7:36

for s being State of SCM+FSA st s . (intloc 0) = 1 holds
for c0 being Nat st IC s = insloc c0 holds
for a being Int-Location
for k being Integer st a <> intloc 0 & ( for c being Nat st c in dom (aSeq a,k) holds
(aSeq a,k) . c = s . (insloc ((c0 + c) -' 1)) ) holds
( ( for i being Nat st i <= len (aSeq a,k) holds
( IC ((Computation s) . i) = insloc (c0 + i) & ( for b being Int-Location st b <> a holds
((Computation s) . i) . b = s . b ) & ( for f being FinSeq-Location holds ((Computation s) . i) . f = s . f ) ) ) & ((Computation s) . (len (aSeq a,k))) . a = k )

proof end;

theorem Th37: :: SCMFSA_7:37

for s being State of SCM+FSA st IC s = insloc 0 & s . (intloc 0) = 1 holds
for a being Int-Location
for k being Integer st Load (aSeq a,k) c= s & a <> intloc 0 holds
( ( for i being Nat st i <= len (aSeq a,k) holds
( IC ((Computation s) . i) = insloc i & ( for b being Int-Location st b <> a holds
((Computation s) . i) . b = s . b ) & ( for f being FinSeq-Location holds ((Computation s) . i) . f = s . f ) ) ) & ((Computation s) . (len (aSeq a,k))) . a = k )

proof end;

theorem :: SCMFSA_7:38

for s being State of SCM+FSA st IC s = insloc 0 & s . (intloc 0) = 1 holds
for a being Int-Location
for k being Integer st a := k c= s & a <> intloc 0 holds
( s is halting & (Result s) . a = k & ( for b being Int-Location st b <> a holds
(Result s) . b = s . b ) & ( for f being FinSeq-Location holds (Result s) . f = s . f ) )

proof end;

theorem :: SCMFSA_7:39

for s being State of SCM+FSA st IC s = insloc 0 & s . (intloc 0) = 1 holds
for f being FinSeq-Location
for p being FinSequence of INT st f := p c= s holds
( s is halting & (Result s) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Result s) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Result s) . g = s . g ) )

proof end;