Step
*
1
of Lemma
lpath_cons
1. l : IdLnk
2. p : IdLnk List
3. lpath([l / p])
⊢ lpath(p)
BY
{ ((((((((((ParallelOp (-1)) THEN D 0) THENA Auto) THEN (InstHyp [⌈i + 1⌉] (-2))⋅) THENA Auto')
THEN (RWO "select_cons_tl" (-1))
)
THENA Auto'
)
THEN (Subst ⌈(i + 1) - 1 ~ i⌉ (-1))⋅
)
THENL [Auto; Id]
)
THEN (Subst ⌈((i + 1) + 1) - 1 ~ i + 1⌉ (-1))⋅
THEN Auto) }
Latex:
1. l : IdLnk
2. p : IdLnk List
3. lpath([l / p])
\mvdash{} lpath(p)
By
((((((((((ParallelOp (-1)) THEN D 0) THENA Auto) THEN (InstHyp [\mkleeneopen{}i + 1\mkleeneclose{}] (-2))\mcdot{}) THENA Auto')
THEN (RWO "select\_cons\_tl" (-1))
)
THENA Auto'
)
THEN (Subst \mkleeneopen{}(i + 1) - 1 \msim{} i\mkleeneclose{} (-1))\mcdot{}
)
THENL [Auto; Id]
)
THEN (Subst \mkleeneopen{}((i + 1) + 1) - 1 \msim{} i + 1\mkleeneclose{} (-1))\mcdot{}
THEN Auto)
Home
Index