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

Lm1: for p1, p2, p3, p4 being XFinSequence 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;

Lm2: for p1, p2, p3, p4, p5 being XFinSequence 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₁( Nat) -> Element of NAT = $1 -' 1;

definition

let a be Int-Location;
let k be Integer;

func a := k -> NAT -defined the InstructionsF of SCM+FSA -valued finite Function means :Def1: :: SCMFSA_7:def 1
ex k1 being Nat st
( k1 + 1 = k & it = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA) ) if k > 0
otherwise ex k1 being Nat st
( k1 + k = 1 & it = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA) );

existence
( ( k > 0 implies ex b₁ being NAT -defined the InstructionsF of SCM+FSA -valued finite Function ex k1 being Nat st
( k1 + 1 = k & b₁ = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA) ) ) & ( not k > 0 implies ex b₁ being NAT -defined the InstructionsF of SCM+FSA -valued finite Function ex k1 being Nat st
( k1 + k = 1 & b₁ = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA) ) ) )

proof end;

uniqueness
for b₁, b₂ being NAT -defined the InstructionsF of SCM+FSA -valued finite Function holds
( ( k > 0 & ex k1 being Nat st
( k1 + 1 = k & b₁ = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA) ) & ex k1 being Nat st
( k1 + 1 = k & b₂ = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA) ) implies b₁ = b₂ ) & ( not k > 0 & ex k1 being Nat st
( k1 + k = 1 & b₁ = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA) ) & ex k1 being Nat st
( k1 + k = 1 & b₂ = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA) ) implies b₁ = b₂ ) ) ;
correctness
consistency
for b₁ being NAT -defined the InstructionsF of SCM+FSA -valued finite Function holds verum;
;

end;

:: deftheorem Def1 defines := SCMFSA_7:def 1 :
for a being Int-Location
for k being Integer
for b₃ being NAT -defined the InstructionsF of SCM+FSA -valued finite Function holds
( ( k > 0 implies ( b₃ = a := k iff ex k1 being Nat st
( k1 + 1 = k & b₃ = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA) ) ) ) & ( not k > 0 implies ( b₃ = a := k iff ex k1 being Nat st
( k1 + k = 1 & b₃ = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA) ) ) ) );

definition

let a be Int-Location;
let k be Integer;

func aSeq (a,k) -> XFinSequence of the InstructionsF of SCM+FSA means :Def2: :: SCMFSA_7:def 2
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
( ( k > 0 implies ex b₁ being XFinSequence of the InstructionsF of SCM+FSA ex k1 being Nat st
( k1 + 1 = k & b₁ = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) ) ) & ( not k > 0 implies ex b₁ being XFinSequence of the InstructionsF of SCM+FSA ex k1 being Nat st
( k1 + k = 1 & b₁ = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) ) ) )

proof end;

uniqueness
for b₁, b₂ being XFinSequence of the InstructionsF of SCM+FSA holds
( ( k > 0 & ex k1 being Nat st
( k1 + 1 = k & b₁ = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) ) & ex k1 being Nat st
( k1 + 1 = k & b₂ = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) ) implies b₁ = b₂ ) & ( not k > 0 & ex k1 being Nat st
( k1 + k = 1 & b₁ = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) ) & ex k1 being Nat st
( k1 + k = 1 & b₂ = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) ) implies b₁ = b₂ ) ) ;
correctness
consistency
for b₁ being XFinSequence of the InstructionsF of SCM+FSA holds verum;
;

end;

:: deftheorem Def2 defines aSeq SCMFSA_7:def 2 :
for a being Int-Location
for k being Integer
for b₃ being XFinSequence of the InstructionsF of SCM+FSA holds
( ( k > 0 implies ( b₃ = aSeq (a,k) iff ex k1 being Nat st
( k1 + 1 = k & b₃ = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) ) ) ) & ( not k > 0 implies ( b₃ = aSeq (a,k) iff ex k1 being Nat st
( k1 + k = 1 & b₃ = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) ) ) ) );

theorem :: SCMFSA_7:1

for a being Int-Location
for k being Integer holds a := k = (aSeq (a,k)) ^ (Stop SCM+FSA)

proof end;

definition

let f be FinSeq-Location ;
let p be FinSequence of INT ;

func aSeq (f,p) -> XFinSequence of the InstructionsF of SCM+FSA means :Def3: :: SCMFSA_7:def 3
ex pp being XFinSequence of the InstructionsF of SCM+FSA ^omega st
( len pp = len p & ( for k being Nat st k < len pp holds
ex i being Integer st
( i = p . (k + 1) & pp . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) ) & it = FlattenSeq pp );

existence
ex b₁ being XFinSequence of the InstructionsF of SCM+FSA ex pp being XFinSequence of the InstructionsF of SCM+FSA ^omega st
( len pp = len p & ( for k being Nat st k < len pp holds
ex i being Integer st
( i = p . (k + 1) & pp . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) ) & b₁ = FlattenSeq pp )

proof end;

uniqueness
for b₁, b₂ being XFinSequence of the InstructionsF of SCM+FSA st ex pp being XFinSequence of the InstructionsF of SCM+FSA ^omega st
( len pp = len p & ( for k being Nat st k < len pp holds
ex i being Integer st
( i = p . (k + 1) & pp . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) ) & b₁ = FlattenSeq pp ) & ex pp being XFinSequence of the InstructionsF of SCM+FSA ^omega st
( len pp = len p & ( for k being Nat st k < len pp holds
ex i being Integer st
( i = p . (k + 1) & pp . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) ) & b₂ = FlattenSeq pp ) holds
b₁ = b₂

proof end;

correctness
;

end;

:: deftheorem Def3 defines aSeq SCMFSA_7:def 3 :
for f being FinSeq-Location
for p being FinSequence of INT
for b₃ being XFinSequence of the InstructionsF of SCM+FSA holds
( b₃ = aSeq (f,p) iff ex pp being XFinSequence of the InstructionsF of SCM+FSA ^omega st
( len pp = len p & ( for k being Nat st k < len pp holds
ex i being Integer st
( i = p . (k + 1) & pp . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) ) & b₃ = FlattenSeq pp ) );

definition

let f be FinSeq-Location ;
let p be FinSequence of INT ;

func f := p -> NAT -defined the InstructionsF of SCM+FSA -valued finite Function equals :: SCMFSA_7:def 4
(((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA);

correctness
coherence
(((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA) is NAT -defined the InstructionsF of SCM+FSA -valued finite Function;
;

end;

:: deftheorem defines := SCMFSA_7:def 4 :
for f being FinSeq-Location
for p being FinSequence of INT holds f := p = (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA);

theorem :: SCMFSA_7:2

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

proof end;

theorem :: SCMFSA_7:3

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

proof end;

theorem Th4: :: SCMFSA_7:4

for P being the InstructionsF of SCM+FSA -valued ManySortedSet of NAT
for c0 being Nat
for s being b₂ -started State of SCM+FSA st s . (intloc 0) = 1 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 = P . (c0 + c) ) holds
( ( for i being Nat st i <= len (aSeq (a,k)) holds
( IC (Comput (P,s,i)) = c0 + i & ( for b being Int-Location st b <> a holds
(Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ) & (Comput (P,s,(len (aSeq (a,k))))) . a = k )

proof end;

theorem Th5: :: SCMFSA_7:5

for P being the InstructionsF of SCM+FSA -valued ManySortedSet of NAT
for s being 0 -started State of SCM+FSA st s . (intloc 0) = 1 holds
for a being Int-Location
for k being Integer st aSeq (a,k) c= P & a <> intloc 0 holds
( ( for i being Nat st i <= len (aSeq (a,k)) holds
( IC (Comput (P,s,i)) = i & ( for b being Int-Location st b <> a holds
(Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ) & (Comput (P,s,(len (aSeq (a,k))))) . a = k )

proof end;

:: Users' guide

theorem :: SCMFSA_7:6

for P being the InstructionsF of SCM+FSA -valued ManySortedSet of NAT
for s being 0 -started State of SCM+FSA st s . (intloc 0) = 1 holds
for a being Int-Location
for k being Integer st a := k c= P & a <> intloc 0 holds
( P halts_on s & (Result (P,s)) . a = k & ( for b being Int-Location st b <> a holds
(Result (P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result (P,s)) . f = s . f ) )

proof end;

theorem :: SCMFSA_7:7

for P being the InstructionsF of SCM+FSA -valued ManySortedSet of NAT
for s being 0 -started State of SCM+FSA st s . (intloc 0) = 1 holds
for f being FinSeq-Location
for p being FinSequence of INT st f := p c= P holds
( P halts_on s & (Result (P,s)) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Result (P,s)) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Result (P,s)) . g = s . g ) )

proof end;