let p1, p2 be Instruction-Sequence of SCM+FSA; for i, k being Nat
for t being FinPartState of SCM+FSA
for p being Program of
for s1, s2 being State of SCM+FSA st k <= i & p c= p1 & p c= p2 & dom t c= Int-Locations \/ FinSeq-Locations & ( for j being Nat holds
( IC (Comput (p1,s1,j)) in dom p & IC (Comput (p2,s2,j)) in dom p ) ) & (Comput (p1,s1,k)) . (IC ) = (Comput (p2,s2,k)) . (IC ) & (Comput (p1,s1,k)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) = (Comput (p2,s2,k)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) holds
( (Comput (p1,s1,i)) . (IC ) = (Comput (p2,s2,i)) . (IC ) & (Comput (p1,s1,i)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) = (Comput (p2,s2,i)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) )
let i, k be Nat; for t being FinPartState of SCM+FSA
for p being Program of
for s1, s2 being State of SCM+FSA st k <= i & p c= p1 & p c= p2 & dom t c= Int-Locations \/ FinSeq-Locations & ( for j being Nat holds
( IC (Comput (p1,s1,j)) in dom p & IC (Comput (p2,s2,j)) in dom p ) ) & (Comput (p1,s1,k)) . (IC ) = (Comput (p2,s2,k)) . (IC ) & (Comput (p1,s1,k)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) = (Comput (p2,s2,k)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) holds
( (Comput (p1,s1,i)) . (IC ) = (Comput (p2,s2,i)) . (IC ) & (Comput (p1,s1,i)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) = (Comput (p2,s2,i)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) )
let t be FinPartState of SCM+FSA; for p being Program of
for s1, s2 being State of SCM+FSA st k <= i & p c= p1 & p c= p2 & dom t c= Int-Locations \/ FinSeq-Locations & ( for j being Nat holds
( IC (Comput (p1,s1,j)) in dom p & IC (Comput (p2,s2,j)) in dom p ) ) & (Comput (p1,s1,k)) . (IC ) = (Comput (p2,s2,k)) . (IC ) & (Comput (p1,s1,k)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) = (Comput (p2,s2,k)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) holds
( (Comput (p1,s1,i)) . (IC ) = (Comput (p2,s2,i)) . (IC ) & (Comput (p1,s1,i)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) = (Comput (p2,s2,i)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) )
let p be Program of ; for s1, s2 being State of SCM+FSA st k <= i & p c= p1 & p c= p2 & dom t c= Int-Locations \/ FinSeq-Locations & ( for j being Nat holds
( IC (Comput (p1,s1,j)) in dom p & IC (Comput (p2,s2,j)) in dom p ) ) & (Comput (p1,s1,k)) . (IC ) = (Comput (p2,s2,k)) . (IC ) & (Comput (p1,s1,k)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) = (Comput (p2,s2,k)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) holds
( (Comput (p1,s1,i)) . (IC ) = (Comput (p2,s2,i)) . (IC ) & (Comput (p1,s1,i)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) = (Comput (p2,s2,i)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) )
let s1, s2 be State of SCM+FSA; ( k <= i & p c= p1 & p c= p2 & dom t c= Int-Locations \/ FinSeq-Locations & ( for j being Nat holds
( IC (Comput (p1,s1,j)) in dom p & IC (Comput (p2,s2,j)) in dom p ) ) & (Comput (p1,s1,k)) . (IC ) = (Comput (p2,s2,k)) . (IC ) & (Comput (p1,s1,k)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) = (Comput (p2,s2,k)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) implies ( (Comput (p1,s1,i)) . (IC ) = (Comput (p2,s2,i)) . (IC ) & (Comput (p1,s1,i)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) = (Comput (p2,s2,i)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) ) )
set Dloc = ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p);
assume that
A1:
k <= i
and
A2:
p c= p1
and
A3:
p c= p2
and
A4:
dom t c= Int-Locations \/ FinSeq-Locations
and
A5:
for j being Nat holds
( IC (Comput (p1,s1,j)) in dom p & IC (Comput (p2,s2,j)) in dom p )
and
A6:
(Comput (p1,s1,k)) . (IC ) = (Comput (p2,s2,k)) . (IC )
and
A7:
(Comput (p1,s1,k)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) = (Comput (p2,s2,k)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))
; ( (Comput (p1,s1,i)) . (IC ) = (Comput (p2,s2,i)) . (IC ) & (Comput (p1,s1,i)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) = (Comput (p2,s2,i)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) )
consider m being Nat such that
A8:
i = k + m
by A1, NAT_1:10;
reconsider m = m as Nat ;
A9:
i = k + m
by A8;
A10:
UsedILoc p c= ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)
by XBOOLE_1:7;
((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) = ((dom t) \/ (UsedILoc p)) \/ (UsedI*Loc p)
by XBOOLE_1:4;
then A11:
UsedI*Loc p c= ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)
by XBOOLE_1:7;
defpred S1[ Nat] means ( (Comput (p1,s1,(k + $1))) . (IC ) = (Comput (p2,s2,(k + $1))) . (IC ) & (Comput (p1,s1,(k + $1))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) = (Comput (p2,s2,(k + $1))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) );
A12:
S1[ 0 ]
by A6, A7;
A13:
now for m being Nat st S1[m] holds
S1[m + 1]let m be
Nat;
( S1[m] implies S1[b1 + 1] )assume A14:
S1[
m]
;
S1[b1 + 1]set sk1 =
Comput (
p1,
s1,
(k + m));
set sk11 =
Comput (
p1,
s1,
(k + (m + 1)));
set i1 =
CurInstr (
p1,
(Comput (p1,s1,(k + m))));
set sk2 =
Comput (
p2,
s2,
(k + m));
set sk12 =
Comput (
p2,
s2,
(k + (m + 1)));
set i2 =
CurInstr (
p2,
(Comput (p2,s2,(k + m))));
A15:
IC (Comput (p1,s1,(k + m))) in dom p
by A5;
A16:
p2 /. (IC (Comput (p2,s2,(k + m)))) = p2 . (IC (Comput (p2,s2,(k + m))))
by PBOOLE:143;
A17:
p1 /. (IC (Comput (p1,s1,(k + m)))) = p1 . (IC (Comput (p1,s1,(k + m))))
by PBOOLE:143;
CurInstr (
p1,
(Comput (p1,s1,(k + m))))
= p . (IC (Comput (p1,s1,(k + m))))
by A2, A15, A17, GRFUNC_1:2;
then A18:
CurInstr (
p1,
(Comput (p1,s1,(k + m))))
in rng p
by A15, FUNCT_1:def 3;
A19:
CurInstr (
p2,
(Comput (p2,s2,(k + m)))) =
(p2 | (dom p)) . (IC (Comput (p2,s2,(k + m))))
by A16, A5, FUNCT_1:49
.=
(p1 | (dom p)) . (IC (Comput (p1,s1,(k + m))))
by A2, A3, A14, GRFUNC_1:33
.=
CurInstr (
p1,
(Comput (p1,s1,(k + m))))
by A17, A5, FUNCT_1:49
;
A20:
Comput (
p1,
s1,
(k + (m + 1))) =
Comput (
p1,
s1,
((k + m) + 1))
.=
Following (
p1,
(Comput (p1,s1,(k + m))))
by EXTPRO_1:3
.=
Exec (
(CurInstr (p1,(Comput (p1,s1,(k + m))))),
(Comput (p1,s1,(k + m))))
;
A21:
Comput (
p2,
s2,
(k + (m + 1))) =
Comput (
p2,
s2,
((k + m) + 1))
.=
Following (
p2,
(Comput (p2,s2,(k + m))))
by EXTPRO_1:3
.=
Exec (
(CurInstr (p2,(Comput (p2,s2,(k + m))))),
(Comput (p2,s2,(k + m))))
;
A22:
dom (Comput (p1,s1,(k + (m + 1)))) =
the
carrier of
SCM+FSA
by PARTFUN1:def 2
.=
dom (Comput (p2,s2,(k + (m + 1))))
by PARTFUN1:def 2
;
not not
InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 0 & ... & not
InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 12
by SCMFSA_2:16;
per cases then
( InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 0 or InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 1 or InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 2 or InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 3 or InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 4 or InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 5 or InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 6 or InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 7 or InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 8 or InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 9 or InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 10 or InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 11 or InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 12 )
;
suppose
InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 0
;
S1[b1 + 1]then A23:
CurInstr (
p1,
(Comput (p1,s1,(k + m))))
= halt SCM+FSA
by SCMFSA_2:95;
then
Comput (
p1,
s1,
(k + (m + 1)))
= Comput (
p1,
s1,
(k + m))
by A20, EXTPRO_1:def 3;
hence
S1[
m + 1]
by A14, A19, A21, A23, EXTPRO_1:def 3;
verum end; suppose
InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 1
;
S1[b1 + 1]then consider da,
db being
Int-Location such that A24:
CurInstr (
p1,
(Comput (p1,s1,(k + m))))
= da := db
by SCMFSA_2:30;
A25:
(Comput (p1,s1,(k + (m + 1)))) . (IC ) =
(IC (Comput (p1,s1,(k + m)))) + 1
by A20, A24, SCMFSA_2:63
.=
(Comput (p2,s2,(k + (m + 1)))) . (IC )
by A14, A19, A21, A24, SCMFSA_2:63
;
now for x being set st x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) holds
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . xlet x be
set ;
( x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) implies (Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1 )assume A26:
x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1per cases
( x is Int-Location or x is FinSeq-Location )
by A4, A26, Th12;
suppose A27:
x is
Int-Location
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1per cases
( x = da or x <> da )
;
suppose A28:
x = da
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1then A29:
(Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . db
by A19, A21, A24, SCMFSA_2:63;
A30:
db in UsedILoc p
by A18, A24, Th6;
then (Comput (p1,s1,(k + m))) . db =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . db
by A10, A14, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . db
by A10, A30, FUNCT_1:49
;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A20, A24, A28, A29, SCMFSA_2:63;
verum end; suppose A31:
x <> da
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1then A32:
(Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x
by A19, A21, A24, A27, SCMFSA_2:63;
(Comput (p1,s1,(k + m))) . x =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x
by A14, A26, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . x
by A26, FUNCT_1:49
;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A20, A24, A27, A31, A32, SCMFSA_2:63;
verum end; end; end; suppose A33:
x is
FinSeq-Location
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1then A34:
(Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x
by A19, A21, A24, SCMFSA_2:63;
(Comput (p1,s1,(k + m))) . x =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x
by A14, A26, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . x
by A26, FUNCT_1:49
;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A20, A24, A33, A34, SCMFSA_2:63;
verum end; end; end; hence
S1[
m + 1]
by A22, A25, FUNCT_1:96;
verum end; suppose
InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 2
;
S1[b1 + 1]then consider da,
db being
Int-Location such that A35:
CurInstr (
p1,
(Comput (p1,s1,(k + m))))
= AddTo (
da,
db)
by SCMFSA_2:31;
A36:
(Comput (p1,s1,(k + (m + 1)))) . (IC ) =
(IC (Comput (p1,s1,(k + m)))) + 1
by A20, A35, SCMFSA_2:64
.=
(Comput (p2,s2,(k + (m + 1)))) . (IC )
by A14, A19, A21, A35, SCMFSA_2:64
;
now for x being set st x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) holds
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . xlet x be
set ;
( x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) implies (Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1 )assume A37:
x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1per cases
( x is Int-Location or x is FinSeq-Location )
by A4, A37, Th12;
suppose A38:
x is
Int-Location
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1per cases
( x = da or x <> da )
;
suppose A39:
x = da
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1then A40:
(Comput (p2,s2,(k + (m + 1)))) . x = ((Comput (p2,s2,(k + m))) . da) + ((Comput (p2,s2,(k + m))) . db)
by A19, A21, A35, SCMFSA_2:64;
A41:
da in UsedILoc p
by A18, A35, Th6;
then A42:
(Comput (p1,s1,(k + m))) . da =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . da
by A10, A14, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . da
by A10, A41, FUNCT_1:49
;
A43:
db in UsedILoc p
by A18, A35, Th6;
then (Comput (p1,s1,(k + m))) . db =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . db
by A10, A14, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . db
by A10, A43, FUNCT_1:49
;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A20, A35, A39, A40, A42, SCMFSA_2:64;
verum end; suppose A44:
x <> da
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1then A45:
(Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x
by A19, A21, A35, A38, SCMFSA_2:64;
(Comput (p1,s1,(k + m))) . x =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x
by A14, A37, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . x
by A37, FUNCT_1:49
;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A20, A35, A38, A44, A45, SCMFSA_2:64;
verum end; end; end; suppose A46:
x is
FinSeq-Location
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1then A47:
(Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x
by A19, A21, A35, SCMFSA_2:64;
(Comput (p1,s1,(k + m))) . x =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x
by A14, A37, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . x
by A37, FUNCT_1:49
;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A20, A35, A46, A47, SCMFSA_2:64;
verum end; end; end; hence
S1[
m + 1]
by A22, A36, FUNCT_1:96;
verum end; suppose
InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 3
;
S1[b1 + 1]then consider da,
db being
Int-Location such that A48:
CurInstr (
p1,
(Comput (p1,s1,(k + m))))
= SubFrom (
da,
db)
by SCMFSA_2:32;
A49:
(Comput (p1,s1,(k + (m + 1)))) . (IC ) =
(IC (Comput (p1,s1,(k + m)))) + 1
by A20, A48, SCMFSA_2:65
.=
(Comput (p2,s2,(k + (m + 1)))) . (IC )
by A14, A19, A21, A48, SCMFSA_2:65
;
now for x being set st x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) holds
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . xlet x be
set ;
( x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) implies (Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1 )assume A50:
x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1per cases
( x is Int-Location or x is FinSeq-Location )
by A4, A50, Th12;
suppose A51:
x is
Int-Location
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1per cases
( x = da or x <> da )
;
suppose A52:
x = da
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1then A53:
(Comput (p2,s2,(k + (m + 1)))) . x = ((Comput (p2,s2,(k + m))) . da) - ((Comput (p2,s2,(k + m))) . db)
by A19, A21, A48, SCMFSA_2:65;
A54:
da in UsedILoc p
by A18, A48, Th6;
then A55:
(Comput (p1,s1,(k + m))) . da =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . da
by A10, A14, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . da
by A10, A54, FUNCT_1:49
;
A56:
db in UsedILoc p
by A18, A48, Th6;
then (Comput (p1,s1,(k + m))) . db =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . db
by A10, A14, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . db
by A10, A56, FUNCT_1:49
;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A20, A48, A52, A53, A55, SCMFSA_2:65;
verum end; suppose A57:
x <> da
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1then A58:
(Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x
by A19, A21, A48, A51, SCMFSA_2:65;
(Comput (p1,s1,(k + m))) . x =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x
by A14, A50, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . x
by A50, FUNCT_1:49
;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A20, A48, A51, A57, A58, SCMFSA_2:65;
verum end; end; end; suppose A59:
x is
FinSeq-Location
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1then A60:
(Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x
by A19, A21, A48, SCMFSA_2:65;
(Comput (p1,s1,(k + m))) . x =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x
by A14, A50, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . x
by A50, FUNCT_1:49
;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A20, A48, A59, A60, SCMFSA_2:65;
verum end; end; end; hence
S1[
m + 1]
by A22, A49, FUNCT_1:96;
verum end; suppose
InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 4
;
S1[b1 + 1]then consider da,
db being
Int-Location such that A61:
CurInstr (
p1,
(Comput (p1,s1,(k + m))))
= MultBy (
da,
db)
by SCMFSA_2:33;
A62:
(Comput (p1,s1,(k + (m + 1)))) . (IC ) =
(IC (Comput (p1,s1,(k + m)))) + 1
by A20, A61, SCMFSA_2:66
.=
(Comput (p2,s2,(k + (m + 1)))) . (IC )
by A14, A19, A21, A61, SCMFSA_2:66
;
now for x being set st x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) holds
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . xlet x be
set ;
( x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) implies (Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1 )assume A63:
x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1per cases
( x is Int-Location or x is FinSeq-Location )
by A4, A63, Th12;
suppose A64:
x is
Int-Location
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1per cases
( x = da or x <> da )
;
suppose A65:
x = da
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1then A66:
(Comput (p2,s2,(k + (m + 1)))) . x = ((Comput (p2,s2,(k + m))) . da) * ((Comput (p2,s2,(k + m))) . db)
by A19, A21, A61, SCMFSA_2:66;
A67:
da in UsedILoc p
by A18, A61, Th6;
then A68:
(Comput (p1,s1,(k + m))) . da =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . da
by A10, A14, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . da
by A10, A67, FUNCT_1:49
;
A69:
db in UsedILoc p
by A18, A61, Th6;
then (Comput (p1,s1,(k + m))) . db =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . db
by A10, A14, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . db
by A10, A69, FUNCT_1:49
;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A20, A61, A65, A66, A68, SCMFSA_2:66;
verum end; suppose A70:
x <> da
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1then A71:
(Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x
by A19, A21, A61, A64, SCMFSA_2:66;
(Comput (p1,s1,(k + m))) . x =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x
by A14, A63, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . x
by A63, FUNCT_1:49
;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A20, A61, A64, A70, A71, SCMFSA_2:66;
verum end; end; end; suppose A72:
x is
FinSeq-Location
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1then A73:
(Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x
by A19, A21, A61, SCMFSA_2:66;
(Comput (p1,s1,(k + m))) . x =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x
by A14, A63, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . x
by A63, FUNCT_1:49
;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A20, A61, A72, A73, SCMFSA_2:66;
verum end; end; end; hence
S1[
m + 1]
by A22, A62, FUNCT_1:96;
verum end; suppose
InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 5
;
S1[b1 + 1]then consider da,
db being
Int-Location such that A74:
CurInstr (
p1,
(Comput (p1,s1,(k + m))))
= Divide (
da,
db)
by SCMFSA_2:34;
A75:
(Comput (p1,s1,(k + (m + 1)))) . (IC ) =
(IC (Comput (p1,s1,(k + m)))) + 1
by A20, A74, SCMFSA_2:67
.=
(Comput (p2,s2,(k + (m + 1)))) . (IC )
by A14, A19, A21, A74, SCMFSA_2:67
;
now for x being set st x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) holds
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . xlet x be
set ;
( x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) implies (Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1 )assume A76:
x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1per cases
( x is Int-Location or x is FinSeq-Location )
by A4, A76, Th12;
suppose A77:
x is
Int-Location
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1A78:
da in UsedILoc p
by A18, A74, Th6;
then A79:
(Comput (p1,s1,(k + m))) . da =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . da
by A10, A14, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . da
by A10, A78, FUNCT_1:49
;
A80:
db in UsedILoc p
by A18, A74, Th6;
then A81:
(Comput (p1,s1,(k + m))) . db =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . db
by A10, A14, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . db
by A10, A80, FUNCT_1:49
;
A82:
(Comput (p1,s1,(k + m))) . x =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x
by A14, A76, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . x
by A76, FUNCT_1:49
;
now (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . xper cases
( da <> db or da = db )
;
suppose A83:
da <> db
;
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . xper cases
( x = da or x = db or ( x <> da & x <> db ) )
;
suppose A84:
x = da
;
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . xthen
(Comput (p1,s1,(k + (m + 1)))) . x = ((Comput (p1,s1,(k + m))) . da) div ((Comput (p1,s1,(k + m))) . db)
by A20, A74, A83, SCMFSA_2:67;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A19, A21, A74, A79, A81, A83, A84, SCMFSA_2:67;
verum end; suppose A85:
x = db
;
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . xthen
(Comput (p1,s1,(k + (m + 1)))) . x = ((Comput (p1,s1,(k + m))) . da) mod ((Comput (p1,s1,(k + m))) . db)
by A20, A74, SCMFSA_2:67;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A19, A21, A74, A79, A81, A85, SCMFSA_2:67;
verum end; suppose A86:
(
x <> da &
x <> db )
;
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . xthen
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p1,s1,(k + m))) . x
by A20, A74, A77, SCMFSA_2:67;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A19, A21, A74, A77, A82, A86, SCMFSA_2:67;
verum end; end; end; suppose A87:
da = db
;
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . xnow ( ( x = da & (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x ) or ( x <> da & (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x ) )per cases
( x = da or x <> da )
;
case A88:
x = da
;
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . xthen
(Comput (p1,s1,(k + (m + 1)))) . x = ((Comput (p1,s1,(k + m))) . da) mod ((Comput (p1,s1,(k + m))) . da)
by A20, A74, A87, SCMFSA_2:68;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A19, A21, A74, A79, A87, A88, SCMFSA_2:68;
verum end; case A89:
x <> da
;
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . xthen
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p1,s1,(k + m))) . x
by A20, A74, A77, A87, SCMFSA_2:68;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A19, A21, A74, A77, A82, A87, A89, SCMFSA_2:68;
verum end; end; end; hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
;
verum end; end; end; hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
;
verum end; suppose A90:
x is
FinSeq-Location
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1then A91:
(Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x
by A19, A21, A74, SCMFSA_2:67;
(Comput (p1,s1,(k + m))) . x =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x
by A14, A76, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . x
by A76, FUNCT_1:49
;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A20, A74, A90, A91, SCMFSA_2:67;
verum end; end; end; hence
S1[
m + 1]
by A22, A75, FUNCT_1:96;
verum end; suppose
InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 6
;
S1[b1 + 1]then consider lb being
Nat such that A92:
CurInstr (
p1,
(Comput (p1,s1,(k + m))))
= goto lb
by SCMFSA_2:35;
A93:
(Comput (p1,s1,(k + (m + 1)))) . (IC ) =
lb
by A20, A92, SCMFSA_2:69
.=
(Comput (p2,s2,(k + (m + 1)))) . (IC )
by A19, A21, A92, SCMFSA_2:69
;
now for x being set st x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) holds
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . xlet x be
set ;
( x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) implies (Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1 )assume A94:
x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1then A95:
(Comput (p1,s1,(k + m))) . x =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x
by A14, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . x
by A94, FUNCT_1:49
;
per cases
( x is Int-Location or x is FinSeq-Location )
by A4, A94, Th12;
suppose A96:
x is
Int-Location
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1then
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p1,s1,(k + m))) . x
by A20, A92, SCMFSA_2:69;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A19, A21, A92, A95, A96, SCMFSA_2:69;
verum end; suppose A97:
x is
FinSeq-Location
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1then
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p1,s1,(k + m))) . x
by A20, A92, SCMFSA_2:69;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A19, A21, A92, A95, A97, SCMFSA_2:69;
verum end; end; end; hence
S1[
m + 1]
by A22, A93, FUNCT_1:96;
verum end; suppose
InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 7
;
S1[b1 + 1]then consider lb being
Nat,
da being
Int-Location such that A98:
CurInstr (
p1,
(Comput (p1,s1,(k + m))))
= da =0_goto lb
by SCMFSA_2:36;
A99:
da in UsedILoc p
by A18, A98, Th7;
then A100:
(Comput (p1,s1,(k + m))) . da =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . da
by A10, A14, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . da
by A10, A99, FUNCT_1:49
;
A101:
now (Comput (p1,s1,(k + (m + 1)))) . (IC ) = (Comput (p2,s2,(k + (m + 1)))) . (IC )per cases
( (Comput (p1,s1,(k + m))) . da = 0 or (Comput (p1,s1,(k + m))) . da <> 0 )
;
suppose A102:
(Comput (p1,s1,(k + m))) . da = 0
;
(Comput (p1,s1,(k + (m + 1)))) . (IC ) = (Comput (p2,s2,(k + (m + 1)))) . (IC )hence (Comput (p1,s1,(k + (m + 1)))) . (IC ) =
lb
by A20, A98, SCMFSA_2:70
.=
(Comput (p2,s2,(k + (m + 1)))) . (IC )
by A19, A21, A98, A100, A102, SCMFSA_2:70
;
verum end; suppose A103:
(Comput (p1,s1,(k + m))) . da <> 0
;
(Comput (p1,s1,(k + (m + 1)))) . (IC ) = (Comput (p2,s2,(k + (m + 1)))) . (IC )hence (Comput (p1,s1,(k + (m + 1)))) . (IC ) =
(IC (Comput (p2,s2,(k + m)))) + 1
by A14, A20, A98, SCMFSA_2:70
.=
(Comput (p2,s2,(k + (m + 1)))) . (IC )
by A19, A21, A98, A100, A103, SCMFSA_2:70
;
verum end; end; end; now for x being set st x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) holds
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . xlet x be
set ;
( x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) implies (Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1 )assume A104:
x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1then A105:
(Comput (p1,s1,(k + m))) . x =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x
by A14, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . x
by A104, FUNCT_1:49
;
per cases
( x is Int-Location or x is FinSeq-Location )
by A4, A104, Th12;
suppose A106:
x is
Int-Location
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1then
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p1,s1,(k + m))) . x
by A20, A98, SCMFSA_2:70;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A19, A21, A98, A105, A106, SCMFSA_2:70;
verum end; suppose A107:
x is
FinSeq-Location
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1then
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p1,s1,(k + m))) . x
by A20, A98, SCMFSA_2:70;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A19, A21, A98, A105, A107, SCMFSA_2:70;
verum end; end; end; hence
S1[
m + 1]
by A22, A101, FUNCT_1:96;
verum end; suppose
InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 8
;
S1[b1 + 1]then consider lb being
Nat,
da being
Int-Location such that A108:
CurInstr (
p1,
(Comput (p1,s1,(k + m))))
= da >0_goto lb
by SCMFSA_2:37;
A109:
da in UsedILoc p
by A18, A108, Th7;
then A110:
(Comput (p1,s1,(k + m))) . da =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . da
by A10, A14, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . da
by A10, A109, FUNCT_1:49
;
A111:
now (Comput (p1,s1,(k + (m + 1)))) . (IC ) = (Comput (p2,s2,(k + (m + 1)))) . (IC )per cases
( (Comput (p1,s1,(k + m))) . da > 0 or (Comput (p1,s1,(k + m))) . da <= 0 )
;
suppose A112:
(Comput (p1,s1,(k + m))) . da > 0
;
(Comput (p1,s1,(k + (m + 1)))) . (IC ) = (Comput (p2,s2,(k + (m + 1)))) . (IC )hence (Comput (p1,s1,(k + (m + 1)))) . (IC ) =
lb
by A20, A108, SCMFSA_2:71
.=
(Comput (p2,s2,(k + (m + 1)))) . (IC )
by A19, A21, A108, A110, A112, SCMFSA_2:71
;
verum end; suppose A113:
(Comput (p1,s1,(k + m))) . da <= 0
;
(Comput (p1,s1,(k + (m + 1)))) . (IC ) = (Comput (p2,s2,(k + (m + 1)))) . (IC )hence (Comput (p1,s1,(k + (m + 1)))) . (IC ) =
(IC (Comput (p2,s2,(k + m)))) + 1
by A14, A20, A108, SCMFSA_2:71
.=
(Comput (p2,s2,(k + (m + 1)))) . (IC )
by A19, A21, A108, A110, A113, SCMFSA_2:71
;
verum end; end; end; now for x being set st x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) holds
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . xlet x be
set ;
( x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) implies (Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1 )assume A114:
x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1then A115:
(Comput (p1,s1,(k + m))) . x =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x
by A14, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . x
by A114, FUNCT_1:49
;
per cases
( x is Int-Location or x is FinSeq-Location )
by A4, A114, Th12;
suppose A116:
x is
Int-Location
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1then
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p1,s1,(k + m))) . x
by A20, A108, SCMFSA_2:71;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A19, A21, A108, A115, A116, SCMFSA_2:71;
verum end; suppose A117:
x is
FinSeq-Location
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1then
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p1,s1,(k + m))) . x
by A20, A108, SCMFSA_2:71;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A19, A21, A108, A115, A117, SCMFSA_2:71;
verum end; end; end; hence
S1[
m + 1]
by A22, A111, FUNCT_1:96;
verum end; suppose
InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 9
;
S1[b1 + 1]then consider a,
b being
Int-Location,
fa being
FinSeq-Location such that A118:
CurInstr (
p1,
(Comput (p1,s1,(k + m))))
= b := (
fa,
a)
by SCMFSA_2:38;
A119:
(Comput (p1,s1,(k + (m + 1)))) . (IC ) =
(IC (Comput (p2,s2,(k + m)))) + 1
by A14, A20, A118, SCMFSA_2:72
.=
(Comput (p2,s2,(k + (m + 1)))) . (IC )
by A19, A21, A118, SCMFSA_2:72
;
now for x being set st x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) holds
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . xlet x be
set ;
( x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) implies (Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1 )assume A120:
x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1per cases
( x is Int-Location or x is FinSeq-Location )
by A4, A120, Th12;
suppose A121:
x is
Int-Location
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1per cases
( x = b or x <> b )
;
suppose A122:
x = b
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1A123:
ex
k1 being
Nat st
(
k1 = |.((Comput (p1,s1,(k + m))) . a).| &
(Exec ((b := (fa,a)),(Comput (p1,s1,(k + m))))) . b = ((Comput (p1,s1,(k + m))) . fa) /. k1 )
by SCMFSA_2:72;
A124:
ex
k2 being
Nat st
(
k2 = |.((Comput (p2,s2,(k + m))) . a).| &
(Exec ((b := (fa,a)),(Comput (p2,s2,(k + m))))) . b = ((Comput (p2,s2,(k + m))) . fa) /. k2 )
by SCMFSA_2:72;
A125:
a in UsedILoc p
by A18, A118, Th8;
then A126:
(Comput (p1,s1,(k + m))) . a =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . a
by A10, A14, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . a
by A10, A125, FUNCT_1:49
;
A127:
fa in UsedI*Loc p
by A18, A118, Th9;
then (Comput (p1,s1,(k + m))) . fa =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . fa
by A11, A14, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . fa
by A11, A127, FUNCT_1:49
;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A19, A20, A21, A118, A122, A123, A124, A126;
verum end; suppose A128:
x <> b
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1then A129:
(Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x
by A19, A21, A118, A121, SCMFSA_2:72;
(Comput (p1,s1,(k + m))) . x =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x
by A14, A120, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . x
by A120, FUNCT_1:49
;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A20, A118, A121, A128, A129, SCMFSA_2:72;
verum end; end; end; suppose A130:
x is
FinSeq-Location
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1then A131:
(Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x
by A19, A21, A118, SCMFSA_2:72;
(Comput (p1,s1,(k + m))) . x =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x
by A14, A120, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . x
by A120, FUNCT_1:49
;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A20, A118, A130, A131, SCMFSA_2:72;
verum end; end; end; hence
S1[
m + 1]
by A22, A119, FUNCT_1:96;
verum end; suppose
InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 10
;
S1[b1 + 1]then consider a,
b being
Int-Location,
fa being
FinSeq-Location such that A132:
CurInstr (
p1,
(Comput (p1,s1,(k + m))))
= (
fa,
a)
:= b
by SCMFSA_2:39;
A133:
(Comput (p1,s1,(k + (m + 1)))) . (IC ) =
(IC (Comput (p2,s2,(k + m)))) + 1
by A14, A20, A132, SCMFSA_2:73
.=
(Comput (p2,s2,(k + (m + 1)))) . (IC )
by A19, A21, A132, SCMFSA_2:73
;
now for x being set st x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) holds
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . xlet x be
set ;
( x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) implies (Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1 )assume A134:
x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1per cases
( x is FinSeq-Location or x is Int-Location )
by A4, A134, Th12;
suppose A135:
x is
FinSeq-Location
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1per cases
( x = fa or x <> fa )
;
suppose A136:
x = fa
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1A137:
ex
k1 being
Nat st
(
k1 = |.((Comput (p1,s1,(k + m))) . a).| &
(Exec (((fa,a) := b),(Comput (p1,s1,(k + m))))) . fa = ((Comput (p1,s1,(k + m))) . fa) +* (
k1,
((Comput (p1,s1,(k + m))) . b)) )
by SCMFSA_2:73;
A138:
ex
k2 being
Nat st
(
k2 = |.((Comput (p2,s2,(k + m))) . a).| &
(Exec (((fa,a) := b),(Comput (p2,s2,(k + m))))) . fa = ((Comput (p2,s2,(k + m))) . fa) +* (
k2,
((Comput (p2,s2,(k + m))) . b)) )
by SCMFSA_2:73;
A139:
a in UsedILoc p
by A18, A132, Th8;
then A140:
(Comput (p1,s1,(k + m))) . a =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . a
by A10, A14, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . a
by A10, A139, FUNCT_1:49
;
A141:
b in UsedILoc p
by A18, A132, Th8;
then A142:
(Comput (p1,s1,(k + m))) . b =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . b
by A10, A14, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . b
by A10, A141, FUNCT_1:49
;
A143:
fa in UsedI*Loc p
by A18, A132, Th9;
then (Comput (p1,s1,(k + m))) . fa =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . fa
by A11, A14, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . fa
by A11, A143, FUNCT_1:49
;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A19, A20, A21, A132, A136, A137, A138, A140, A142;
verum end; suppose A144:
x <> fa
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1then A145:
(Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x
by A19, A21, A132, A135, SCMFSA_2:73;
(Comput (p1,s1,(k + m))) . x =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x
by A14, A134, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . x
by A134, FUNCT_1:49
;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A20, A132, A135, A144, A145, SCMFSA_2:73;
verum end; end; end; suppose A146:
x is
Int-Location
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1then A147:
(Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x
by A19, A21, A132, SCMFSA_2:73;
(Comput (p1,s1,(k + m))) . x =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x
by A14, A134, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . x
by A134, FUNCT_1:49
;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A20, A132, A146, A147, SCMFSA_2:73;
verum end; end; end; hence
S1[
m + 1]
by A22, A133, FUNCT_1:96;
verum end; suppose
InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 11
;
S1[b1 + 1]then consider a being
Int-Location,
fa being
FinSeq-Location such that A148:
CurInstr (
p1,
(Comput (p1,s1,(k + m))))
= a :=len fa
by SCMFSA_2:40;
A149:
(Comput (p1,s1,(k + (m + 1)))) . (IC ) =
(IC (Comput (p2,s2,(k + m)))) + 1
by A14, A20, A148, SCMFSA_2:74
.=
(Comput (p2,s2,(k + (m + 1)))) . (IC )
by A19, A21, A148, SCMFSA_2:74
;
now for x being set st x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) holds
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . xlet x be
set ;
( x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) implies (Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1 )assume A150:
x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1per cases
( x is Int-Location or x is FinSeq-Location )
by A4, A150, Th12;
suppose A151:
x is
Int-Location
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1per cases
( x = a or x <> a )
;
suppose A152:
x = a
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1then A153:
(Comput (p2,s2,(k + (m + 1)))) . x = len ((Comput (p2,s2,(k + m))) . fa)
by A19, A21, A148, SCMFSA_2:74;
A154:
fa in UsedI*Loc p
by A18, A148, Th11;
then (Comput (p1,s1,(k + m))) . fa =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . fa
by A11, A14, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . fa
by A11, A154, FUNCT_1:49
;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A20, A148, A152, A153, SCMFSA_2:74;
verum end; suppose A155:
x <> a
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1then A156:
(Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x
by A19, A21, A148, A151, SCMFSA_2:74;
(Comput (p1,s1,(k + m))) . x =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x
by A14, A150, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . x
by A150, FUNCT_1:49
;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A20, A148, A151, A155, A156, SCMFSA_2:74;
verum end; end; end; suppose A157:
x is
FinSeq-Location
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1then A158:
(Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x
by A19, A21, A148, SCMFSA_2:74;
(Comput (p1,s1,(k + m))) . x =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x
by A14, A150, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . x
by A150, FUNCT_1:49
;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A20, A148, A157, A158, SCMFSA_2:74;
verum end; end; end; hence
S1[
m + 1]
by A22, A149, FUNCT_1:96;
verum end; suppose
InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 12
;
S1[b1 + 1]then consider a being
Int-Location,
fa being
FinSeq-Location such that A159:
CurInstr (
p1,
(Comput (p1,s1,(k + m))))
= fa :=<0,...,0> a
by SCMFSA_2:41;
A160:
(Comput (p1,s1,(k + (m + 1)))) . (IC ) =
(IC (Comput (p2,s2,(k + m)))) + 1
by A14, A20, A159, SCMFSA_2:75
.=
(Comput (p2,s2,(k + (m + 1)))) . (IC )
by A19, A21, A159, SCMFSA_2:75
;
now for x being set st x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) holds
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . xlet x be
set ;
( x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) implies (Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1 )assume A161:
x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1per cases
( x is FinSeq-Location or x is Int-Location )
by A4, A161, Th12;
suppose A162:
x is
FinSeq-Location
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1per cases
( x = fa or x <> fa )
;
suppose A163:
x = fa
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1A164:
ex
k1 being
Nat st
(
k1 = |.((Comput (p1,s1,(k + m))) . a).| &
(Exec ((fa :=<0,...,0> a),(Comput (p1,s1,(k + m))))) . fa = k1 |-> 0 )
by SCMFSA_2:75;
A165:
ex
k2 being
Nat st
(
k2 = |.((Comput (p2,s2,(k + m))) . a).| &
(Exec ((fa :=<0,...,0> a),(Comput (p2,s2,(k + m))))) . fa = k2 |-> 0 )
by SCMFSA_2:75;
A166:
a in UsedILoc p
by A18, A159, Th10;
then (Comput (p1,s1,(k + m))) . a =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . a
by A10, A14, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . a
by A10, A166, FUNCT_1:49
;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A19, A20, A21, A159, A163, A164, A165;
verum end; suppose A167:
x <> fa
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1then A168:
(Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x
by A19, A21, A159, A162, SCMFSA_2:75;
(Comput (p1,s1,(k + m))) . x =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x
by A14, A161, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . x
by A161, FUNCT_1:49
;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A20, A159, A162, A167, A168, SCMFSA_2:75;
verum end; end; end; suppose A169:
x is
Int-Location
;
(Comput (p1,s1,(k + (m + 1)))) . b1 = (Comput (p2,s2,(k + (m + 1)))) . b1then A170:
(Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x
by A19, A21, A159, SCMFSA_2:75;
(Comput (p1,s1,(k + m))) . x =
((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x
by A14, A161, FUNCT_1:49
.=
(Comput (p2,s2,(k + m))) . x
by A161, FUNCT_1:49
;
hence
(Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x
by A20, A159, A169, A170, SCMFSA_2:75;
verum end; end; end; hence
S1[
m + 1]
by A22, A160, FUNCT_1:96;
verum end; end; end;
for m being Nat holds S1[m]
from NAT_1:sch 2(A12, A13);
hence
( (Comput (p1,s1,i)) . (IC ) = (Comput (p2,s2,i)) . (IC ) & (Comput (p1,s1,i)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) = (Comput (p2,s2,i)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) )
by A9; verum