let I be Instruction of SCM ; :: thesis: for S being State of SCM
for s being State of SCM+FSA st S = (s | SCM-Memory ) +* (NAT --> I) holds
s = (s +* S) +* (s | NAT )
let S be State of SCM ; :: thesis: for s being State of SCM+FSA st S = (s | SCM-Memory ) +* (NAT --> I) holds
s = (s +* S) +* (s | NAT )
let s be State of SCM+FSA ; :: thesis: ( S = (s | SCM-Memory ) +* (NAT --> I) implies s = (s +* S) +* (s | NAT ) )
A1: dom (NAT --> I) = NAT by FUNCOP_1:19;
A2: dom s = dom SCM+FSA-OK by CARD_3:18
.= SCM+FSA-Memory by FUNCT_2:def 1 ;
dom (s | NAT ) = (dom s) /\ NAT by RELAT_1:90
.= NAT by A2, XBOOLE_1:28 ;
then A3: (NAT --> I) +* (s | NAT ) = s | NAT by A1, FUNCT_4:20;
assume S = (s | SCM-Memory ) +* (NAT --> I) ; :: thesis: s = (s +* S) +* (s | NAT )
hence (s +* S) +* (s | NAT ) = ((s +* (s | SCM-Memory )) +* (NAT --> I)) +* (s | NAT ) by FUNCT_4:15
.= (s +* (NAT --> I)) +* (s | NAT ) by FUNCT_4:80
.= s +* ((NAT --> I) +* (s | NAT )) by FUNCT_4:15
.= s by A3, FUNCT_4:80 ;
:: thesis: verum