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