let s be SCM+FSA-State; :: thesis: for s1 being SCM-State holds s +* s1 is SCM+FSA-State
let s1 be SCM-State; :: thesis: s +* s1 is SCM+FSA-State
A1: dom = SCM+FSA-Memory by Lm8;
then reconsider f = SCM*-VAL * SCM+FSA-OK as non-empty ManySortedSet of SCM+FSA-Memory by PARTFUN1:def 2;
A2: dom s1 = dom () by CARD_3:9
.= SCM-Memory by AMI_2:27 ;
now :: thesis: for x being set st x in dom s1 holds
s1 . x in f . x
let x be set ; :: thesis: ( x in dom s1 implies s1 . b1 in f . b1 )
assume A3: x in dom s1 ; :: thesis: s1 . b1 in f . b1
then A4: x in \/ SCM-Data-Loc by A2;
per cases by ;
suppose A5: x in ; :: thesis: s1 . b1 in f . b1
reconsider a = x as Element of SCM-Memory by A2, A3;
A6: s1 . a in pi ((),a) by CARD_3:def 6;
A7: x = NAT by ;
dom () = SCM-Memory by AMI_2:27;
then pi ((),a) = () . a by CARD_3:12
.= NAT by ;
hence s1 . x in f . x by ; :: thesis: verum
end;
suppose A8: x in SCM-Data-Loc ; :: thesis: s1 . b1 in f . b1
reconsider a = x as Element of SCM-Memory by A2, A3;
A9: s1 . a in pi ((),a) by CARD_3:def 6;
dom () = SCM-Memory by AMI_2:27;
then A10: pi ((),a) = () . a by CARD_3:12;
(SCM*-VAL * SCM+FSA-OK) . x = INT by ;
hence s1 . x in f . x by ; :: thesis: verum
end;
end;
end;
then s +* s1 is SCM+FSA-State by ;
hence s +* s1 is SCM+FSA-State ; :: thesis: verum