Step * of Lemma lg-all_functionality

[T:Type]. ∀G:LabeledDAG(T). ∀[P1,P2:T ─→ ℙ].  ((∀x:T. (P1[x]  P2[x]))  {∀x∈G.P1[x]  ∀x∈G.P2[x]})
BY
(Unfold `guard` 0
   THEN (RepeatFor ((D THENA Auto))
         THEN -1
         THEN Auto
         THEN RepeatFor (ParallelLast)
         THEN BHyp 
         THEN Try (Complete (Auto)))
   }


Latex:



Latex:
\mforall{}[T:Type]
    \mforall{}G:LabeledDAG(T).  \mforall{}[P1,P2:T  {}\mrightarrow{}  \mBbbP{}].    ((\mforall{}x:T.  (P1[x]  {}\mRightarrow{}  P2[x]))  {}\mRightarrow{}  \{\mforall{}x\mmember{}G.P1[x]  {}\mRightarrow{}  \mforall{}x\mmember{}G.P2[x]\})


By


Latex:
(Unfold  `guard`  0
  THEN  (RepeatFor  2  ((D  0  THENA  Auto))
              THEN  D  -1
              THEN  Auto
              THEN  RepeatFor  2  (ParallelLast)
              THEN  BHyp  6 
              THEN  Try  (Complete  (Auto)))
  )




Home Index