let p1, p2 be Instruction-Sequence of SCM+FSA; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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)) ; :: thesis: ( (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; :: thesis: (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; :: thesis: verum