prover.sml

这是我们参加06年全国开源软件的竞赛作品

Decl 8
f%Prover.f-sqsSequent.v$SEQ.;-;sAgent.v$McAGENT.;-;rSequent.Agent.;sFormula.v$PFORMULA.;-;rSequent.Formula.;sNameequation.v$NAMEEQUATION.;-;rSequent.Nameequation.;sBool.v$COND.;-;rBool.Agent.;sName.v$NAME.;-;rSequent.Formula.Bool.Name.Agent.Nameequation.;sEnv.v$ENV.;-;rSequent.Env.Agent.;sAgentSubSemantics.v$AGENTSUBSEM.;-;rName.AgentSubSemantics.Agent.;sNameSubstitution.v$NAMESUBSTITUTION.;-;rName.AgentSubSemantics.NameSubstitution.;sAct.v$ACTION.;-;rSequent.Formula.Act.Name.Agent.;sConstant.v$CONSTANT.;-;rSequent.Formula.Constant.;;;sqsS.vSequent.;-;sF.vFormula.;-;sA.vAgent.;-;sN.vName.;-;sNE.vNameequation.;-;sE.vEnv.;-;sAS.vAgentSubSemantics.;-;sNS.vNameSubstitution.;-;sB.vBool.;-;sACT.vAct.;-;sCST.vConstant.;-;rA.B.F.N.S.NE.AS.NS.ACT.CST.Lib.List.Agent.TextIO.Flags.;;+v$PROVER.;;