let i, k be Element of NAT ; :: thesis: for p being Program of {INT,(INT *)}
for s1, s2 being State of SCM+FSA st k <= i & p c= s1 & p c= s2 & ( for j being Element of NAT holds
( IC (Comput ((ProgramPart s1),s1,j)) in dom p & IC (Comput ((ProgramPart s2),s2,j)) in dom p ) ) & (Comput ((ProgramPart s1),s1,k)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,k)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,k)) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) = (Comput ((ProgramPart s2),s2,k)) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) holds
( (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,i)) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) = (Comput ((ProgramPart s2),s2,i)) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) )
let p be Program of {INT,(INT *)}; :: thesis: for s1, s2 being State of SCM+FSA st k <= i & p c= s1 & p c= s2 & ( for j being Element of NAT holds
( IC (Comput ((ProgramPart s1),s1,j)) in dom p & IC (Comput ((ProgramPart s2),s2,j)) in dom p ) ) & (Comput ((ProgramPart s1),s1,k)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,k)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,k)) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) = (Comput ((ProgramPart s2),s2,k)) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) holds
( (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,i)) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) = (Comput ((ProgramPart s2),s2,i)) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) )
let s1, s2 be State of SCM+FSA; :: thesis: ( k <= i & p c= s1 & p c= s2 & ( for j being Element of NAT holds
( IC (Comput ((ProgramPart s1),s1,j)) in dom p & IC (Comput ((ProgramPart s2),s2,j)) in dom p ) ) & (Comput ((ProgramPart s1),s1,k)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,k)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,k)) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) = (Comput ((ProgramPart s2),s2,k)) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) implies ( (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,i)) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) = (Comput ((ProgramPart s2),s2,i)) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) ) )
set D = (UsedInt*Loc p) \/ (UsedIntLoc p);
assume that
A1: k <= i and
A2: p c= s1 and
A3: p c= s2 and
A4: for j being Element of NAT holds
( IC (Comput ((ProgramPart s1),s1,j)) in dom p & IC (Comput ((ProgramPart s2),s2,j)) in dom p ) and
A5: (Comput ((ProgramPart s1),s1,k)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,k)) . (IC SCM+FSA) and
A6: (Comput ((ProgramPart s1),s1,k)) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) = (Comput ((ProgramPart s2),s2,k)) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) ; :: thesis: ( (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,i)) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) = (Comput ((ProgramPart s2),s2,i)) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) )
reconsider t = {} as PartState of SCM+FSA by FUNCT_1:174, RELAT_1:206;
set D1 = ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p);
A7: dom t c= Int-Locations \/ FinSeq-Locations by RELAT_1:60, XBOOLE_1:2;
A8: ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p) = (UsedInt*Loc p) \/ (UsedIntLoc p) by RELAT_1:60;
hence (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) by A1, A2, A3, A4, A5, A6, A7, Th25; :: thesis: (Comput ((ProgramPart s1),s1,i)) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) = (Comput ((ProgramPart s2),s2,i)) | ((UsedInt*Loc p) \/ (UsedIntLoc p))
thus (Comput ((ProgramPart s1),s1,i)) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) = (Comput ((ProgramPart s2),s2,i)) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) by A1, A2, A3, A4, A5, A6, A7, A8, Th25; :: thesis: verum