let i, k be Element of NAT ; :: thesis: for p being Program of
for s1, s2 being State of st k <= i & p c= s1 & p c= s2 & ( for j being Element of NAT holds
( IC (Computation s1,j) in dom p & IC (Computation s2,j) in dom p ) ) & (Computation s1,k) . (IC SCM+FSA ) = (Computation s2,k) . (IC SCM+FSA ) & (Computation s1,k) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) = (Computation s2,k) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) holds
( (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) & (Computation s1,i) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) = (Computation s2,i) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) )
let p be Program of ; :: thesis: for s1, s2 being State of st k <= i & p c= s1 & p c= s2 & ( for j being Element of NAT holds
( IC (Computation s1,j) in dom p & IC (Computation s2,j) in dom p ) ) & (Computation s1,k) . (IC SCM+FSA ) = (Computation s2,k) . (IC SCM+FSA ) & (Computation s1,k) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) = (Computation s2,k) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) holds
( (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) & (Computation s1,i) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) = (Computation s2,i) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) )
let s1, s2 be State of ; :: thesis: ( k <= i & p c= s1 & p c= s2 & ( for j being Element of NAT holds
( IC (Computation s1,j) in dom p & IC (Computation s2,j) in dom p ) ) & (Computation s1,k) . (IC SCM+FSA ) = (Computation s2,k) . (IC SCM+FSA ) & (Computation s1,k) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) = (Computation s2,k) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) implies ( (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) & (Computation s1,i) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) = (Computation 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 (Computation s1,j) in dom p & IC (Computation s2,j) in dom p ) and
A5: (Computation s1,k) . (IC SCM+FSA ) = (Computation s2,k) . (IC SCM+FSA ) and
A6: (Computation s1,k) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) = (Computation s2,k) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) ; :: thesis: ( (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) & (Computation s1,i) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) = (Computation s2,i) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) )
reconsider t = {} as FinPartState of by CARD_3:66;
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 (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) by A1, A2, A3, A4, A5, A6, A7, Th25; :: thesis: (Computation s1,i) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) = (Computation s2,i) | ((UsedInt*Loc p) \/ (UsedIntLoc p))
thus (Computation s1,i) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) = (Computation s2,i) | ((UsedInt*Loc p) \/ (UsedIntLoc p)) by A1, A2, A3, A4, A5, A6, A7, A8, Th25; :: thesis: verum