Step
*
1
1
of Lemma
stdEO_wf
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. S0 : System(P.M[P])
4. [%3] : std-initial(S0)
5. n2m : ℕ ─→ pMsg(P.M[P])
6. l2m : Id ─→ pMsg(P.M[P])
7. env : pEnvType(P.M[P])
8. pRun(S0;env;n2m;l2m) ∈ pRunType(P.M[P])
⊢ SqStable(std-initial(S0))
BY
{ (D 3
THEN RepUR ``std-initial lg-all`` 0
THEN Auto
THEN (DoSubsume THEN Auto THEN BLemma `subtype_rel-ldag` THEN Auto)⋅) }
Latex:
Latex:
1. M : Type {}\mrightarrow{} Type
2. Continuous+(P.M[P])
3. S0 : System(P.M[P])
4. [\%3] : std-initial(S0)
5. n2m : \mBbbN{} {}\mrightarrow{} pMsg(P.M[P])
6. l2m : Id {}\mrightarrow{} pMsg(P.M[P])
7. env : pEnvType(P.M[P])
8. pRun(S0;env;n2m;l2m) \mmember{} pRunType(P.M[P])
\mvdash{} SqStable(std-initial(S0))
By
Latex:
(D 3
THEN RepUR ``std-initial lg-all`` 0
THEN Auto
THEN (DoSubsume THEN Auto THEN BLemma `subtype\_rel-ldag` THEN Auto)\mcdot{})
Home
Index