let R be good Ring; :: thesis: for I being Instruction of (SCM R) st InsCode I = 5 holds
ex a being Data-Location of R ex r being Element of R st I = a := r
let I be Instruction of (SCM R); :: thesis: ( InsCode I = 5 implies ex a being Data-Location of R ex r being Element of R st I = a := r )
assume A1: InsCode I = 5 ; :: thesis: ex a being Data-Location of R ex r being Element of R st I = a := r
( I = [0 ,{} ] or ex a, b being Data-Location of R st I = a := b or ex a, b being Data-Location of R st I = AddTo a,b or ex a, b being Data-Location of R st I = SubFrom a,b or ex a, b being Data-Location of R st I = MultBy a,b or ex i1 being Instruction-Location of SCM R st I = goto i1 or ex a being Data-Location of R ex i1 being Instruction-Location of SCM R st I = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st I = a := r ) by SCMRING2:8;
hence ex a being Data-Location of R ex r being Element of R st I = a := r by A1, MCART_1:def 1; :: thesis: verum