let p1, p2 be Instruction-Sequence of SCM+FSA; for i, k being Nat
for p being Program of
for s1, s2 being State of SCM+FSA st k <= i & p c= p1 & p c= p2 & ( 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)) | ((UsedI*Loc p) \/ (UsedILoc p)) = (Comput (p2,s2,k)) | ((UsedI*Loc p) \/ (UsedILoc p)) holds
( (Comput (p1,s1,i)) . (IC ) = (Comput (p2,s2,i)) . (IC ) & (Comput (p1,s1,i)) | ((UsedI*Loc p) \/ (UsedILoc p)) = (Comput (p2,s2,i)) | ((UsedI*Loc p) \/ (UsedILoc p)) )
let i, k be Nat; for p being Program of
for s1, s2 being State of SCM+FSA st k <= i & p c= p1 & p c= p2 & ( 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)) | ((UsedI*Loc p) \/ (UsedILoc p)) = (Comput (p2,s2,k)) | ((UsedI*Loc p) \/ (UsedILoc p)) holds
( (Comput (p1,s1,i)) . (IC ) = (Comput (p2,s2,i)) . (IC ) & (Comput (p1,s1,i)) | ((UsedI*Loc p) \/ (UsedILoc p)) = (Comput (p2,s2,i)) | ((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 & ( 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)) | ((UsedI*Loc p) \/ (UsedILoc p)) = (Comput (p2,s2,k)) | ((UsedI*Loc p) \/ (UsedILoc p)) holds
( (Comput (p1,s1,i)) . (IC ) = (Comput (p2,s2,i)) . (IC ) & (Comput (p1,s1,i)) | ((UsedI*Loc p) \/ (UsedILoc p)) = (Comput (p2,s2,i)) | ((UsedI*Loc p) \/ (UsedILoc p)) )
let s1, s2 be State of SCM+FSA; ( k <= i & p c= p1 & p c= p2 & ( 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)) | ((UsedI*Loc p) \/ (UsedILoc p)) = (Comput (p2,s2,k)) | ((UsedI*Loc p) \/ (UsedILoc p)) implies ( (Comput (p1,s1,i)) . (IC ) = (Comput (p2,s2,i)) . (IC ) & (Comput (p1,s1,i)) | ((UsedI*Loc p) \/ (UsedILoc p)) = (Comput (p2,s2,i)) | ((UsedI*Loc p) \/ (UsedILoc p)) ) )
set D = (UsedI*Loc p) \/ (UsedILoc p);
assume that
A1:
k <= i
and
A2:
p c= p1
and
A3:
p c= p2
and
A4:
for j being Nat holds
( IC (Comput (p1,s1,j)) in dom p & IC (Comput (p2,s2,j)) in dom p )
and
A5:
(Comput (p1,s1,k)) . (IC ) = (Comput (p2,s2,k)) . (IC )
and
A6:
(Comput (p1,s1,k)) | ((UsedI*Loc p) \/ (UsedILoc p)) = (Comput (p2,s2,k)) | ((UsedI*Loc p) \/ (UsedILoc p))
; ( (Comput (p1,s1,i)) . (IC ) = (Comput (p2,s2,i)) . (IC ) & (Comput (p1,s1,i)) | ((UsedI*Loc p) \/ (UsedILoc p)) = (Comput (p2,s2,i)) | ((UsedI*Loc p) \/ (UsedILoc p)) )
reconsider t = {} as PartState of SCM+FSA by FUNCT_1:104, RELAT_1:171;
set D1 = ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p);
A7:
dom t c= Int-Locations \/ FinSeq-Locations
by RELAT_1:38, XBOOLE_1:2;
A8:
((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) = (UsedI*Loc p) \/ (UsedILoc p)
by RELAT_1:38;
hence
(Comput (p1,s1,i)) . (IC ) = (Comput (p2,s2,i)) . (IC )
by A1, A2, A3, A4, A5, A6, A7, Th13; (Comput (p1,s1,i)) | ((UsedI*Loc p) \/ (UsedILoc p)) = (Comput (p2,s2,i)) | ((UsedI*Loc p) \/ (UsedILoc p))
thus
(Comput (p1,s1,i)) | ((UsedI*Loc p) \/ (UsedILoc p)) = (Comput (p2,s2,i)) | ((UsedI*Loc p) \/ (UsedILoc p))
by A1, A2, A3, A4, A5, A6, A7, A8, Th13; verum