let T be TuringStr ; :: thesis: for t being Tape of T
for h being Integer
for s being Symbol of T st t . h = s holds
Tape-Chg t,h,s = t
let t be Tape of T; :: thesis: for h being Integer
for s being Symbol of T st t . h = s holds
Tape-Chg t,h,s = t
let h be Integer; :: thesis: for s being Symbol of T st t . h = s holds
Tape-Chg t,h,s = t
let s be Symbol of T; :: thesis: ( t . h = s implies Tape-Chg t,h,s = t )
assume A1: t . h = s ; :: thesis: Tape-Chg t,h,s = t
consider f being Function such that
A2: ( t = f & dom f = INT & rng f c= the Symbols of T ) by FUNCT_2:def 2;
h in dom t by A2, INT_1:def 2;
hence Tape-Chg t,h,s = t by A1, FUNCT_7:98; :: thesis: verum