mirror of
https://github.com/ProgramSnail/pass_strategy_synthesis.git
synced 2026-03-12 02:57:09 +00:00
model description fix
This commit is contained in:
parent
00d13ddbbe
commit
72805e06c9
1 changed files with 19 additions and 2 deletions
|
|
@ -114,7 +114,7 @@ $M subset NN$ - множество испорченных ячеек памят
|
|||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ $f(x), space f := lambda a. e$],
|
||||
name: [ $f(x), space f(ast.basic a) = e$],
|
||||
|
||||
$cl [a -> sigma(x)], mu, l, nothing cr
|
||||
xarrow(e)
|
||||
|
|
@ -123,7 +123,24 @@ $M subset NN$ - множество испорченных ячеек памят
|
|||
$mu' =>^M' gamma$,
|
||||
|
||||
$cl sigma, mu, l, M cr
|
||||
xarrow(f(*x))
|
||||
xarrow(f(ast.basic x))
|
||||
cl sigma, gamma|_[0, l), l, M cr$,
|
||||
)
|
||||
))
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ $f(x), space f(a) = e$],
|
||||
|
||||
$cl [a -> l], mu, l + 1, nothing cr
|
||||
xarrow(e)
|
||||
cl sigma, mu', l', M' cr$,
|
||||
|
||||
$mu' =>^M' gamma$,
|
||||
|
||||
$cl sigma, mu, l, M cr
|
||||
xarrow(f(x))
|
||||
cl sigma, gamma|_[0, l), l, M cr$,
|
||||
)
|
||||
))
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue