PrintForm
Definitions
Turing
Sections
NuprlLIB
Doc
At:
next
config
wf
M:PM{i}, C:Config(M). M(C)
Config(M)
By:
Unfold `next_config` 0
THEN
Unfold `tm_config` 0
THEN
UnivCD
Generated subgoal:
1
1.
M:
PM{i}
2.
C:
(M)
(
G(M))
let delta =
(M)( < C.st,C.tape(C.hd) > ) in < 1of(delta) ,(
z.if z=
C.hd
1of(2of(delta)) else C.tape(z) fi) ,if 2of(2of(delta))
C.hd+1 else C.hd-1 fi >
(M)
(
G(M))
(M)
(
G(M))
let delta = 
(M)( < C.st,C.tape(C.hd) > ) in
< 1of(delta)
,(
z.if z=
C.hd
1of(2of(delta)) else C.tape(z) fi)
,if 2of(2of(delta)) C.hd+1 else C.hd-1 fi >
(M)(G(M))