Step
*
1
of Lemma
ts-reachable-induction3
1. ts : transition-system{i:l}
2. [P] : ts-reachable(ts) ⟶ ℙ
3. P[ts-init(ts)]
4. ∀x:ts-type(ts). ((ts-init(ts) (ts-rel(ts)^*) x) 
⇒ (∀y:ts-reachable(ts). (P[x] 
⇒ (x ts-rel(ts) y) 
⇒ P[y])))
5. x : ts-type(ts)
6. n : ℕ
7. ts-rel(ts)^n ts-init(ts) x
8. x ∈ ts-reachable(ts)
⊢ P[x]
BY
{ xxx(MoveToConcl (-2)
      THEN GenConclAtAddr [2;2]
      THEN Try (Complete (Auto))
      THEN Thin (-1)
      THEN MoveToConcl (-1)
      THEN Thin (-1))xxx }
1
1. ts : transition-system{i:l}
2. [P] : ts-reachable(ts) ⟶ ℙ
3. P[ts-init(ts)]
4. ∀x:ts-type(ts). ((ts-init(ts) (ts-rel(ts)^*) x) 
⇒ (∀y:ts-reachable(ts). (P[x] 
⇒ (x ts-rel(ts) y) 
⇒ P[y])))
5. x : ts-type(ts)
6. n : ℕ
⊢ ∀v:ts-reachable(ts). ((ts-rel(ts)^n ts-init(ts) v) 
⇒ P[v])
Latex:
Latex:
1.  ts  :  transition-system\{i:l\}
2.  [P]  :  ts-reachable(ts)  {}\mrightarrow{}  \mBbbP{}
3.  P[ts-init(ts)]
4.  \mforall{}x:ts-type(ts)
          ((ts-init(ts)  (ts-rel(ts)\^{}*)  x)  {}\mRightarrow{}  (\mforall{}y:ts-reachable(ts).  (P[x]  {}\mRightarrow{}  (x  ts-rel(ts)  y)  {}\mRightarrow{}  P[y])))
5.  x  :  ts-type(ts)
6.  n  :  \mBbbN{}
7.  rel\_exp(ts-type(ts);  ts-rel(ts);  n)  ts-init(ts)  x
8.  x  \mmember{}  ts-reachable(ts)
\mvdash{}  P[x]
By
Latex:
xxx(MoveToConcl  (-2)
        THEN  GenConclAtAddr  [2;2]
        THEN  Try  (Complete  (Auto))
        THEN  Thin  (-1)
        THEN  MoveToConcl  (-1)
        THEN  Thin  (-1))xxx
Home
Index