SCMFSA_7: Some Multi-instructions defined by sequence of instructions of SCM+FSA

:: Some Multi-instructions defined by sequence of instructions of SCM+FSA
:: by Noriko Asamoto
::
:: Received April 24, 1996
:: Copyright (c) 1996 Association of Mizar Users

begin

Lm1: 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;

Lm2: 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;

Lm3: 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;

deffunc H₁( Element of NAT ) -> Element of NAT = $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 = { (m -' 1) where m is Element of NAT : m in dom f } & ( for k being Element of NAT st k in dom it holds
it . k = f /. (k + 1) ) );
existence

proof end;

proof end;

end;

:: deftheorem Def1 defines Load SCMFSA_7:def 1 :

theorem :: SCMFSA_7:1

canceled;

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;

theorem :: SCMFSA_7:11

canceled;

theorem :: SCMFSA_7:12

canceled;

theorem :: SCMFSA_7:13

canceled;

theorem :: SCMFSA_7:14

canceled;

theorem :: SCMFSA_7:15

canceled;

theorem :: SCMFSA_7:16

canceled;

theorem :: SCMFSA_7:17

canceled;

theorem :: SCMFSA_7:18

canceled;

theorem :: SCMFSA_7:19

canceled;

theorem :: SCMFSA_7:20

canceled;

theorem :: SCMFSA_7:21

canceled;

theorem :: SCMFSA_7:22

canceled;

theorem :: SCMFSA_7:23

canceled;

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 Element of NAT holds
( k in dom (Load p) iff k + 1 in dom p )

proof end;

theorem :: SCMFSA_7:27

canceled;

theorem :: SCMFSA_7:28

canceled;

theorem Th29: :: SCMFSA_7:29

for p being FinSequence of the Instructions of SCM+FSA
for k being Element of NAT holds
( 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 Element of 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 Element of 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 Element of NAT st
( k1 + 1 = k & it = <*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 ))) ) if k > 0
otherwise ex k1 being Element of 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 Element of 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;

proof end;

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 Element of NAT st IC s = insloc c0 holds
for a being Int-Location
for k being Integer st a <> intloc 0 & ( for c being Element of NAT st c in dom (aSeq a,k) holds
(aSeq a,k) . c = s . (insloc ((c0 + c) -' 1)) ) holds
( ( for i being Element of 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 Element of 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
( ProgramPart s halts_on s & (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
( ProgramPart s halts_on s & (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;