let s1, s2 be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA
for a being Int-Location st I does_not_refer a & ( for b being Int-Location st a <> b holds
s1 . b = s2 . b ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) & I is_closed_on s1 & I is_halting_on s1 holds
for k being Element of NAT holds
( ( for b being Int-Location st a <> b holds
(Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . b = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . b ) & ( for f being FinSeq-Location holds (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . f = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . f ) & IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) & CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) )
let I be Program of SCM+FSA ; :: thesis: for a being Int-Location st I does_not_refer a & ( for b being Int-Location st a <> b holds
s1 . b = s2 . b ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) & I is_closed_on s1 & I is_halting_on s1 holds
for k being Element of NAT holds
( ( for b being Int-Location st a <> b holds
(Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . b = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . b ) & ( for f being FinSeq-Location holds (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . f = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . f ) & IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) & CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) )
let a be Int-Location ; :: thesis: ( I does_not_refer a & ( for b being Int-Location st a <> b holds
s1 . b = s2 . b ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) & I is_closed_on s1 & I is_halting_on s1 implies for k being Element of NAT holds
( ( for b being Int-Location st a <> b holds
(Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . b = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . b ) & ( for f being FinSeq-Location holds (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . f = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . f ) & IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) & CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) ) )
assume A1: I does_not_refer a ; :: thesis: ( ex b being Int-Location st
( a <> b & not s1 . b = s2 . b ) or ex f being FinSeq-Location st not s1 . f = s2 . f or not I is_closed_on s1 or not I is_halting_on s1 or for k being Element of NAT holds
( ( for b being Int-Location st a <> b holds
(Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . b = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . b ) & ( for f being FinSeq-Location holds (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . f = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . f ) & IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) & CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) ) )
assume A2: ( ( for b being Int-Location st a <> b holds
s1 . b = s2 . b ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) ) ; :: thesis: ( not I is_closed_on s1 or not I is_halting_on s1 or for k being Element of NAT holds
( ( for b being Int-Location st a <> b holds
(Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . b = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . b ) & ( for f being FinSeq-Location holds (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . f = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . f ) & IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) & CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) ) )
assume A3: ( I is_closed_on s1 & I is_halting_on s1 ) ; :: thesis: for k being Element of NAT holds
( ( for b being Int-Location st a <> b holds
(Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . b = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . b ) & ( for f being FinSeq-Location holds (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . f = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . f ) & IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) & CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) )
defpred S1[ State of SCM+FSA , State of SCM+FSA ] means ( ( for b being Int-Location st a <> b holds
$1 . b = $2 . b ) & ( for f being FinSeq-Location holds $1 . f = $2 . f ) );
set S1 = s1 +* (I +* (Start-At (insloc 0 )));
set S2 = s2 +* (I +* (Start-At (insloc 0 )));
A4: I +* (Start-At (insloc 0 )) c= s1 +* (I +* (Start-At (insloc 0 ))) by FUNCT_4:26;
A5: I +* (Start-At (insloc 0 )) c= s2 +* (I +* (Start-At (insloc 0 ))) by FUNCT_4:26;
A6: now
let b be Int-Location ; :: thesis: ( a <> b implies (s1 +* (I +* (Start-At (insloc 0 )))) . b = (s2 +* (I +* (Start-At (insloc 0 )))) . b )
assume A7: a <> b ; :: thesis: (s1 +* (I +* (Start-At (insloc 0 )))) . b = (s2 +* (I +* (Start-At (insloc 0 )))) . b
A8: ( b in dom s2 & not b in dom (I +* (Start-At (insloc 0 ))) & b in dom s1 ) by SCMFSA6B:12, SCMFSA_2:66;
hence (s1 +* (I +* (Start-At (insloc 0 )))) . b = s1 . b by FUNCT_4:12
.= s2 . b by A2, A7
.= (s2 +* (I +* (Start-At (insloc 0 )))) . b by A8, FUNCT_4:12 ;
:: thesis: verum
end;
A9: now
let f be FinSeq-Location ; :: thesis: (s1 +* (I +* (Start-At (insloc 0 )))) . f = (s2 +* (I +* (Start-At (insloc 0 )))) . f
A10: ( f in dom s2 & not f in dom (I +* (Start-At (insloc 0 ))) & f in dom s1 ) by SCMFSA6B:13, SCMFSA_2:67;
hence (s1 +* (I +* (Start-At (insloc 0 )))) . f = s1 . f by FUNCT_4:12
.= s2 . f by A2
.= (s2 +* (I +* (Start-At (insloc 0 )))) . f by A10, FUNCT_4:12 ;
:: thesis: verum
end;
defpred S2[ Element of NAT ] means ( S1[ Computation (s1 +* (I +* (Start-At (insloc 0 )))),$1, Computation (s2 +* (I +* (Start-At (insloc 0 )))),$1] & IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),$1) = IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),$1) & CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),$1) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),$1) );
I c= I +* (Start-At (insloc 0 )) by SCMFSA8A:9;
then A11: ( I c= s1 +* (I +* (Start-At (insloc 0 ))) & I c= s2 +* (I +* (Start-At (insloc 0 ))) ) by A4, A5, XBOOLE_1:1;
A12: S2[ 0 ]
proof
A13: IC SCM+FSA in dom (I +* (Start-At (insloc 0 ))) by SF_MASTR:65;
A14: Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 = s1 +* (I +* (Start-At (insloc 0 ))) by AMI_1:13;
Computation (s2 +* (I +* (Start-At (insloc 0 )))),0 = s2 +* (I +* (Start-At (insloc 0 ))) by AMI_1:13;
hence S1[ Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 , Computation (s2 +* (I +* (Start-At (insloc 0 )))),0 ] by A6, A9, A14; :: thesis: ( IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 ) = IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),0 ) & CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 ) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),0 ) )
thus A15: IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 ) = (s1 +* (I +* (Start-At (insloc 0 )))) . (IC SCM+FSA ) by AMI_1:13
.= (I +* (Start-At (insloc 0 ))) . (IC SCM+FSA ) by A13, FUNCT_4:14
.= (s2 +* (I +* (Start-At (insloc 0 )))) . (IC SCM+FSA ) by A13, FUNCT_4:14
.= IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),0 ) by AMI_1:13 ; :: thesis: CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 ) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),0 )
A16: IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 ) in dom I by A3, SCMFSA7B:def 7;
thus CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 ) = (s1 +* (I +* (Start-At (insloc 0 )))) . (IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 )) by AMI_1:13
.= I . (IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 )) by A11, A16, GRFUNC_1:8
.= (s2 +* (I +* (Start-At (insloc 0 )))) . (IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),0 )) by A11, A15, A16, GRFUNC_1:8
.= CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),0 ) by AMI_1:13 ; :: thesis: verum
end;
A17: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S2[k] implies S2[k + 1] )
assume A18: S2[k] ; :: thesis: S2[k + 1]
A19: ProgramPart I = I by AMI_1:105;
then A20: ( I c= Computation (s1 +* (I +* (Start-At (insloc 0 )))),k & I c= Computation (s2 +* (I +* (Start-At (insloc 0 )))),k ) by A11, AMI_1:99;
A21: ( I c= Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1) & I c= Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1) ) by A11, A19, AMI_1:99;
A22: IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) in dom I by A3, SCMFSA7B:def 7;
then A23: CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = I . (IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k)) by A20, GRFUNC_1:8;
A24: Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1) = Following (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) by AMI_1:14
.= Exec (CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k)),(Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) ;
A25: Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1) = Following (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) by AMI_1:14
.= Exec (CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k)),(Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) ;
CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) in rng I by A22, A23, FUNCT_1:def 5;
then A26: CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) does_not_refer a by A1, SCMFSA7B:def 2;
hence S1[ Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1), Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1)] by A18, A24, A25, Th37; :: thesis: ( IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1)) = IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1)) & CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1)) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1)) )
thus A27: IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1)) = IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1)) by A18, A24, A25, A26, Th37; :: thesis: CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1)) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1))
A28: IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1)) in dom I by A3, SCMFSA7B:def 7;
hence CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1)) = I . (IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1))) by A21, GRFUNC_1:8
.= CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1)) by A21, A27, A28, GRFUNC_1:8 ;
:: thesis: verum
end;
for k being Element of NAT holds S2[k] from NAT_1:sch 1(A12, A17);
 hence for k being Element of NAT holds
( ( for b being Int-Location st a <> b holds
(Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . b = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . b ) & ( for f being FinSeq-Location holds (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . f = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . f ) & IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) & CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) ) ; :: thesis: verum