let s be State of SCM; :: thesis: for tl, tr being bin-term holds
( (tl + tr) @ s = (tl @ s) + (tr @ s) & (tl - tr) @ s = (tl @ s) - (tr @ s) & (tl * tr) @ s = (tl @ s) * (tr @ s) & (tl div tr) @ s = (tl @ s) div (tr @ s) & (tl mod tr) @ s = (tl @ s) mod (tr @ s) )
let tl, tr be bin-term; :: thesis: ( (tl + tr) @ s = (tl @ s) + (tr @ s) & (tl - tr) @ s = (tl @ s) - (tr @ s) & (tl * tr) @ s = (tl @ s) * (tr @ s) & (tl div tr) @ s = (tl @ s) div (tr @ s) & (tl mod tr) @ s = (tl @ s) mod (tr @ s) )
thus (tl + tr) @ s = nt0 -Meaning_on ((tl @ s),(tr @ s)) by Th5
.= (tl @ s) + (tr @ s) by Def8 ; :: thesis: ( (tl - tr) @ s = (tl @ s) - (tr @ s) & (tl * tr) @ s = (tl @ s) * (tr @ s) & (tl div tr) @ s = (tl @ s) div (tr @ s) & (tl mod tr) @ s = (tl @ s) mod (tr @ s) )
thus (tl - tr) @ s = nt1 -Meaning_on ((tl @ s),(tr @ s)) by Th5
.= (tl @ s) - (tr @ s) by Def8 ; :: thesis: ( (tl * tr) @ s = (tl @ s) * (tr @ s) & (tl div tr) @ s = (tl @ s) div (tr @ s) & (tl mod tr) @ s = (tl @ s) mod (tr @ s) )
thus (tl * tr) @ s = nt2 -Meaning_on ((tl @ s),(tr @ s)) by Th5
.= (tl @ s) * (tr @ s) by Def8 ; :: thesis: ( (tl div tr) @ s = (tl @ s) div (tr @ s) & (tl mod tr) @ s = (tl @ s) mod (tr @ s) )
thus (tl div tr) @ s = nt3 -Meaning_on ((tl @ s),(tr @ s)) by Th5
.= (tl @ s) div (tr @ s) by Def8 ; :: thesis: (tl mod tr) @ s = (tl @ s) mod (tr @ s)
thus (tl mod tr) @ s = nt4 -Meaning_on ((tl @ s),(tr @ s)) by Th5
.= (tl @ s) mod (tr @ s) by Def8 ; :: thesis: verum