Step * of Lemma MachinPi4-req

MachinPi4() /r(4))
BY
(GenConclTerm ⌜MachinPi4()⌝⋅ THEN Auto) }


Latex:


Latex:
MachinPi4()  =  (\mpi{}/r(4))


By


Latex:
(GenConclTerm  \mkleeneopen{}MachinPi4()\mkleeneclose{}\mcdot{}  THEN  Auto)




Home Index