let P1, P2 be Instruction-Sequence of SCM+FSA; :: thesis: for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st DataPart s1 = DataPart s2 & I is_pseudo-closed_on s1,P1 holds
I is_pseudo-closed_on s2,P2
let s1, s2 be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA st DataPart s1 = DataPart s2 & I is_pseudo-closed_on s1,P1 holds
I is_pseudo-closed_on s2,P2
set D = Data-Locations ;
let I be Program of SCM+FSA; :: thesis: ( DataPart s1 = DataPart s2 & I is_pseudo-closed_on s1,P1 implies I is_pseudo-closed_on s2,P2 )
set S1 = Initialize s1;
set Q1 = P1 +* I;
set S2 = Initialize s2;
set Q2 = P2 +* I;
A1: I c= P1 +* I by FUNCT_4:25;
A2: Reloc (I,0) = I ;
A3: IC (Initialize s2) = IC (s2 +* (Start-At (0,SCM+FSA)))
.= 0 by FUNCT_4:113 ;
A4: I c= P2 +* I by FUNCT_4:25;
assume DataPart s1 = DataPart s2 ; :: thesis: ( not I is_pseudo-closed_on s1,P1 or I is_pseudo-closed_on s2,P2 )
then A5: DataPart (Initialize s1) = DataPart s2 by MEMSTR_0:79
.= DataPart (Initialize s2) by MEMSTR_0:79 ;
assume A6: I is_pseudo-closed_on s1,P1 ; :: thesis: I is_pseudo-closed_on s2,P2
then A7: IC (Comput ((P1 +* I),(Initialize s1),(pseudo-LifeSpan (s1,P1,I)))) = card I by SCMFSA8A:def 4;
A8: I is_pseudo-closed_on Initialize s1,P1 +* I by A6;
A9: now :: thesis: for k being Nat st k < pseudo-LifeSpan (s1,P1,I) holds
IC (Comput ((P2 +* I),(Initialize s2),k)) in dom I
let k be Nat; :: thesis: ( k < pseudo-LifeSpan (s1,P1,I) implies IC (Comput ((P2 +* I),(Initialize s2),k)) in dom I )
assume A10: k < pseudo-LifeSpan (s1,P1,I) ; :: thesis: IC (Comput ((P2 +* I),(Initialize s2),k)) in dom I
then k <= pseudo-LifeSpan ((Initialize s1),(P1 +* I),I) by A6, Th13;
then IC (Comput ((P2 +* I),(Initialize s2),k)) = (IC (Comput ((P1 +* I),(Initialize s1),k))) + 0 by A5, A8, A4, A3, Th14, A1, A2
.= IC (Comput ((P1 +* I),(Initialize s1),k)) ;
hence IC (Comput ((P2 +* I),(Initialize s2),k)) in dom I by A6, A10, SCMFSA8A:def 4; :: thesis: verum
end;
IC (Comput ((P2 +* I),(Initialize s2),(pseudo-LifeSpan (s1,P1,I)))) = IC (Comput ((P2 +* I),(Initialize s2),(pseudo-LifeSpan ((Initialize s1),(P1 +* I),I)))) by A6, Th13
.= (IC (Comput ((P1 +* I),(Initialize s1),(pseudo-LifeSpan ((Initialize s1),(P1 +* I),I))))) + 0 by A5, A8, A4, A3, Th14, A1, A2
.= IC (Comput ((P1 +* I),(Initialize s1),(pseudo-LifeSpan (s1,P1,I)))) by A6, Th13 ;
hence I is_pseudo-closed_on s2,P2 by A7, A9; :: thesis: verum