let i, k be Element of NAT ; :: thesis: for p being Program of SCM+FSA
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 SCM+FSA ; :: 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