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) )
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 )
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) )
deffunc H1( Element of NAT ) -> Element of NAT = $1 -' 1;
:: deftheorem Def1 defines Load SCMFSA_7:def 1 :
for f being FinSequence of the Instructions of SCM+FSA
for b2 being FinPartState of SCM+FSA holds
( b2 = Load f iff ( dom b2 = { (m -' 1) where m is Element of NAT : m in dom f } & ( for k being Element of NAT st k in dom b2 holds
b2 . k = f /. (k + 1) ) ) );
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th26:
theorem
canceled;
theorem
canceled;
theorem Th29:
theorem
theorem Th31:
theorem
:: deftheorem Def2 defines := SCMFSA_7:def 2 :
for a being Int-Location
for k being Integer
for b3 being FinPartState of SCM+FSA holds
( ( k > 0 implies ( b3 = a := k iff ex k1 being Element of NAT st
( k1 + 1 = k & b3 = Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) ) ) ) & ( not k > 0 implies ( b3 = a := k iff ex k1 being Element of NAT st
( k1 + k = 1 & b3 = Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) ) ) ) );
definition
let a be
Int-Location ;
let k be
Integer;
func aSeq a,
k -> FinSequence of the
Instructions of
SCM+FSA means :
Def3:
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
( ( k > 0 implies ex b1 being FinSequence of the Instructions of SCM+FSA ex k1 being Element of NAT st
( k1 + 1 = k & b1 = <*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 ))) ) ) & ( not k > 0 implies ex b1 being FinSequence of the Instructions of SCM+FSA ex k1 being Element of NAT st
( k1 + k = 1 & b1 = <*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 ))) ) ) )
uniqueness
for b1, b2 being FinSequence of the Instructions of SCM+FSA holds
( ( k > 0 & ex k1 being Element of NAT st
( k1 + 1 = k & b1 = <*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 ))) ) & ex k1 being Element of NAT st
( k1 + 1 = k & b2 = <*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 ))) ) implies b1 = b2 ) & ( not k > 0 & ex k1 being Element of NAT st
( k1 + k = 1 & b1 = <*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 ))) ) & ex k1 being Element of NAT st
( k1 + k = 1 & b2 = <*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 ))) ) implies b1 = b2 ) )
;
correctness
consistency
for b1 being FinSequence of the Instructions of SCM+FSA holds verum;
;
end;
:: deftheorem Def3 defines aSeq SCMFSA_7:def 3 :
for a being Int-Location
for k being Integer
for b3 being FinSequence of the Instructions of SCM+FSA holds
( ( k > 0 implies ( b3 = aSeq a,k iff ex k1 being Element of NAT st
( k1 + 1 = k & b3 = <*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 ))) ) ) ) & ( not k > 0 implies ( b3 = aSeq a,k iff ex k1 being Element of NAT st
( k1 + k = 1 & b3 = <*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 ))) ) ) ) );
theorem
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:
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
ex b1 being FinSequence of the Instructions of SCM+FSA 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))*> ) ) & b1 = FlattenSeq pp )
uniqueness
for b1, b2 being FinSequence of the Instructions of SCM+FSA st 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))*> ) ) & b1 = FlattenSeq pp ) & 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))*> ) ) & b2 = FlattenSeq pp ) holds
b1 = b2
correctness
;
end;
:: deftheorem Def4 defines aSeq SCMFSA_7:def 4 :
for f being FinSeq-Location
for p being FinSequence of INT
for b3 being FinSequence of the Instructions of SCM+FSA holds
( b3 = aSeq f,p iff 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))*> ) ) & b3 = FlattenSeq pp ) );
:: deftheorem defines := SCMFSA_7:def 5 :
for f being FinSeq-Location
for p being FinSequence of INT holds f := p = Load ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>);
theorem
theorem
theorem Th36:
for
s being
State of
SCM+FSA st
s . (intloc 0 ) = 1 holds
for
c0 being
Element of
NAT st
IC s = 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 . ((c0 + c) -' 1) ) holds
( ( for
i being
Element of
NAT st
i <= len (aSeq a,k) holds
(
IC (Comput (ProgramPart s),s,i) = c0 + i & ( for
b being
Int-Location st
b <> a holds
(Comput (ProgramPart s),s,i) . b = s . b ) & ( for
f being
FinSeq-Location holds
(Comput (ProgramPart s),s,i) . f = s . f ) ) ) &
(Comput (ProgramPart s),s,(len (aSeq a,k))) . a = k )
theorem Th37:
for
s being
State of
SCM+FSA st
IC s = 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 (Comput (ProgramPart s),s,i) = i & ( for
b being
Int-Location st
b <> a holds
(Comput (ProgramPart s),s,i) . b = s . b ) & ( for
f being
FinSeq-Location holds
(Comput (ProgramPart s),s,i) . f = s . f ) ) ) &
(Comput (ProgramPart s),s,(len (aSeq a,k))) . a = k )
theorem
theorem