:: SCMFSA_7 semantic presentation

registration

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

end;

registration

let c₁ be FinSequence;
let c₂, c₃ be set ;
cluster a₁ +* a₂,a₃ -> FinSequence-like ;
coherence

proof end;

end;

theorem Th1: :: SCMFSA_7:1

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

Lemma2: for b₁, b₂, b₃ being Nat st b₁ >= b₃ & b₂ >= b₃ & b₁ -' b₃ = b₂ -' b₃ holds
b₁ = b₂
by BINARITH:49;

Lemma3: for b₁, b₂ being natural number st b₁ >= b₂ holds
b₁ -' b₂ = b₁ - b₂
by BINARITH:50;

Lemma4: for b₁, b₂ being Integer st b₁ < b₂ holds
b₁ <= b₂ - 1
by INT_1:79;

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

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

provided

E5: F₁() c= F₂() and
E6: for b₁, b₂ being Element of F₂() st b₁ in F₁() & b₂ in F₁() & F₃(b₁) = F₃(b₂) holds
b₁ = b₂

proof end;

theorem Th2: :: SCMFSA_7:2

canceled;

theorem Th3: :: SCMFSA_7:3

canceled;

theorem Th4: :: SCMFSA_7:4

canceled;

theorem Th5: :: SCMFSA_7:5

canceled;

theorem Th6: :: SCMFSA_7:6

canceled;

theorem Th7: :: SCMFSA_7:7

canceled;

theorem Th8: :: SCMFSA_7:8

canceled;

theorem Th9: :: SCMFSA_7:9

canceled;

theorem Th10: :: SCMFSA_7:10

canceled;

Lemma5: for b₁, b₂, b₃ being FinSequence holds
( ((len b₁) + (len b₂)) + (len b₃) = len ((b₁ ^ b₂) ^ b₃) & ((len b₁) + (len b₂)) + (len b₃) = len (b₁ ^ (b₂ ^ b₃)) & (len b₁) + ((len b₂) + (len b₃)) = len (b₁ ^ (b₂ ^ b₃)) & (len b₁) + ((len b₂) + (len b₃)) = len ((b₁ ^ b₂) ^ b₃) )

proof end;

Lemma6: for b₁, b₂, b₃, b₄ being FinSequence holds
( ((b₁ ^ b₂) ^ b₃) ^ b₄ = (b₁ ^ b₂) ^ (b₃ ^ b₄) & ((b₁ ^ b₂) ^ b₃) ^ b₄ = b₁ ^ ((b₂ ^ b₃) ^ b₄) & ((b₁ ^ b₂) ^ b₃) ^ b₄ = b₁ ^ (b₂ ^ (b₃ ^ b₄)) & ((b₁ ^ b₂) ^ b₃) ^ b₄ = (b₁ ^ (b₂ ^ b₃)) ^ b₄ )

proof end;

Lemma7: for b₁, b₂, b₃, b₄, b₅ being FinSequence holds
( (((b₁ ^ b₂) ^ b₃) ^ b₄) ^ b₅ = ((b₁ ^ b₂) ^ b₃) ^ (b₄ ^ b₅) & (((b₁ ^ b₂) ^ b₃) ^ b₄) ^ b₅ = (b₁ ^ b₂) ^ ((b₃ ^ b₄) ^ b₅) & (((b₁ ^ b₂) ^ b₃) ^ b₄) ^ b₅ = (b₁ ^ b₂) ^ (b₃ ^ (b₄ ^ b₅)) & (((b₁ ^ b₂) ^ b₃) ^ b₄) ^ b₅ = b₁ ^ (((b₂ ^ b₃) ^ b₄) ^ b₅) & (((b₁ ^ b₂) ^ b₃) ^ b₄) ^ b₅ = b₁ ^ ((b₂ ^ b₃) ^ (b₄ ^ b₅)) & (((b₁ ^ b₂) ^ b₃) ^ b₄) ^ b₅ = b₁ ^ (b₂ ^ ((b₃ ^ b₄) ^ b₅)) & (((b₁ ^ b₂) ^ b₃) ^ b₄) ^ b₅ = b₁ ^ (b₂ ^ (b₃ ^ (b₄ ^ b₅))) & (((b₁ ^ b₂) ^ b₃) ^ b₄) ^ b₅ = ((b₁ ^ b₂) ^ (b₃ ^ b₄)) ^ b₅ & (((b₁ ^ b₂) ^ b₃) ^ b₄) ^ b₅ = (b₁ ^ ((b₂ ^ b₃) ^ b₄)) ^ b₅ & (((b₁ ^ b₂) ^ b₃) ^ b₄) ^ b₅ = (b₁ ^ (b₂ ^ (b₃ ^ b₄))) ^ b₅ & (((b₁ ^ b₂) ^ b₃) ^ b₄) ^ b₅ = b₁ ^ ((b₂ ^ (b₃ ^ b₄)) ^ b₅) )

proof end;

theorem Th11: :: SCMFSA_7:11

canceled;

theorem Th12: :: SCMFSA_7:12

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

proof end;

theorem Th13: :: SCMFSA_7:13

for b₁ being set holds FlattenSeq (<*> (b₁ * )) = <*> b₁

proof end;

theorem Th14: :: SCMFSA_7:14

for b₁ being set
for b₂, b₃ being FinSequence of b₁ * holds FlattenSeq (b₂ ^ b₃) = (FlattenSeq b₂) ^ (FlattenSeq b₃)

proof end;

theorem Th15: :: SCMFSA_7:15

for b₁ being set
for b₂, b₃ being Element of b₁ * holds FlattenSeq <*b₂,b₃*> = b₂ ^ b₃

proof end;

theorem Th16: :: SCMFSA_7:16

for b₁ being set
for b₂, b₃, b₄ being Element of b₁ * holds FlattenSeq <*b₂,b₃,b₄*> = (b₂ ^ b₃) ^ b₄

proof end;

theorem Th17: :: SCMFSA_7:17

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁ st b₂ c= b₃ holds
ex b₄ being FinSequence of b₁ st b₂ ^ b₄ = b₃

proof end;

theorem Th18: :: SCMFSA_7:18

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁
for b₄ being Nat st b₂ c= b₃ & 1 <= b₄ & b₄ <= len b₂ holds
b₃ . b₄ = b₂ . b₄

proof end;

theorem Th19: :: SCMFSA_7:19

for b₁ being set
for b₂, b₃ being FinSequence of b₁ * st b₂ c= b₃ holds
FlattenSeq b₂ c= FlattenSeq b₃

proof end;

theorem Th20: :: SCMFSA_7:20

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

proof end;

theorem Th21: :: SCMFSA_7:21

for b₁, b₂ being FinSequence holds b₁ | (Seg 0) = b₂ | (Seg 0)

proof end;

theorem Th22: :: SCMFSA_7:22

for b₁ being non empty set
for b₂ being Element of b₁ holds <*b₂*> is FinSequence of b₁ ;

theorem Th23: :: SCMFSA_7:23

for b₁ being set
for b₂, b₃ being FinSequence of b₁ holds b₂ ^ b₃ is FinSequence of b₁ ;

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

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Load SCMFSA_7:def 1 :

theorem Th24: :: SCMFSA_7:24

canceled;

theorem Th25: :: SCMFSA_7:25

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

proof end;

theorem Th26: :: SCMFSA_7:26

for b₁ being FinSequence of the Instructions of SCM+FSA
for b₂ being Nat holds
( insloc b₂ in dom (Load b₁) iff b₂ + 1 in dom b₁ )

proof end;

theorem Th27: :: SCMFSA_7:27

canceled;

theorem Th28: :: SCMFSA_7:28

for b₁, b₂ being Nat holds
( b₁ < b₂ iff ( 1 <= b₁ + 1 & b₁ + 1 <= b₂ ) )

proof end;

theorem Th29: :: SCMFSA_7:29

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

proof end;

theorem Th30: :: SCMFSA_7:30

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

proof end;

theorem Th31: :: SCMFSA_7:31

for b₁, b₂ being FinSequence of the Instructions of SCM+FSA holds Load b₁ c= Load (b₁ ^ b₂)

proof end;

theorem Th32: :: SCMFSA_7:32

for b₁, b₂ being FinSequence of the Instructions of SCM+FSA st b₁ c= b₂ holds
Load b₁ c= Load b₂

proof end;

definition

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

proof end;

uniqueness ;
correctness ;

end;

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

definition

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

proof end;

uniqueness ;
correctness ;

end;

:: deftheorem Def3 defines aSeq SCMFSA_7:def 3 :

theorem Th33: :: SCMFSA_7:33

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

proof end;

definition

let c₁ be FinSeq-Location ;
let c₂ be FinSequence of INT ;
func aSeq c₁,c₂ -> FinSequence of the Instructions of SCM+FSA means :Def4: :: SCMFSA_7:def 4
ex b₁ being FinSequence of the Instructions of SCM+FSA * st
( len b₁ = len a₂ & ( for b₂ being Nat st 1 <= b₂ & b₂ <= len a₂ holds
ex b₃ being Integer st
( b₃ = a₂ . b₂ & b₁ . b₂ = ((aSeq (intloc 1),b₂) ^ (aSeq (intloc 2),b₃)) ^ <*(a₁,(intloc 1) := (intloc 2))*> ) ) & a₃ = FlattenSeq b₁ );
existence

proof end;

uniqueness

proof end;

correctness ;

end;

:: deftheorem Def4 defines aSeq SCMFSA_7:def 4 :

definition

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

end;

:: deftheorem Def5 defines := SCMFSA_7:def 5 :

theorem Th34: :: SCMFSA_7:34

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

proof end;

theorem Th35: :: SCMFSA_7:35

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

proof end;

theorem Th36: :: SCMFSA_7:36

for b₁ being State of SCM+FSA st b₁ . (intloc 0) = 1 holds
for b₂ being Nat st IC b₁ = insloc b₂ holds
for b₃ being Int-Location
for b₄ being Integer st b₃ <> intloc 0 & ( for b₅ being Nat st b₅ in dom (aSeq b₃,b₄) holds
(aSeq b₃,b₄) . b₅ = b₁ . (insloc ((b₂ + b₅) -' 1)) ) holds
( ( for b₅ being Nat st b₅ <= len (aSeq b₃,b₄) holds
( IC ((Computation b₁) . b₅) = insloc (b₂ + b₅) & ( for b₆ being Int-Location st b₆ <> b₃ holds
((Computation b₁) . b₅) . b₆ = b₁ . b₆ ) & ( for b₆ being FinSeq-Location holds ((Computation b₁) . b₅) . b₆ = b₁ . b₆ ) ) ) & ((Computation b₁) . (len (aSeq b₃,b₄))) . b₃ = b₄ )

proof end;

theorem Th37: :: SCMFSA_7:37

for b₁ being State of SCM+FSA st IC b₁ = insloc 0 & b₁ . (intloc 0) = 1 holds
for b₂ being Int-Location
for b₃ being Integer st Load (aSeq b₂,b₃) c= b₁ & b₂ <> intloc 0 holds
( ( for b₄ being Nat st b₄ <= len (aSeq b₂,b₃) holds
( IC ((Computation b₁) . b₄) = insloc b₄ & ( for b₅ being Int-Location st b₅ <> b₂ holds
((Computation b₁) . b₄) . b₅ = b₁ . b₅ ) & ( for b₅ being FinSeq-Location holds ((Computation b₁) . b₄) . b₅ = b₁ . b₅ ) ) ) & ((Computation b₁) . (len (aSeq b₂,b₃))) . b₂ = b₃ )

proof end;

theorem Th38: :: SCMFSA_7:38

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

proof end;

theorem Th39: :: SCMFSA_7:39

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

proof end;