010 J ^!! defaultprefix !!! defaultprefix # defaultprefix ## defaultprefix $ defaultprefix *** defaultprefix - 0 |- true |-| defaultprefix ~ true Y1 1 ! Y0 1 !!! Y0 0 # Y0 0 ## Y0 0 $ Y0 0 % Y0 0 %! Y0 0 & Y0 0 * Y0 0 *! Y0 0 ** Y0 1 *** Y0 0 + Y0 0 +! Y0 0 , Y0 0 - Y0 0 -! Y0 0 -> Y~1 ~1 ->> Y0 0 . Y0 0 .-. Y0 0 ./. Y0 0 / Y0 0 /! Y0 0 // c3pt11 c3pt14 c3pt15a c3pt15b c3pt15bF c3pt32 c3pt32F c3pt43a c3pt43aF c3pt43b c3pt43bF c3pt44a c3pt44b c3pt48 c3pt49 c3pt50 c3pt62 c3pt64 c3pt65 c3pt66 c3pt67 c3pt67F c3pt68 c3pt68F c3pt69 c3pt70 c3pt74 c3pt75 c3pt75F c3pt76a c3pt76aF c3pt76b c3pt76bF c3pt76c c3pt76cF c3pt76d c3pt76dF c3pt76e c3pt76eF c3pt78 c3pt79 c3pt79F c3pt80 c3pt81 c3pt81F c3pt82a c3pt82aF c3pt82b c3pt82bF c3pt82c c3pt82cF c3pt83 c3pt83F c3pt84b c3pt84c c3pt85a c3pt85b c3pt86a c3pt86b c3pt87 c3pt88 c3pt89 c8pt13E c8pt13U c8pt14E c8pt14U c8pt15E c8pt15U c8pt16E c8pt16U c8pt19E c8pt19U c9pt10 c9pt11 c9pt16a c9pt16a1 c9pt16b c9pt18a c9pt18b c9pt18c c9pt20 c9pt21 c9pt22 c9pt23 c9pt24 c9pt25 c9pt26 c9pt30a c9pt30b c9pt3a c9pt3b c9pt3c c9pt4a c9pt4b c9pt4c c9pt4d c9pt5 c9pt6 c9pt7 c9pt8 Y0 0 : Y0 0 < Y0 0 Y0 0 <+> Y0 0 <- Y0 0 <<= Y0 0 <= Y0 0 =! Y0 0 =/= Y0 0 =< Y0 0 == Y0 0 => Y0 0 =>> Y0 0 > Y0 0 >= Y1 0 @ Y0 0 @@ cABS cABS2 cABS3 cABSREST cABSREST2 cABSSETUP cABSSETUP2 cABSTRACT cABSTRACT1 cABSTRACT2 cABSTRACT3 cABSTRACT4 cADD_CANCEL cADD_MONO_LEQ cAF cALLASSERTS cALLASSOCS cALL_CANCEL cALL_CANCEL_1 cALL_CANCEL_2 cALL_CANCEL_3 cALL_CANCEL_4 cALL_CANCEL_5 cALL_CANCEL_6 cALL_CANCEL_7 cALL_EXP cALL_GEQ_0 cALL_STEPS cALTORDEF cALT_POS_DEF cALT_PUSH cALT_QUANT_AGAIN cALT_QUANT_IMP cAND cANDBOOL cANDSCIN cANDUNPACK cAND_EXP cANY_INSTANCE cAP3pt86a cAP3pt86b cAP3pt88 cAPLZ cARROWTYPE cASRTCOND cASRTEQ cASRTLEFT cASRTRIGHT cASSERT cASSERT2 cASSERTCLEAN cASSERTSCOUT cASSERT_EXP cASSERT_UNEXP cASSOCS cASSRTBOTH cAT cBALTDEF cBASSOC cBCONV cBDIS cBEQSUBS cBFLIP cBID cBID2 cBIDF cBOOLDEF cBOUNDED_N cBREAKMINUS cBRULE1 cBRULE2 cBRULE3 cBSYM cBTYPE cBUILTIN cCASEINTRO cCASEPREP cCASSOC cCCON cCDISC cCDISD cCEX cCEX_TAC cCHOICE cCHOICE_TAC cCID cCIDEM cCNBOOL cCNRULE1 cCNRULE2 cCNRULE3 cCN_EXP cCOMMDIST cCOMMPLUSID cCOMMUTE_LEVEL_QUANT cCOMP cCONDCASES cCONDCASES2 cCONDCASESL1 cCONDCASESL1F cCONDSIMP cCONS cCONSCIN cCONSTRUCTBOOL cCONTP cCONTYPE cCONVANDIMP cCONVANDOR cCONVERT_IMP_1 cCONVERT_IMP_2 cCONVIF cCONVIMPAND cCONVIMPOR cCONVORAND cCONVORIMP cCOUNTER cCOUNTER1 cCRULE1 cCRULE2 cCRULE3 cCSYM cCTYPE cCZER cCZERF cDASSOC cDDIS cDDISC cDDISD cDEMa cDEMb cDID cDIDEM cDIFF_EQ cDINSTANTIATE cDINSTANTIATEF1 cDIST cDIVCOMP cDIVSCIN cDIVTYPE cDRULE1 cDRULE2 cDRULE3 cDSYM cDTYPE cDUAL cDUBNEG cDUBNEG2 cDXM cDXMF cDZER cDZERF cEPLUSID cEQBOOL cEQEVAL2 cEQSYMM cEQT cEQUATION cEQUATION_TO_DIFFERENCE cEQ_LEQ cEQ_NOT_LESS cEQ_NOT_LESSF cEQ_TRANS cEVALEQ cEVERYWHERE cEVERYWHERE2 cEVERYWHERE_ABS cEVERYWHERE_CASE cEVERYWHERE_INFIX cEXAMPLE1 cElimForall cFACTORZERO cFALSEBOOL cFDEF cFINDGCD cFIXBREAKMINUS cFLEQ_ADD cFLESS_ADD_NZ cFLESS_ADD_SUC cFLESS_MONO_MULT cFLIPALL cFLIPPASTA cFLIPPASTB cFLIPPASTC cFLIPPASTD cFLIPPASTN cFLIPPASTX cFNDIST cFNOT_LESS_0 cFORALLBOOL cFORALLBOOL2 cFORALLDIST cFORALLDROP cFORALLNOT cFORALLOR cFORALLORDIST cFORALLRBOOL cFORALLRBOOL2 cFORALLRBOOL3 cFORALLSWITCH cFORALLSWITCH2 cFORALL_IMP_FORSOME_EQ cFORALL_LESS_0 cFORALL_LESS_ANTISYM cFORALL_LESS_CASES cFORALL_LESS_MONO_ADD cFORALL_LESS_MONO_ADDF cFORALL_LESS_MONO_ADD_INV cFORALL_LESS_MONO_ADD_INVF cFORALL_LESS_SUC_REFL cFORALL_LESS_TRANS cFORALL_NOTFORSOME cFORSOMEBOOL cFORSOMEBOOL2 cFORSOMEDIST2 cFORSOMEDROP cFORSOMERBOOL cFORSOMERBOOL2 cFORSOMERBOOL3 cFORSOME_NOTFORALL cGCD cGCD1 cGCD2 cGCDTYPE cGCLEAN cGET cGET0 cGET1 cGET2 cGETPLUS cGR cGR2 cGR3 cGREATER cGREATER_EQ cGREATER_EQ_REAL cGREATER_OR_EQ cHYP cID cIDEF cIDEF2 cIDEF3 cIDIS1 cIDIS2 cIDIS3 cIDIS4 cIDISB cIF cIFBOOL cIFF cIFFBOOL cIFFSCIN cIFF_EXP cIFSCIN cIF_EXP cIGNOREFIRST cILID cIMPTOCOND cIMPTYPE cINDUCTION cINDUCT_TAC cINDUCT_TAC_1 cINDUCT_TAC_2 cINSTANTIATE cINSTANTIATEF cIREF cIREFF cIRULE1 cIRULE2 cIRULE3 cIRZER cIRZERF cId cL cL3pt43 cLABELINTRO cLAMBDAINTRO cLAMBDAINTRO1 cLAMBDAINTRO2 cLAMBDAREMOVE cLAMBDAREMOVE1 cLAMBDAREMOVE2 cLEFT cLEFT_CASE cLEQ_0 cLEQ_ADD cLEQ_ADDF cLEQ_ANTISYM cLEQ_CASES cLEQ_IMP_LESS_SUC cLEQ_LEQ_MONO cLEQ_LESS_TRANS cLEQ_MONO_ADD_EQ cLEQ_MONO_ADD_EQF cLEQ_REFL cLEQ_SUC cLEQ_SUC_REFL cLEQ_TRANS cLESS1 cLESSBOOL cLESSBOOL2 cLESSCOMP cLESSTYPE cLESS_0 cLESS_0F cLESS_0_0 cLESS_0_CASES cLESS_0_CASES_INV cLESS_0_FALSE cLESS_ADD cLESS_ADD1 cLESS_ADD_NZ cLESS_ADD_NZF cLESS_ADD_SUC cLESS_ADD_SUCF cLESS_ANTISYM cLESS_ANTISYMF cLESS_CASES cLESS_CASESF cLESS_CASES_IMP cLESS_EQ cLESS_EQ_ADD cLESS_EQ_ANTISYM cLESS_EQ_MONO cLESS_EQ_REAL cLESS_EQ_SUC_LESS cLESS_IMP_LEQ cLESS_LEMMA1 cLESS_LEMMA1F cLESS_LEMMA2 cLESS_LEMMA2F cLESS_LEQ_TRANS cLESS_LESS_CASES cLESS_LESS_SUC cLESS_MONO cLESS_MONOF cLESS_MONO_ADD cLESS_MONO_ADDF cLESS_MONO_ADD_EQ cLESS_MONO_ADD_INV cLESS_MONO_ADD_INVF cLESS_MONO_EQ cLESS_MONO_MULT cLESS_MONO_MULTF cLESS_MONO_REV cLESS_MONO_REVF cLESS_MULT2 cLESS_NOT_EQ cLESS_NOT_EQF cLESS_NOT_REFL cLESS_NOT_SUC cLESS_OR cLESS_OR_ADD cLESS_OR_EQ cLESS_SUC cLESS_SUCF cLESS_SUC_EQ_COR cLESS_SUC_IMP cLESS_SUC_IMPF cLESS_SUC_NOT cLESS_SUC_REFL cLESS_SUC_REFLF cLESS_SUC_SUC cLESS_SUC_SUCF cLESS_THM cLESS_TRANS cLESS_TRANSF cLISTBIND cLOOP_TAC cLZ cMAKE_CASE cMINUSCOMP cMINUSMINUS cMINUSPLUS cMINUSSCIN cMINUSTYPE cMINUSZERO cMKASRT cMODCOMP cMODSCIN cMODTYPE cMOP cMOPF cMP_THM cMP_THMF cMULT_SUC cMUTASSOC cMUTINT cNATCALC cNATCALCEXPAND cNATMINUSCOMP cNATMINUSSCIN cNATMINUSTYPE cNAT_SUB cNAT__SUB cNEGF cNEQ cNEWTAUT cNONTRIV cNONTRIV2a cNOT cNOT1 cNOTBOOL cNOTBOOLDROP cNOTBOTHPOS cNOTCLEAN cNOTFORALL cNOT_ADD_LESS cNOT_ADD_LESSF cNOT_EQ cNOT_EXP cNOT_GREATER cNOT_GREATER_EQ cNOT_LEQ cNOT_LEQ_SUC cNOT_LESS cNOT_LESS_0 cNOT_LESS_0F cNOT_NUM_EQ cNOT_SUC_ADD_LEQ cNOT_SUC_LEQ cNOT_SUC_LEQ_0 cNOT_SUC_LESS cNRULE1 cNRULE2 cNTYPE cNat cODDCHOICE cONENAT cONEPOINT cOR cORBOOL cORSCIN cOR_EXP cOR_LESS cP1 cP2 cPAIRBIND cPCASEINTRO cPI1 cPI1F cPI2 cPI2F cPIVOT cPLUSASSOC cPLUSCOMM cPLUSCOMP cPLUSID cPLUSINVDIST cPLUSINVDISTS cPLUSMINUS cPLUSSCIN cPLUSTYPE cPLUSTYPE2 cPOINTTYPE cPOSASSERT cPOSPLUS cPOSTIMES cPOSTYPE cPOS_ONE cPOS_SIGN cPOS_ZERO cPRE9pt12 cPREDSCIN cPREDTYPE cPRODTYPE cPROVETAUT cPROVETAUT2 cPositive cPred cR cRAISE0 cREALDIVCOMP cREALDIVSCIN cREALDIVTYPE cREALNAT cREALNUMERAL cREALNUMERAL2 cREALSUBNATTYPE cREALZERO cREAL_LESS_CANCEL cREAL_LESS_DEF cREAL_LESS_TRANS cREAL_NOT_LESS cREAL_TYPE cREAL_TYPE_1 cREAL_UNTYPE cREAL_UNTYPE_1 cREDUCE cREFLEX cREMA cREMFLIP cREPL cREVPIVOT cRIGHT cRIGHT_CASE cRL cRSFN cReal cSAMESUCC cSFLIPALL cSIGNPULL cSQUARE_POS cSREMFLIP cSTARTLOOP cSTL cSTOPLOOP cSTR cSTRONG_EVERYWHERE_CASE cSTT cSUBTRACT_DIFF cSUBTRACT_SUM cSUBTYPE cSUB_REFL cSUCCNOTZERO cSUC_EQ_LESS cSUC_EQ_LESSF cSUC_ID cSUC_IDF cSUC_LESS cSUC_LESSF cTAB_ALL cTAB_ALL_2 cTAB_ALL_NEW_1 cTAB_ALL_NEW_2 cTAB_AND cTAB_AND_2 cTAB_CEX cTAB_IF cTAB_IFF cTAB_IFF_2 cTAB_IF_2 cTAB_NOT cTAB_NOT_2 cTAB_OR cTAB_OR_2 cTAB_SOME cTAB_SOME_2 cTAB_SOME_NEW_1 cTAB_SOME_NEW_2 cTAB_WITNESS cTAB_XOR cTAB_XOR_2 cTADDBOTH cTADDLEFT cTADDRIGHT cTADDTOP cTEMP_PIVOT cTESTSIMP cTHMAP cTIMESASSOC cTIMESCOMM cTIMESCOMP cTIMESDIV cTIMESID cTIMESINTDIV cTIMESSCIN cTIMESTYPE cTIMESTYPE2 cTIMESZERO cTOPDOWN cTOPDOWN_CASE cTOPDOWN_INFIX cTREMBOTH cTREMLEFT cTREMRIGHT cTREMTOP cTRICHOTOMY cTRUEBOOL cTWOASSERTS cTYPENUMERAL cTYPES cUNIONTYPE cUNIV_EQ cUNIV_EQ_TAC cUNIV_RANGE_1 cUNIV_RANGE_2 cUNIV_TAC cUNPACK cX cX1 cX2 cXALTDEF cXOR cXORALTDEF cXORASSOC cXORBOOL cXORDEF cXORFLIP cXORSCIN cXORSYM cXORTYPE cXOR_EXP cXRULE1 cXRULE2 cXRULE3 cZERONAT cZERONOTONE cZERONOTPOS cZEROORSUCC Y0 0 ^& cbool cdefaultprefix ceven cfalse cforall cforall2 cforallcase cforallr cforallr2 cforsome cforsome2 cforsomecase cforsomer cforsomer2 cforsomer3 cgcd codd ctrue Y0 0 | Y0 0 |- Y0 0 |/ Y0 0 || Y0 0 ~ Y0 0 ~= O^+ %% MODSCIN & ANDSCIN * TIMESSCIN + PLUSSCIN - MINUSSCIN -> IFSCIN .-. NATMINUSSCIN ./. REALDIVSCIN / DIVSCIN < LESSTYPE <- CONSCIN =/= XORSCIN == IFFSCIN Pred PREDSCIN | ORSCIN && ANDBOOL -> IFBOOL = EQBOOL == IFFBOOL forall FORALLBOOL forallr FORALLRBOOL forsome FORSOMEBOOL forsomer FORSOMERBOOL | ORBOOL |- ASSERTSCOUT ~ NOTBOOL M$ $?thm ?x ?thm <= ?x A$ M** ?thm1 ** ?thm2 ?x ?thm2 => ?thm1 => ?x A** M3pt11 3pt11 ( ~?p) == ?q ?p == ~?q A3pt11 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt14 3pt14 ?p =/= ?q ( ~?p) == ?q A3pt14 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt15a 3pt15a ?p == false ~?p A3pt15a AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt15b 3pt15b ( ~?p) == ?p false A3pt15b AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt15bF 3pt15bF @ ?p false ( ~?p) == ?p A3pt15bF AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt32 3pt32 (?p | ?q) == ?p | ~?q |-?p A3pt32 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt32F 3pt32F @ ?q |-?p (?p | ?q) == ?p | ~?q A3pt32F AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt43a 3pt43a ?p & ?p | ?q |-?p A3pt43a AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt43aF 3pt43aF @ ?q |-?p ?p & ?p | ?q A3pt43aF AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt43b 3pt43b ?p | ?p & ?q |-?p A3pt43b AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt43bF 3pt43bF @ ?q |-?p ?p | ?p & ?q A3pt43bF AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt44a 3pt44a ?p & ( ~?p) | ?q ?p & ?q A3pt44a AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt44b 3pt44b ?p | ( ~?p) & ?q ?p | ?q A3pt44b AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt48 3pt48 (?p & ~?q) == ~?p ?p & ?q A3pt48 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt49 3pt49 (?p & ?q) == (?p & ?r) == ?p ?p & ?q == ?r A3pt49 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt50 3pt50 ?p & ?q == ?p ?p & ?q A3pt50 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt62 3pt62 ?p -> ?q == ?r (?p & ?q) == ?p & ?r A3pt62 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt64 3pt64 (?p -> ?q) -> ?p -> ?r ?p -> ?q -> ?r A3pt64 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt65 3pt65 ?p -> ?q -> ?r (?p & ?q) -> ?r A3pt65 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt66 3pt66 ?p & ?p -> ?q ?p & ?q A3pt66 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt67 3pt67 ?p & ?q -> ?p |-?p A3pt67 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt67F 3pt67F @ ?q |-?p ?p & ?q -> ?p A3pt67F AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt68 3pt68 ?p | ?p -> ?q true A3pt68 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt68F 3pt68F @ ?p , ?q true ?p | ?p -> ?q A3pt68F AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt69 3pt69 ?p | ?q -> ?p ?q -> ?p A3pt69 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt70 3pt70 (?p | ?q) -> ?p & ?q ?p == ?q A3pt70 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt74 3pt74 ?p -> false ~?p A3pt74 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt75 3pt75 false -> ?p true A3pt75 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt75F 3pt75F @ ?p true false -> ?p A3pt75F AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt76a 3pt76a ?p -> ?p | ?q true A3pt76a AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt76aF 3pt76aF @ ?p , ?q true ?p -> ?p | ?q A3pt76aF AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt76b 3pt76b (?p & ?q) -> ?p true A3pt76b AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt76bF 3pt76bF @ ?p , ?q true (?p & ?q) -> ?p A3pt76bF AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt76c 3pt76c (?p & ?q) -> ?p | ?q true A3pt76c AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt76cF 3pt76cF @ ?p , ?q true (?p & ?q) -> ?p | ?q A3pt76cF AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt76d 3pt76d (?p | ?q & ?r) -> ?p | ?q true A3pt76d AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt76dF 3pt76dF @ ?p , ?q , ?r true (?p | ?q & ?r) -> ?p | ?q A3pt76dF AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt76e 3pt76e (?p & ?q) -> ?p & ?q | ?r true A3pt76e AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt76eF 3pt76eF @ ?p , ?q , ?r true (?p & ?q) -> ?p & ?q | ?r A3pt76eF AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt78 3pt78 (?p -> ?r) & ?q -> ?r (?p | ?q) -> ?r A3pt78 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt79 3pt79 (?p -> ?r) & ( ~?p) -> ?r |-?r A3pt79 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt79F 3pt79F @ ?p |-?r (?p -> ?r) & ( ~?p) -> ?r A3pt79F AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt80 3pt80 (?p -> ?q) & ?q -> ?p ?p == ?q A3pt80 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt81 3pt81 ((?p -> ?q) & ?q -> ?p) -> ?p == ?q true A3pt81 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt81F 3pt81F @ ?p , ?q true ((?p -> ?q) & ?q -> ?p) -> ?p == ?q A3pt81F AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt82a 3pt82a ((?p -> ?q) & ?q -> ?r) -> ?p -> ?r true A3pt82a AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt82aF 3pt82aF @ ?p , ?q , ?r true ((?p -> ?q) & ?q -> ?r) -> ?p -> ?r A3pt82aF AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt82b 3pt82b ((?p == ?q) & ?q -> ?r) -> ?p -> ?r true A3pt82b AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt82bF 3pt82bF @ ?p , ?q , ?r true ((?p == ?q) & ?q -> ?r) -> ?p -> ?r A3pt82bF AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt82c 3pt82c ((?p -> ?q) & ?q == ?r) -> ?p -> ?r true A3pt82c AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt82cF 3pt82cF @ ?p , ?q , ?r true ((?p -> ?q) & ?q == ?r) -> ?p -> ?r A3pt82cF AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt83 3pt83 (?e = ?f) -> (?F @ ?e) = ?F @ ?f true A3pt83 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt83F 3pt83F @ ?F , ?e , ?f true (?e = ?f) -> (?F @ ?e) = ?F @ ?f A3pt83F AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt84b 3pt84b (?e = ?f) -> ?F @ ?e (?e = ?f) -> ?F @ ?f A3pt84b AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt84c 3pt84c (?q & ?e = ?f) -> ?F @ ?e (?q & ?e = ?f) -> ?F @ ?f A3pt84c AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt85a 3pt85a ?p -> ?F @ ?p ?p -> ?F @ true A3pt85a AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt85b 3pt85b (?q & ?p) -> ?F @ ?p (?q & ?p) -> ?F @ true A3pt85b AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt86a 3pt86a (?F @ |-?p) -> ?p (?F @ false) -> ?p A3pt86a AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt86b 3pt86b (?F @ |-?p) -> ?p | ?q (?F @ false) -> ?p | ?q A3pt86b AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt87 3pt87 ?p & ?F @ ?p ?p & ?F @ true A3pt87 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt88 3pt88 ?p | ?F @ |-?p ?p | ?F @ false A3pt88 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M3pt89 3pt89 (?p & ?F @ true) | ( ~?p) & ?F @ false |-?F @ |-?p A3pt89 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M8pt13E 8pt13E forsomer @ [false] , [?P @ ?1] false A8pt13E AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forall forallr forsomer M8pt13U 8pt13U forallr @ [false] , [?P @ ?1] true A8pt13U AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forall forallr M8pt14E 8pt14E forsomer @ [?1 = ?e] , [?P @ ?1] |-EVAL => ?P @ ?e A8pt14E AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forall forallr forsomer M8pt14U 8pt14U forallr @ [?1 = ?e] , [?P @ ?1] |-EVAL => ?P @ ?e A8pt14U AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forall forallr M8pt15E 8pt15E (forsomer @ [?R @ ?1] , [?P @ ?1]) | forsomer @ [?R @ ?1] , [?Q @ ?1] forsomer @ [?R @ ?1] , [(?P @ ?1) | ?Q @ ?1] A8pt15E AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forall forallr forsomer M8pt15U 8pt15U (forallr @ [?R @ ?1] , [?P @ ?1]) & forallr @ [?R @ ?1] , [?Q @ ?1] forallr @ [?R @ ?1] , [(?P @ ?1) & ?Q @ ?1] A8pt15U AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forall forallr M8pt16E 8pt16E forsomer @ [(?R @ ?1) | ?S @ ?1] , [?P @ ?1] (forsomer @ [?R @ ?1] , [?P @ ?1]) | forsomer @ [?S @ ?1] , [?P @ ?1] A8pt16E AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forall forallr forsomer M8pt16U 8pt16U forallr @ [(?R @ ?1) | ?S @ ?1] , [?P @ ?1] (forallr @ [?R @ ?1] , [?P @ ?1]) & forallr @ [?S @ ?1] , [?P @ ?1] A8pt16U AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forall forallr M8pt19E 8pt19E forsomer @ [?R @ ?1] , [forsomer @ [?Q @ ?2] , [?P @ ?1 , ?2]] forsomer @ [?Q @ ?1] , [forsomer @ [?R @ ?2] , [?P @ ?2 , ?1]] A8pt19E AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forall forallr forsomer M8pt19U 8pt19U forallr @ [?R @ ?1] , [forallr @ [?Q @ ?2] , [?P @ ?1 , ?2]] forallr @ [?Q @ ?1] , [forallr @ [?R @ ?2] , [?P @ ?2 , ?1]] A8pt19U AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forall forallr M9pt10 9pt10 (forallr @ [(?Q @ ?1) | ?R @ ?1] , [?P @ ?1]) -> forallr @ [?Q @ ?1] , [?P @ ?1] true A9pt10 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forall forallr M9pt11 9pt11 (forallr @ [?R @ ?1] , [(?P @ ?1) & ?Q @ ?1]) -> forallr @ [?R @ ?1] , [?P @ ?1] true A9pt11 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forall forallr M9pt16a 9pt16a @ ?x , ?thm ?y (9pt16a1 @ ?thm) => (BIND @ ?x) => ?y A9pt16a CASEINTRO forall M9pt16a1 9pt16a1 @ ?thm ?P @ ?x (LEFT @ ?thm) => (forall @ [?P @ ?1]) || true , [?P @ ?1] @ ?x A9pt16a1 CASEINTRO forall M9pt16b 9pt16b @ ?thm forall @ [?P @ ?1] (FORALLDROP ** AT) => forall @ [?thm => ?P @ ?1] A9pt16b AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR forall M9pt18a 9pt18a ~forsomer @ [?R @ ?1] , [ ~?P @ ?1] forallr @ [?R @ ?1] , [?P @ ?1] A9pt18a ASSERT BOOLDEF CASEINTRO EQUATION IF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES forall forallr forsomer M9pt18b 9pt18b ~forsomer @ [?R @ ?1] , [?P @ ?1] forallr @ [?R @ ?1] , [ ~?P @ ?1] A9pt18b BOOLDEF CASEINTRO EQUATION IF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX forall forallr forsomer M9pt18c 9pt18c forsomer @ [?R @ ?1] , [ ~?P @ ?1] ~forallr @ [?R @ ?1] , [?P @ ?1] A9pt18c ASSERT BOOLDEF CASEINTRO EQUATION IF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES forallr forsomer M9pt20 9pt20 forsomer @ [(?Q @ ?1) & ?R @ ?1] , [?P @ ?1] forsomer @ [?Q @ ?1] , [(?R @ ?1) & ?P @ ?1] A9pt20 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forallr forsome forsomer M9pt21 9pt21 forsomer @ [?R @ ?1] , [?P & ?Q @ ?1] ?P & forsomer @ [?R @ ?1] , [?Q @ ?1] A9pt21 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forall forallr forsomer M9pt22 9pt22 forsomer @ [?R @ ?1] , [?P] ?P & forsome @ [?R @ ?1] A9pt22 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forall forallr forsome forsomer M9pt23 9pt23 (forsome @ [?R @ ?1]) -> (forsomer @ [?R @ ?1] , [?P | ?Q @ ?1]) == ?P | forsomer @ [?R @ ?1] , [?Q @ ?1] true A9pt23 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forall forallr forsome forsomer M9pt24 9pt24 forsomer @ [?R @ ?1] , [false] false A9pt24 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forall forallr forsomer M9pt25 9pt25 (forsomer @ [?R @ ?1] , [?P @ ?1]) -> forsomer @ [(?Q @ ?1) | ?R @ ?1] , [?P @ ?1] true A9pt25 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forall forallr forsomer M9pt26 9pt26 (forsomer @ [?R @ ?1] , [?P @ ?1]) -> forsomer @ [?R @ ?1] , [(?P @ ?1) | ?Q @ ?1] true A9pt26 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forall forallr forsome forsomer M9pt30a 9pt30a @ ?thm (?P @ ?x) -> ?Q (LEFT @ ?thm) => ((forsome @ [?P @ ?1]) -> ?Q) || true , [(?P @ ?1) -> ?Q] @ ?x A9pt30a AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR forall forsome M9pt30b 9pt30b @ ?thm (forsome @ [?P @ ?1]) -> ?Q (FORALLDROP ** AT) => forall @ [?thm => (?P @ ?1) -> ?Q] A9pt30b AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR forall forsome M9pt3a 9pt3a forallr @ [?R @ ?1] , [?P @ ?1] forall @ [( ~?R @ ?1) | ?P @ ?1] A9pt3a AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forallr M9pt3b 9pt3b forallr @ [?R @ ?1] , [?P @ ?1] forall @ [((?R @ ?1) & ?P @ ?1) == ?R @ ?1] A9pt3b AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forallr M9pt3c 9pt3c forallr @ [?R @ ?1] , [?P @ ?1] forall @ [((?R @ ?1) | ?P @ ?1) == ?P @ ?1] A9pt3c AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forallr M9pt4a 9pt4a forallr @ [(?Q @ ?1) & ?R @ ?1] , [?P @ ?1] forallr @ [?Q @ ?1] , [(?R @ ?1) -> ?P @ ?1] A9pt4a AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forallr M9pt4b 9pt4b forallr @ [(?Q @ ?1) & ?R @ ?1] , [?P @ ?1] forallr @ [?Q @ ?1] , [( ~?R @ ?1) | ?P @ ?1] A9pt4b AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forallr M9pt4c 9pt4c forallr @ [(?Q @ ?1) & ?R @ ?1] , [?P @ ?1] forallr @ [?Q @ ?1] , [((?R @ ?1) & ?P @ ?1) == ?R @ ?1] A9pt4c AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forallr M9pt4d 9pt4d forallr @ [(?Q @ ?1) & ?R @ ?1] , [?P @ ?1] forallr @ [?Q @ ?1] , [((?R @ ?1) | ?P @ ?1) == ?P @ ?1] A9pt4d AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forallr M9pt5 9pt5 ?P | forallr @ [?R @ ?1] , [?Q @ ?1] forallr @ [?R @ ?1] , [?P | ?Q @ ?1] A9pt5 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forall forallr M9pt6 9pt6 forallr @ [?R @ ?1] , [?P] ?P | forall @ [ ~?R @ ?1] A9pt6 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forall forallr M9pt7 9pt7 ( ~forall @ [ ~?R @ ?1]) -> (forallr @ [?R @ ?1] , [?P & ?Q @ ?1]) == ?P & forallr @ [?R @ ?1] , [?Q @ ?1] true A9pt7 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forall forallr M9pt8 9pt8 forallr @ [?R @ ?1] , [true] true A9pt8 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forall forallr MABS ABS @ ?x ?a (ABS2 @ ?x) =>> (ABSTRACT1 @ ?x) => ?a AABS IGNOREFIRST Id MABS2 ABS2 @ ?x ?a (IGNOREFIRST ** ABSTRACT4 @ ?x) =>> ABSREST => (ABSSETUP @ ?x) => ?a AABS2 IGNOREFIRST Id MABS3 ABS3 [?f ^+ ?g] @ ?x IGNOREFIRST =>> ABSREST2 => ABSSETUP2 => [?f ^+ ?g] @ ?x AABS3 IGNOREFIRST MABSREST ABSREST ((?a @ ?y) ^+ ?b @ ?z) . ?a ^+ ?b RAISE => ((ABS @ ?y) => ?a) ^+ (ABS @ ?z) => ?b AABSREST IGNOREFIRST Id MABSREST2 ABSREST2 (([?f] @ ?y) ^+ [?g] @ ?z) . [?f ^+ ?g] @ ?x RAISE => (ABS3 => (ABSTRACT4 @ ?y) => ?f) ^+ ABS3 => (ABSTRACT4 @ ?z) => ?g AABSREST2 IGNOREFIRST MABSSETUP ABSSETUP @ ?x ?a ^+ ?b (RAISE <= (?a :^+ ?b) @ ?x) . ?a ^+ ?b AABSSETUP IGNOREFIRST MABSSETUP2 ABSSETUP2 [?f ^+ ?g] @ ?x (RAISE <= ([?f] :^+ [?g]) @ ?x) . [?f ^+ ?g] @ ?x AABSSETUP2 IGNOREFIRST MABSTRACT ABSTRACT @ ?x ?a (ABSTRACT4 @ ?x) =>> (ABSTRACT3 @ ?x) =>> (ABSTRACT2 @ ?x) =>> (ABSTRACT1 @ ?x) => ?a AABSTRACT COMP Id MABSTRACT1 ABSTRACT1 @ ?x ?x Id @ ?x AABSTRACT1 Id MABSTRACT2 ABSTRACT2 @ ?x ?f @ ?a COMP <= ?f @ (ABSTRACT @ ?x) => ?a AABSTRACT2 COMP Id MABSTRACT3 ABSTRACT3 @ ?x ?a ^& ?b RAISE0 => ((ABSTRACT @ ?x) => ?a) ^& (ABSTRACT @ ?x) => ?b AABSTRACT3 COMP Id MABSTRACT4 ABSTRACT4 @ ?x ?a [?a] @ ?x AABSTRACT4 MADD_CANCEL ADD_CANCEL (?z + ?x) = ?z + ?y (Real : ?x) = Real : ?y AADD_CANCEL BUILTIN CASEINTRO EQUATION PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE REFLEX TYPES MADD_MONO_LEQ ADD_MONO_LEQ ((Nat : ?m) + Nat : ?n) =< (Nat : ?m) + Nat : ?p (Nat : ?n) =< Nat : ?p AADD_MONO_LEQ AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MAF AF |-false false AAF AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MALLASSERTS ALLASSERTS |- |-?x ALLASSERTS => |-?x AALLASSERTS ASSERT TYPES MALLASSOCS ALLASSOCS @ ?thm ?x (RIGHT @ ALLASSOCS @ ?thm) => (ASSOCS @ ?thm) => ?x AALLASSOCS MALL_CANCEL ALL_CANCEL ?x (TREMTOP @ MINUSTYPE) => (TREMTOP @ PLUSTYPE) => ALL_CANCEL_7 => (EVERYWHERE @ TREMRIGHT @ PLUSTYPE) => (EVERYWHERE @ TREMLEFT @ PLUSTYPE) => (EVERYWHERE @ TYPES) => (TOPDOWN @ MINUSMINUS) => (EVERYWHERE @ PLUSINVDISTS) => (EVERYWHERE @ BREAKMINUS ** FIXBREAKMINUS) => ?x AALL_CANCEL BUILTIN CASEINTRO MINUSTYPE PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE REFLEX TYPES MALL_CANCEL_1 ALL_CANCEL_1 ( -?x) + ?x 0 AALL_CANCEL_1 BUILTIN CASEINTRO PLUSCOMP PLUSMINUS PLUSTYPE REFLEX TYPES MALL_CANCEL_2 ALL_CANCEL_2 ?x + -?x 0 AALL_CANCEL_2 BUILTIN CASEINTRO PLUSCOMM PLUSCOMP PLUSMINUS PLUSTYPE REFLEX TYPES MALL_CANCEL_3 ALL_CANCEL_3 ?x + ( -?x) + ?y Real : ?y AALL_CANCEL_3 BUILTIN CASEINTRO PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE REFLEX TYPES MALL_CANCEL_4 ALL_CANCEL_4 ( -?x) + ?x + ?y Real : ?y AALL_CANCEL_4 BUILTIN CASEINTRO PLUSASSOC PLUSCOMP PLUSID PLUSMINUS PLUSTYPE REFLEX TYPES MALL_CANCEL_5 ALL_CANCEL_5 ( -?x) + ?y ALL_CANCEL_4 =>> ALL_CANCEL_1 => ( -?x) + (GETPLUS @ ?x) => ?y AALL_CANCEL_5 BUILTIN CASEINTRO PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE REFLEX TYPES MALL_CANCEL_6 ALL_CANCEL_6 ?x + ?y ALL_CANCEL_3 =>> ALL_CANCEL_2 => ?x + (GETPLUS @ -?x) => ?y AALL_CANCEL_6 BUILTIN CASEINTRO PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE REFLEX TYPES MALL_CANCEL_7 ALL_CANCEL_7 ?x ALL_CANCEL_5 => ALL_CANCEL_6 => (TREMRIGHT @ PLUSTYPE) => (RIGHT @ ALL_CANCEL_7) => (ALLASSOCS @ PLUSASSOC) => ?x AALL_CANCEL_7 BUILTIN CASEINTRO PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE REFLEX TYPES MALL_EXP ALL_EXP ?p || ?a , ?b (ALL_EXP *> CN_EXP) =>> (ALL_EXP *> XOR_EXP) =>> (ALL_EXP *> IFF_EXP) =>> (ALL_EXP *> IF_EXP) =>> (ALL_EXP *> OR_EXP) =>> (ALL_EXP *> AND_EXP) =>> (ALL_EXP *> NOT_EXP) =>> (ALL_EXP *> ASSERT_EXP) => ?p || ?a , ?b AALL_EXP AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX XOR MALL_GEQ_0 ALL_GEQ_0 0 =< Nat : ?x true AALL_GEQ_0 AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MALL_STEPS ALL_STEPS @ ?ONE_STEP ?x . ?y (ALL_STEPS @ ?ONE_STEP) =>> STOPLOOP => (RIGHT @ ?ONE_STEP) => STARTLOOP => IGNOREFIRST => ?x . ?y AALL_STEPS IGNOREFIRST MALTORDEF ALTORDEF ?x | ?y (true = ?x) || true , true = ?y AALTORDEF AND CASEINTRO EQUATION NONTRIV NOT OR REFLEX MALT_POS_DEF ALT_POS_DEF Positive @ ?x 0 < ?x AALT_POS_DEF PLUSCOMM PLUSID PLUSMINUS POSTYPE REAL_LESS_DEF MALT_PUSH ALT_PUSH ?p || ?a , ?b CASEINTRO <= ?p || (ALT_PUSH => (EVERYWHERE @ 1 |-| 1) => ?a) , ALT_PUSH => (EVERYWHERE @ 1 |-| 1) => ?b AALT_PUSH CASEINTRO MALT_QUANT_AGAIN ALT_QUANT_AGAIN (forsome @ [forall @ [?P @ ?1 , ?2]]) -> forall @ [forsome @ [?P @ ?2 , ?1]] true AALT_QUANT_AGAIN AND BOOLDEF CASEINTRO CHOICE COUNTER1 EQUATION IF NONTRIV NOT ODDCHOICE OR REFLEX forall forsome MALT_QUANT_IMP ALT_QUANT_IMP (forsome @ [forall @ [?P @ ?1 , ?2]]) -> forall @ [forsome @ [?P @ ?2 , ?1]] true AALT_QUANT_IMP AND BOOLDEF CASEINTRO EQUATION IF NONTRIV NOT ODDCHOICE OR REFLEX forall forsome MAND AND ?x & ?y (true = ?x) || (true = ?y) , false AAND AND MANDBOOL ANDBOOL ?x & ?y bool : ?x & ?y AANDBOOL AND BOOLDEF CASEINTRO EQUATION NONTRIV ODDCHOICE MANDSCIN ANDSCIN (bool : ?x) & bool : ?y ?x & ?y AANDSCIN AND BOOLDEF CASEINTRO EQUATION NONTRIV ODDCHOICE REFLEX TYPES MANDUNPACK ANDUNPACK (?P & ?Q) || ?x , ?y (true = ?P) || ((true = ?Q) || ?x , ?y) , ?y AANDUNPACK AND CASEINTRO MAND_EXP AND_EXP (?p & ?q) || ?a , ?b ?p || (?q || ?a , ?b) , ?b AAND_EXP AND CASEINTRO ODDCHOICE MANY_INSTANCE ANY_INSTANCE (?P @ ?x) -> ?P @ !!![?P @ ?1] true AANY_INSTANCE AND BOOLDEF CASEINTRO CHOICE EQUATION IF NONTRIV NOT ODDCHOICE OR REFLEX forall forsome MAP3pt86a AP3pt86a ?x -> ?p (THMAP @ LEFT , ?p , 3pt86a) => ?x -> ?p AAP3pt86a AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MAP3pt86b AP3pt86b ?x -> ?p | ?q (THMAP @ LEFT , ?p , 3pt86b) => ?x -> ?p | ?q AAP3pt86b AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MAP3pt88 AP3pt88 ?p | ?x (THMAP @ RIGHT , ?p , 3pt88) => ?p | ?x AAP3pt88 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MAPLZ APLZ (?e = ?f) & ?x ((RIGHT @ BIND @ ?e) ** LZ ** RIGHT @ EVAL) => (?e = ?f) & ?x AAPLZ AND BOOLDEF EQUATION ODDCHOICE MARROWTYPE ARROWTYPE (?t1 ->> ?t2) : ?f [?t2 : ?f @ ?t1 : ?1] AARROWTYPE ARROWTYPE MASRTCOND ASRTCOND ?a || ?b , ?c ( |-?a) || ?b , ?c AASRTCOND AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MASRTEQ ASRTEQ ?e = ?f |-?e = ?f AASRTEQ ASSERT BOOLDEF EQUATION ODDCHOICE MASRTLEFT ASRTLEFT @ ?p ?p ^+ ?q (RIGHT @ MKASRT @ ?p) => ((( |-?r) ^+ ?s) = ?r ^+ ?s) <= ?p ^+ ?q AASRTLEFT MASRTRIGHT ASRTRIGHT @ ?p ?q ^+ ?p (LEFT @ MKASRT @ ?p) => ((?r ^+ |-?s) = ?r ^+ ?s) <= ?q ^+ ?p AASRTRIGHT MASSERT ASSERT ?y |- ?x bool : ?x AASSERT ASSERT MASSERT2 ASSERT2 bool : ?x |-?x AASSERT2 ASSERT MASSERTCLEAN ASSERTCLEAN ?x |- ?y |-?y AASSERTCLEAN ASSERT MASSERTSCOUT ASSERTSCOUT ?y |- ?x bool : ?y |- ?x AASSERTSCOUT ASSERT TYPES MASSERT_EXP ASSERT_EXP ( |-?p) || ?x , ?y ?p || ?x , ?y AASSERT_EXP ASSERT BOOLDEF ODDCHOICE MASSERT_UNEXP ASSERT_UNEXP ?p || true , false |-?p AASSERT_UNEXP ASSERT BOOLDEF EQUATION ODDCHOICE MASSOCS ASSOCS @ ?thm ?x ((ASSOCS @ ?thm) *> ?thm) => ?x AASSOCS MASSRTBOTH ASSRTBOTH @ ?p ?p ^+ ?p ((?r ^+ |-?s) = ?r ^+ ?s) <= ((( |-?r) ^+ ?s) = ?r ^+ ?s) <= ?p ^+ ?p AASSRTBOTH MAT AT |-true true AAT AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MBALTDEF BALTDEF ?p == ?q (?p & ?q) | ( ~?p) & ~?q ABALTDEF AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MBASSOC BASSOC (?p == ?q) == ?r ?p == ?q == ?r ABASSOC AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MBCONV BCONV ?e == ?f ( |-?e) = |-?f ABCONV ASSERT IFF MBDIS BDIS ~?p == ?q ( ~?p) == ?q ABDIS AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MBEQSUBS BEQSUBS (?a == ?b) -> ?a (?a == ?b) -> ?b ABEQSUBS AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MBFLIP BFLIP ~?p == ?q ( ~?p) =/= ~?q ABFLIP AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MBID BID ?p == ?p true ABID AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX XOR MBID2 BID2 ?p == true |-?p ABID2 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MBIDF BIDF @ ?p true ?p == ?p ABIDF AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX XOR MBOOLDEF BOOLDEF bool : ?x true = ?x ABOOLDEF BOOLDEF MBOUNDED_N BOUNDED_N (((Nat : ?m) < Nat : ?n) & (Nat : ?n) =< 1 + Nat : ?m) -> (Nat : ?n) = 1 + Nat : ?m true ABOUNDED_N AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MBREAKMINUS BREAKMINUS ?x - ?y ?x + -?y ABREAKMINUS BUILTIN CASEINTRO MINUSTYPE PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE REFLEX TYPES MBRULE1 BRULE1 |-?p == ?q ?p == ?q ABRULE1 ASSERT BOOLDEF EQUATION IFF ODDCHOICE TYPES MBRULE2 BRULE2 ( |-?p) == ?q ?p == ?q ABRULE2 ASSERT BOOLDEF EQUATION IFF ODDCHOICE TYPES MBRULE3 BRULE3 ?p == |-?q ?p == ?q ABRULE3 ASSERT BOOLDEF EQUATION IFF ODDCHOICE TYPES MBSYM BSYM ?p == ?q ?q == ?p ABSYM AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MBTYPE BTYPE ?p == ?q |-( |-?p) == |-?q ABTYPE ASSERT BOOLDEF EQUATION IFF ODDCHOICE TYPES MBUILTIN BUILTIN 0 +! ?x Nat : ?x ABUILTIN BUILTIN MCASEINTRO CASEINTRO ?x ?y || ?x , ?x ACASEINTRO CASEINTRO MCASEPREP CASEPREP ?a || ?b , ?c ?a || (ALLASSERTS => (?b = |-?b) => ?b) , ALLASSERTS => (?c = |-?c) => ?c ACASEPREP ASSERT TYPES MCASSOC CASSOC (?p & ?q) & ?r ?p & ?q & ?r ACASSOC AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MCCON CCON ?p & ~?p false ACCON AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MCDISC CDISC ?p & ?q & ?r (?p & ?q) & ?p & ?r ACDISC AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MCDISD CDISD ?p & ?q | ?r (?p & ?q) | ?p & ?r ACDISD AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MCEX CEX forall @ [?P @ ?1] bool : ?P @ ***[?P @ ?1] ACEX BOOLDEF CASEINTRO CHOICE COUNTER1 EQUATION NONTRIV NOT ODDCHOICE REFLEX forall forsome MCEX_TAC CEX_TAC forall @ [?P @ ?1] bool : EVAL => ?P @ ***[?P @ ?1] ACEX_TAC BOOLDEF CASEINTRO CHOICE COUNTER1 EQUATION NONTRIV NOT ODDCHOICE REFLEX forall forsome MCHOICE CHOICE forsome @ [?P @ ?1] ?P @ !!![?P @ ?1] ACHOICE CHOICE MCHOICE_TAC CHOICE_TAC forsome @ [?P @ ?1] EVAL => ?P @ !!![?P @ ?1] ACHOICE_TAC CHOICE MCID CID ?p & true |-?p ACID AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MCIDEM CIDEM ?p & ?p |-?p ACIDEM AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MCNBOOL CNBOOL ?x <- ?y bool : ?x <- ?y ACNBOOL BOOLDEF CASEINTRO CONVIF EQUATION IF NONTRIV NOT ODDCHOICE OR REFLEX MCNRULE1 CNRULE1 |-?p <- ?q ?p <- ?q ACNRULE1 ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF NONTRIV NOT ODDCHOICE OR REFLEX TYPES MCNRULE2 CNRULE2 ( |-?p) <- ?q ?p <- ?q ACNRULE2 ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF NONTRIV NOT ODDCHOICE OR REFLEX TYPES MCNRULE3 CNRULE3 ?p <- |-?q ?p <- ?q ACNRULE3 ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF NONTRIV NOT ODDCHOICE OR REFLEX TYPES MCN_EXP CN_EXP (?p <- ?q) || ?a , ?b ?q || (?p || ?a , ?b) , ?a ACN_EXP AND CASEINTRO CONVIF IF NOT ODDCHOICE OR MCOMMDIST COMMDIST (?x + ?y) * ?z (?x * ?z) + ?y * ?z ACOMMDIST DIST TIMESCOMM MCOMMPLUSID COMMPLUSID ?x + 0 Real : ?x ACOMMPLUSID PLUSCOMM PLUSID MCOMMUTE_LEVEL_QUANT COMMUTE_LEVEL_QUANT (forall @ [forall @ [?P @ ?1 , ?2]]) == forall @ [forall @ [?P @ ?2 , ?1]] true ACOMMUTE_LEVEL_QUANT AND ASSERT BOOLDEF CASEINTRO CHOICE CONVIF COUNTER1 EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX XOR forall forsome MCOMP COMP (?f @@ ?g) @ ?x ?f @ ?g @ ?x ACOMP COMP MCONDCASES CONDCASES (?a & ?b) | ( ~?a) & ?c |-?a || ?b , ?c ACONDCASES AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MCONDCASES2 CONDCASES2 ?a || ( |-?b) , |-?c (?a & ?b) | ( ~?a) & ?c ACONDCASES2 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MCONDCASESL1 CONDCASESL1 (?a || ?b , ?c) == (?a & ?b) | ( ~?a) & ?c true ACONDCASESL1 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MCONDCASESL1F CONDCASESL1F @ ?a , ?b , ?c true (?a || ?b , ?c) == (?a & ?b) | ( ~?a) & ?c ACONDCASESL1F AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MCONDSIMP CONDSIMP ?a || ( |-?b) , |-?c DSYM =>> DZER =>> DID => DSYM => (DID ** DZER) => XORALTDEF => BALTDEF <= (DRULE1 ** DRULE2) => (RL @ CRULE1 ** CRULE2 ** CID ** CZER) => (?a & ?b) | ( ~?a) & ?c ACONDSIMP AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MCONS CONS ?p -> ?q ?q <- ?p ACONS AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MCONSCIN CONSCIN (bool : ?x) <- bool : ?y ?x <- ?y ACONSCIN ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF NONTRIV NOT ODDCHOICE OR REFLEX TYPES MCONSTRUCTBOOL CONSTRUCTBOOL ([true] <+> [false]) : ?x bool : ?x ACONSTRUCTBOOL BOOLDEF CASEINTRO EQUATION POINTTYPE REFLEX UNIONTYPE MCONTP CONTP ?p -> ?q ( ~?q) -> ~?p ACONTP AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MCONTYPE CONTYPE ?p <- ?q |-( |-?p) <- |-?q ACONTYPE ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF NONTRIV NOT ODDCHOICE OR REFLEX MCONVANDIMP CONVANDIMP @ ?thm ?p -> ?q BID => BRULE2 => (?thm => ?p & ?q) == ?p ACONVANDIMP AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MCONVANDOR CONVANDOR @ ?thm ?p | ?q DID => ?q | FDEF <= ~(CONVANDIMP @ ?thm) => ?p -> ?q ACONVANDOR AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MCONVERT_IMP_1 CONVERT_IMP_1 @ ?thm ?p -> ?q 3pt76b => (LEFT @ ?thm) => ( $IRULE2) => ?p -> ?q ACONVERT_IMP_1 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MCONVERT_IMP_2 CONVERT_IMP_2 @ ?thm , ?q |-?p CRULE1 => DID => (?p & ?q) | FDEF <= ~?thm => ?p -> ?q ACONVERT_IMP_2 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MCONVIF CONVIF ?p <- ?q ?q -> ?p ACONVIF CONVIF MCONVIMPAND CONVIMPAND @ ?thm ?p & ?q CID => ?p & ?thm => ?p -> ?q ACONVIMPAND AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MCONVIMPOR CONVIMPOR @ ?thm ?p | ?q DID => ?q | FDEF <= ~?thm => ?p -> ?q ACONVIMPOR AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MCONVORAND CONVORAND @ ?thm ?p & ?q BID2 => (RIGHT @ BID) => BASSOC => BRULE3 => (?p == ?q) == ?thm => ?p | ?q ACONVORAND AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MCONVORIMP CONVORIMP @ ?thm ?p -> ?q BID => BRULE2 => (?thm => ?p | ?q) == ?q ACONVORIMP AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MCOUNTER COUNTER ***[?P @ ?1] !!![ ~?P @ ?1] ACOUNTER BOOLDEF CASEINTRO COUNTER1 EQUATION NONTRIV NOT ODDCHOICE REFLEX MCOUNTER1 COUNTER1 ***?P !!![ ~?P @ ?1] ACOUNTER1 COUNTER1 MCRULE1 CRULE1 |-?p & ?q ?p & ?q ACRULE1 AND ASSERT BOOLDEF CASEINTRO EQUATION NONTRIV ODDCHOICE REFLEX TYPES MCRULE2 CRULE2 ( |-?p) & ?q ?p & ?q ACRULE2 AND ASSERT BOOLDEF CASEINTRO EQUATION NONTRIV ODDCHOICE REFLEX TYPES MCRULE3 CRULE3 ?p & |-?q ?p & ?q ACRULE3 AND ASSERT BOOLDEF CASEINTRO EQUATION NONTRIV ODDCHOICE REFLEX TYPES MCSYM CSYM ?p & ?q ?q & ?p ACSYM AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MCTYPE CTYPE ?p & ?q |-( |-?p) & |-?q ACTYPE AND ASSERT BOOLDEF CASEINTRO EQUATION NONTRIV ODDCHOICE REFLEX TYPES MCZER CZER ?p & false false ACZER AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MCZERF CZERF @ ?p false ?p & false ACZERF AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MDASSOC DASSOC (?p | ?q) | ?r ?p | ?q | ?r ADASSOC AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MDDIS DDIS ?p | ?q == ?r (?p | ?q) == ?p | ?r ADDIS AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MDDISC DDISC ?p | ?q & ?r (?p | ?q) & ?p | ?r ADDISC AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MDDISD DDISD ?p | ?q | ?r (?p | ?q) | ?p | ?r ADDISD AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MDEMa DEMa ( ~?p) | ~?q ~?p & ?q ADEMa AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MDEMb DEMb ( ~?p) & ~?q ~?p | ?q ADEMb AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MDID DID ?p | false |-?p ADID AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MDIDEM DIDEM ?p | ?p |-?p ADIDEM AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MDIFF_EQ DIFF_EQ 0 = ?y - ?x (Real : ?x) = Real : ?y ADIFF_EQ BUILTIN CASEINTRO EQUATION MINUSTYPE PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE REFLEX TYPES MDINSTANTIATE DINSTANTIATE (?P @ ?x) | forsome @ [?P @ ?1] forsome @ ?P ADINSTANTIATE AND BOOLDEF CASEINTRO EQUATION NONTRIV NOT ODDCHOICE OR REFLEX forall forsome MDINSTANTIATEF1 DINSTANTIATEF1 @ ?x forsome @ ?P (?P @ ?x) | forsome @ [?P @ ?1] ADINSTANTIATEF1 AND BOOLDEF CASEINTRO EQUATION NONTRIV NOT ODDCHOICE OR REFLEX forall forsome MDIST DIST ?x * ?y + ?z (?x * ?y) + ?x * ?z ADIST DIST MDIVCOMP DIVCOMP ?x / ?y ?x /! ?y ADIVCOMP DIVCOMP MDIVSCIN DIVSCIN ?x / ?y (Nat : ?x) / Nat : ?y ADIVSCIN DIVTYPE TYPES MDIVTYPE DIVTYPE ?x / ?y Nat : (Nat : ?x) / Nat : ?y ADIVTYPE DIVTYPE MDRULE1 DRULE1 |-?p | ?q ?p | ?q ADRULE1 ASSERT BOOLDEF CASEINTRO EQUATION NONTRIV NOT ODDCHOICE OR REFLEX TYPES MDRULE2 DRULE2 ( |-?p) | ?q ?p | ?q ADRULE2 ASSERT BOOLDEF CASEINTRO EQUATION NONTRIV NOT ODDCHOICE OR REFLEX TYPES MDRULE3 DRULE3 ?p | |-?q ?p | ?q ADRULE3 ASSERT BOOLDEF CASEINTRO EQUATION NONTRIV NOT ODDCHOICE OR REFLEX TYPES MDSYM DSYM ?p | ?q ?q | ?p ADSYM AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MDTYPE DTYPE ?p | ?q |-( |-?p) | |-?q ADTYPE ASSERT BOOLDEF CASEINTRO EQUATION NONTRIV NOT ODDCHOICE OR REFLEX MDUAL DUAL @ ?thm ?x REMFLIP => (RIGHT @ ?thm) => FLIPALL => ?x ADUAL AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MDUBNEG DUBNEG ~ ~?p bool : ?p ADUBNEG BOOLDEF CASEINTRO EQUATION NONTRIV NOT REFLEX MDUBNEG2 DUBNEG2 ~ ~?p |-?p ADUBNEG2 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MDXM DXM ?p | ~?p true ADXM AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX XOR MDXMF DXMF @ ?p true ?p | ~?p ADXMF AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX XOR MDZER DZER ?p | true true ADZER AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MDZERF DZERF @ ?p true ?p | true ADZERF AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MEPLUSID EPLUSID ?x + ?y COMMPLUSID =>> PLUSID => ?x + ?y AEPLUSID PLUSCOMM PLUSID MEQBOOL EQBOOL ?x = ?y bool : ?x = ?y AEQBOOL BOOLDEF EQUATION ODDCHOICE MEQEVAL2 EQEVAL2 (Nat : ?a) = 0 ?a =! 0 AEQEVAL2 BUILTIN EVALEQ MEQSYMM EQSYMM ?x = ?y ?y = ?x AEQSYMM CASEINTRO EQUATION REFLEX MEQT EQT ( |-?p) = true ?p = true AEQT ASSERT BOOLDEF CASEINTRO EQUATION REFLEX TYPES MEQUATION EQUATION ?a = ?b (?a = ?b) || true , false AEQUATION EQUATION MEQUATION_TO_DIFFERENCE EQUATION_TO_DIFFERENCE (Real : ?m) = Real : ?n (?m - ?n) = 0 AEQUATION_TO_DIFFERENCE BUILTIN CASEINTRO EQUATION MINUSTYPE PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE REFLEX TYPES MEQ_LEQ EQ_LEQ ((Nat : ?m) =< Nat : ?n) & (Nat : ?n) =< Nat : ?m (Nat : ?m) = Nat : ?n AEQ_LEQ AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MEQ_NOT_LESS EQ_NOT_LESS ((Nat : ?x) = Nat : ?y) -> ~(Nat : ?x) < Nat : ?y true AEQ_NOT_LESS AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF LESS1 NONTRIV NOT ODDCHOICE OR PLUSTYPE REFLEX TYPES XOR forall forsome MEQ_NOT_LESSF EQ_NOT_LESSF @ ?x , ?y true ((Nat : ?x) = Nat : ?y) -> ~(Nat : ?x) < Nat : ?y AEQ_NOT_LESSF AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF LESS1 NONTRIV NOT ODDCHOICE OR PLUSTYPE REFLEX TYPES XOR forall forsome MEQ_TRANS EQ_TRANS ((?x = ?y) & ?y = ?z) -> ?x = ?z true AEQ_TRANS AND CASEINTRO EQUATION IF NONTRIV NOT ODDCHOICE OR REFLEX MEVALEQ EVALEQ ?x =! ?y (Nat : ?x) = Nat : ?y AEVALEQ EVALEQ MEVERYWHERE EVERYWHERE @ ?thm ?x ?thm =>> (EVERYWHERE_INFIX @ EVERYWHERE , ?thm) =>> (EVERYWHERE_CASE @ EVERYWHERE , ?thm) => ?x AEVERYWHERE MEVERYWHERE2 EVERYWHERE2 @ ?thm ?x ?thm =>> (EVERYWHERE_ABS @ EVERYWHERE2 , ?thm) =>> (EVERYWHERE_INFIX @ EVERYWHERE2 , ?thm) =>> (STRONG_EVERYWHERE_CASE @ EVERYWHERE2 , ?thm) => ?x AEVERYWHERE2 MEVERYWHERE_ABS EVERYWHERE_ABS @ ?EVERYWHERE , ?thm [?f @ ?1] ?thm => [(?EVERYWHERE @ ?thm) => ?f @ ?1] AEVERYWHERE_ABS MEVERYWHERE_CASE EVERYWHERE_CASE @ ?EVERYWHERE , ?thm ?a || ?x , ?y ?thm => ?a || ((?EVERYWHERE @ ?thm) => ?x) , (?EVERYWHERE @ ?thm) => ?y AEVERYWHERE_CASE MEVERYWHERE_INFIX EVERYWHERE_INFIX @ ?EVERYWHERE , ?thm ?x ^+ ?y ?thm => ((?EVERYWHERE @ ?thm) => ?x) ^+ (?EVERYWHERE @ ?thm) => ?y AEVERYWHERE_INFIX MEXAMPLE1 EXAMPLE1 forall @ [forsome @ [?1 = ?2]] true AEXAMPLE1 BOOLDEF CASEINTRO EQUATION NONTRIV NOT ODDCHOICE REFLEX forall forsome MElimForall ElimForall @ ?thm , ?x true ASSERT2 <= CID => (LEFT @ EVAL) => (RIGHT @ ?thm) => (INSTANTIATEF @ ?x) => ?thm <= true AElimForall AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR forall MFACTORZERO FACTORZERO 0 = ?y * ?z (0 = Real : ?y) | 0 = Real : ?z AFACTORZERO AND BUILTIN CASEINTRO DIST EQUATION NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMP PLUSID PLUSMINUS PLUSTYPE REALDIVTYPE REFLEX TIMESASSOC TIMESCOMM TIMESDIV TIMESTYPE TYPES MFALSEBOOL FALSEBOOL false bool : false AFALSEBOOL BOOLDEF EQUATION NONTRIV ODDCHOICE MFDEF FDEF false ~true AFDEF AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX XOR MFINDGCD FINDGCD gcd @ ?a , ?b (GCD2 ** (RIGHT @ RIGHT @ MODCOMP) ** FINDGCD) =>> GCD1 => gcd @ ?a , ?b AFINDGCD GCD1 GCD2 MODCOMP MFIXBREAKMINUS FIXBREAKMINUS 0 + -?x -?x AFIXBREAKMINUS MINUSTYPE PLUSID TYPES MFLEQ_ADD FLEQ_ADD forall @ [(Nat : ?m) =< (Nat : ?m) + Nat : ?1] true AFLEQ_ADD AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MFLESS_ADD_NZ FLESS_ADD_NZ forall @ [( ~(Nat : ?1) = 0) -> (Nat : ?m) < (Nat : ?m) + Nat : ?1] true AFLESS_ADD_NZ AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC SUCCNOTZERO TYPES XOR forall forsome MFLESS_ADD_SUC FLESS_ADD_SUC forall @ [(Nat : ?1) < (Nat : ?1) + 1 + Nat : ?n] true AFLESS_ADD_SUC AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMP PLUSID PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MFLESS_MONO_MULT FLESS_MONO_MULT forall @ [((Nat : ?m) =< Nat : ?n) -> ((Nat : ?m) * Nat : ?1) =< (Nat : ?n) * Nat : ?1] true AFLESS_MONO_MULT AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF DIST EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TIMESCOMM TIMESID TIMESTYPE TIMESTYPE2 TYPES XOR forall forsome MFLIPALL FLIPALL ?x SFLIPALL => DUBNEG2 <= CRULE1 <<= DRULE1 <<= XRULE1 <<= BRULE1 <= ?x AFLIPALL AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MFLIPPASTA FLIPPASTA ~ |-?p |-SFLIPALL => ~?p AFLIPPASTA AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MFLIPPASTB FLIPPASTB ~?x == ?y (SFLIPALL => ~?x) =/= SFLIPALL => ~?y AFLIPPASTB AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MFLIPPASTC FLIPPASTC ~?x & ?y (SFLIPALL => ~?x) | SFLIPALL => ~?y AFLIPPASTC AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MFLIPPASTD FLIPPASTD ~?x | ?y (SFLIPALL => ~?x) & SFLIPALL => ~?y AFLIPPASTD AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MFLIPPASTN FLIPPASTN ~ ~?x ~SFLIPALL => ~?x AFLIPPASTN AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MFLIPPASTX FLIPPASTX ~?x =/= ?y (SFLIPALL => ~?x) == SFLIPALL => ~?y AFLIPPASTX AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MFNDIST FNDIST ?f @ ?x || ?y , ?z ?x || (?f @ ?y) , ?f @ ?z AFNDIST CASEINTRO MFNOT_LESS_0 FNOT_LESS_0 forall @ [ ~(Nat : ?1) < 0] true AFNOT_LESS_0 AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSTYPE PLUSTYPE2 REFLEX TYPES XOR forall forsome MFORALLBOOL FORALLBOOL forall @ ?P bool : forall @ ?P AFORALLBOOL BOOLDEF EQUATION ODDCHOICE forall MFORALLBOOL2 FORALLBOOL2 forall @ [bool : ?P @ ?1] forall @ [?P @ ?1] AFORALLBOOL2 BOOLDEF CASEINTRO EQUATION ODDCHOICE REFLEX forall MFORALLDIST FORALLDIST forall @ [(?P @ ?1) & ?Q @ ?1] (forall @ [?P @ ?1]) & forall @ [?Q @ ?1] AFORALLDIST AND BOOLDEF CASEINTRO EQUATION NONTRIV ODDCHOICE REFLEX TYPES forall MFORALLDROP FORALLDROP forall @ [?x] |-?x AFORALLDROP ASSERT BOOLDEF CASEINTRO EQUATION ODDCHOICE REFLEX forall MFORALLNOT FORALLNOT forall @ [ ~?P @ ?1] (forall @ [ ~?P @ ?1]) & ~forall @ [?P @ ?1] AFORALLNOT AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR forall MFORALLOR FORALLOR forall @ [(?P @ ?1) | ?Q @ ?1] (forall @ [?P @ ?1]) | forall @ [(?P @ ?1) | ?Q @ ?1] AFORALLOR AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR forall MFORALLORDIST FORALLORDIST forall @ [?P | ?Q @ ?1] ?P | forall @ [?Q @ ?1] AFORALLORDIST AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR forall MFORALLRBOOL FORALLRBOOL forallr @ ?x bool : forallr @ ?x AFORALLRBOOL BOOLDEF CASEINTRO EQUATION IF NONTRIV NOT ODDCHOICE OR REFLEX forall forallr MFORALLRBOOL2 FORALLRBOOL2 forallr @ [?R @ ?1] , [?P @ ?1] forallr @ [bool : ?R @ ?1] , [?P @ ?1] AFORALLRBOOL2 ASSERT BOOLDEF CASEINTRO EQUATION IF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES forallr MFORALLRBOOL3 FORALLRBOOL3 forallr @ [?R @ ?1] , [?P @ ?1] forallr @ [?R @ ?1] , [bool : ?P @ ?1] AFORALLRBOOL3 ASSERT BOOLDEF CASEINTRO EQUATION IF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES forallr MFORALLSWITCH FORALLSWITCH forall @ [forall @ [?P @ ?1 , ?2]] forall @ [forall @ [?P @ ?2 , ?1]] AFORALLSWITCH BOOLDEF CASEINTRO EQUATION ODDCHOICE REFLEX forall MFORALLSWITCH2 FORALLSWITCH2 forall @ [forall @ [(?P @ ?1) @ ?2]] forall @ [forall @ [bool : (?P @ ?2) @ ?1]] AFORALLSWITCH2 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR forall MFORALL_IMP_FORSOME_EQ FORALL_IMP_FORSOME_EQ forall @ [(?P @ ?1) -> ?Q] (forsome @ [?P @ ?1]) -> ?Q AFORALL_IMP_FORSOME_EQ AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR forall forsome MFORALL_LESS_0 FORALL_LESS_0 forall @ [0 < 1 + Nat : ?1] true AFORALL_LESS_0 AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MFORALL_LESS_ANTISYM FORALL_LESS_ANTISYM forall @ [ ~((Nat : ?m) < Nat : ?1) & (Nat : ?1) < Nat : ?m] true AFORALL_LESS_ANTISYM AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MFORALL_LESS_CASES FORALL_LESS_CASES forall @ [((Nat : ?1) < Nat : ?m) | ((Nat : ?1) = Nat : ?m) | (Nat : ?m) < Nat : ?1] true AFORALL_LESS_CASES AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MFORALL_LESS_MONO_ADD FORALL_LESS_MONO_ADD forall @ [((Nat : ?m) < Nat : ?n) -> ((Nat : ?m) + Nat : ?1) < (Nat : ?n) + Nat : ?1] true AFORALL_LESS_MONO_ADD AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MFORALL_LESS_MONO_ADDF FORALL_LESS_MONO_ADDF @ ?m , ?n true forall @ [((Nat : ?m) < Nat : ?n) -> ((Nat : ?m) + Nat : ?1) < (Nat : ?n) + Nat : ?1] AFORALL_LESS_MONO_ADDF AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MFORALL_LESS_MONO_ADD_INV FORALL_LESS_MONO_ADD_INV forall @ [(((Nat : ?m) + Nat : ?1) < (Nat : ?n) + Nat : ?1) -> (Nat : ?m) < Nat : ?n] true AFORALL_LESS_MONO_ADD_INV AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MFORALL_LESS_MONO_ADD_INVF FORALL_LESS_MONO_ADD_INVF @ ?m , ?n true forall @ [(((Nat : ?m) + Nat : ?1) < (Nat : ?n) + Nat : ?1) -> (Nat : ?m) < Nat : ?n] AFORALL_LESS_MONO_ADD_INVF AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MFORALL_LESS_SUC_REFL FORALL_LESS_SUC_REFL forall @ [(Nat : ?1) < 1 + Nat : ?1] true AFORALL_LESS_SUC_REFL AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MFORALL_LESS_TRANS FORALL_LESS_TRANS forall @ [(((Nat : ?m) < Nat : ?n) & (Nat : ?n) < Nat : ?1) -> (Nat : ?m) < Nat : ?1] true AFORALL_LESS_TRANS AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MFORALL_NOTFORSOME FORALL_NOTFORSOME ~forsome @ ?P forall @ [ ~?P @ ?1] AFORALL_NOTFORSOME BOOLDEF CASEINTRO EQUATION NONTRIV NOT ODDCHOICE REFLEX forall forsome MFORSOMEBOOL FORSOMEBOOL forsome @ ?P bool : forsome @ ?P AFORSOMEBOOL BOOLDEF CASEINTRO EQUATION NONTRIV NOT ODDCHOICE REFLEX forsome MFORSOMEBOOL2 FORSOMEBOOL2 forsome @ [bool : ?P @ ?1] forsome @ [?P @ ?1] AFORSOMEBOOL2 BOOLDEF CASEINTRO EQUATION NONTRIV NOT ODDCHOICE REFLEX forsome MFORSOMEDIST2 FORSOMEDIST2 forsome @ [(?P @ ?1) & ?Q] (forsome @ [?P @ ?1]) & ?Q AFORSOMEDIST2 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR forall forsome MFORSOMEDROP FORSOMEDROP forsome @ [?x] |-?x AFORSOMEDROP AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR forall forsome MFORSOMERBOOL FORSOMERBOOL forsomer @ ?x bool : forsomer @ ?x AFORSOMERBOOL BOOLDEF CASEINTRO EQUATION NONTRIV NOT ODDCHOICE REFLEX forsomer MFORSOMERBOOL2 FORSOMERBOOL2 forsomer @ [?R @ ?1] , [?P @ ?1] forsomer @ [bool : ?R @ ?1] , [?P @ ?1] AFORSOMERBOOL2 ASSERT BOOLDEF CASEINTRO EQUATION IF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES forallr forsomer MFORSOMERBOOL3 FORSOMERBOOL3 forsomer @ [?R @ ?1] , [?P @ ?1] forsomer @ [?R @ ?1] , [bool : ?P @ ?1] AFORSOMERBOOL3 BOOLDEF CASEINTRO EQUATION NONTRIV NOT ODDCHOICE P1 P2 REFLEX forsomer MFORSOME_NOTFORALL FORSOME_NOTFORALL ~forall @ ?P forsome @ [ ~?P @ ?1] AFORSOME_NOTFORALL BOOLDEF CASEINTRO EQUATION NONTRIV NOT ODDCHOICE REFLEX forall forsome MGCD GCD gcd @ ?a , ?b (EQEVAL2 => (Nat : ?b) = 0) || (BUILTIN => BUILTIN <= TYPES => GCD1 => gcd @ (Nat : ?a) , 0) , GCD => gcd @ ?b , MODCOMP => ?a % ?b AGCD BUILTIN CASEINTRO EVALEQ GCD1 GCD2 GCDTYPE MODCOMP TYPES MGCD1 GCD1 gcd @ ?a , 0 Nat : ?a AGCD1 GCD1 MGCD2 GCD2 gcd @ ?a , ?b gcd @ ?b , ?a % ?b AGCD2 GCD2 MGCDTYPE GCDTYPE gcd @ ?a , ?b gcd @ (Nat : ?a) , Nat : ?b AGCDTYPE GCDTYPE MGCLEAN GCLEAN ?x (RL @ GCLEAN) => NRULE2 => NRULE1 => STL => STR => STT => (ALLASSERTS ** RIGHT @ (RIGHT @ ALLASSERTS) ** LEFT @ ALLASSERTS) => ?x AGCLEAN ASSERT BOOLDEF CASEINTRO EQUATION NONTRIV NOT ODDCHOICE REFLEX TYPES MGET GET @ ?y , ?comm , ?assoc ?x (GET2 @ ?y , ?comm , ?assoc) =>> (GET1 @ ?y , ?comm) => (RIGHT @ GET @ ?y , ?comm , ?assoc) =>> (GET0 @ ?y) => (ASSOCS @ ?assoc) => ?x AGET MGET0 GET0 @ ?x ?x ^+ ?y ?x ^+ ?y AGET0 MGET1 GET1 @ ?x , ?comm ?y ^+ ?x ?comm => ?y ^+ ?x AGET1 MGET2 GET2 @ ?x , ?comm , ?assoc ?y ^+ ?x ^+ ?z ?assoc => (LEFT @ ?comm) => ?assoc <= ?y ^+ ?x ^+ ?z AGET2 MGETPLUS GETPLUS @ ?z ?x + ?y (GET @ ?z , PLUSCOMM , PLUSASSOC) => ?x + ?y AGETPLUS PLUSASSOC PLUSCOMM MGR GR (?p & ?q) == ?p | ?q ?p == ?q AGR AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MGR2 GR2 (?p == ?q) == ?p | ?q ?p & ?q AGR2 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MGR3 GR3 (?p == ?q) == ?p & ?q ?p | ?q AGR3 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MGREATER GREATER ?x > ?y ?y < ?x AGREATER GREATER MGREATER_EQ GREATER_EQ (Nat : ?n) >= Nat : ?m (Nat : ?m) =< Nat : ?n AGREATER_EQ AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION GREATER GREATER_EQ_REAL IF IFF LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE REFLEX TYPES XOR MGREATER_EQ_REAL GREATER_EQ_REAL ?x >= ?y ((Real : ?x) = Real : ?y) | ?x > ?y AGREATER_EQ_REAL GREATER_EQ_REAL MGREATER_OR_EQ GREATER_OR_EQ (Nat : ?x) >= Nat : ?y ((Nat : ?x) > Nat : ?y) | (Nat : ?x) = Nat : ?y AGREATER_OR_EQ AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION GREATER_EQ_REAL IF IFF NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE REFLEX TYPES XOR MHYP HYP (?a = ?b) || (?f @ ?a) , ?c (?a = ?b) || (?f @ ?b) , ?c AHYP MID ID Id @ ?x ?x AID Id MIDEF IDEF ?p -> ?q (?p | ?q) == ?q AIDEF AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MIDEF2 IDEF2 ?p -> ?q ( ~?p) | ?q AIDEF2 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MIDEF3 IDEF3 ?p -> ?q (?p & ?q) == ?p AIDEF3 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MIDIS1 IDIS1 (?p | ?q) -> ?r (?p -> ?r) & ?q -> ?r AIDIS1 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MIDIS2 IDIS2 (?p & ?q) -> ?r (?p -> ?r) | ?q -> ?r AIDIS2 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MIDIS3 IDIS3 ?p -> ?q & ?r (?p -> ?q) & ?p -> ?r AIDIS3 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MIDIS4 IDIS4 ?p -> ?q | ?r (?p -> ?q) | ?p -> ?r AIDIS4 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MIDISB IDISB ?p -> ?q == ?r (?p -> ?q) == ?p -> ?r AIDISB AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MIF IF ?x -> ?y ( ~?x) | ?y AIF IF MIFBOOL IFBOOL ?x -> ?y bool : ?x -> ?y AIFBOOL BOOLDEF CASEINTRO EQUATION IF NONTRIV NOT ODDCHOICE OR REFLEX MIFF IFF ?x == ?y (bool : ?x) = bool : ?y AIFF IFF MIFFBOOL IFFBOOL ?x == ?y bool : ?x == ?y AIFFBOOL BOOLDEF EQUATION IFF ODDCHOICE MIFFSCIN IFFSCIN (bool : ?x) == bool : ?y ?x == ?y AIFFSCIN IFF TYPES MIFF_EXP IFF_EXP (?p == ?q) || ?a , ?b ?p || (?q || ?a , ?b) , ?q || ?b , ?a AIFF_EXP BOOLDEF CASEINTRO EQUATION IFF NONTRIV ODDCHOICE REFLEX MIFSCIN IFSCIN (bool : ?x) -> bool : ?y ?x -> ?y AIFSCIN BOOLDEF CASEINTRO EQUATION IF NONTRIV NOT ODDCHOICE OR REFLEX MIF_EXP IF_EXP (?p -> ?q) || ?a , ?b ?p || (?q || ?a , ?b) , ?a AIF_EXP AND CASEINTRO IF NOT ODDCHOICE OR MIGNOREFIRST IGNOREFIRST ?x . ?y ?y AIGNOREFIRST IGNOREFIRST MILID ILID true -> ?p |-?p AILID AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MIMPTOCOND IMPTOCOND ?a -> ?b |-?a || ?b , true AIMPTOCOND AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MIMPTYPE IMPTYPE ?p -> ?q |-( |-?p) -> |-?q AIMPTYPE ASSERT BOOLDEF CASEINTRO EQUATION IF NONTRIV NOT ODDCHOICE OR REFLEX MINDUCTION INDUCTION forall @ [?P @ Nat : ?1] (?P @ 0) & forall @ [(?P @ Nat : ?1) -> ?P @ 1 + Nat : ?1] AINDUCTION INDUCTION MINDUCT_TAC INDUCT_TAC forall @ [?P @ ?1] INDUCT_TAC_2 => INDUCT_TAC_1 => forall @ [?P @ ?1] AINDUCT_TAC BOOLDEF CASEINTRO EQUATION IF INDUCTION NONTRIV NOT ODDCHOICE OR PLUSTYPE REFLEX TYPES MINDUCT_TAC_1 INDUCT_TAC_1 forall @ [?P @ ?1] forall @ [(BIND @ Nat : ?1) => ?P @ ?1] AINDUCT_TAC_1 MINDUCT_TAC_2 INDUCT_TAC_2 forall @ [?P @ Nat : ?1] (EVAL => ?P @ 0) & forall @ [(EVAL => ?P @ Nat : ?1) -> EVAL => ?P @ 1 + Nat : ?1] AINDUCT_TAC_2 BOOLDEF CASEINTRO EQUATION IF INDUCTION NONTRIV NOT ODDCHOICE OR PLUSTYPE REFLEX TYPES MINSTANTIATE INSTANTIATE (?P @ ?x) & forall @ [?P @ ?1] forall @ [?P @ ?1] AINSTANTIATE AND BOOLDEF CASEINTRO EQUATION NONTRIV ODDCHOICE REFLEX forall MINSTANTIATEF INSTANTIATEF @ ?x forall @ [?P @ ?1] (?P @ ?x) & forall @ [?P @ ?1] AINSTANTIATEF AND BOOLDEF CASEINTRO EQUATION NONTRIV ODDCHOICE REFLEX forall MIREF IREF ?p -> ?p true AIREF AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MIREFF IREFF @ ?p true ?p -> ?p AIREFF AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MIRULE1 IRULE1 |-?p -> ?q ?p -> ?q AIRULE1 ASSERT BOOLDEF CASEINTRO EQUATION IF NONTRIV NOT ODDCHOICE OR REFLEX TYPES MIRULE2 IRULE2 ( |-?p) -> ?q ?p -> ?q AIRULE2 ASSERT BOOLDEF CASEINTRO EQUATION IF NONTRIV NOT ODDCHOICE OR REFLEX TYPES MIRULE3 IRULE3 ?p -> |-?q ?p -> ?q AIRULE3 ASSERT BOOLDEF CASEINTRO EQUATION IF NONTRIV NOT ODDCHOICE OR REFLEX TYPES MIRZER IRZER ?p -> true true AIRZER AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MIRZERF IRZERF @ ?p true ?p -> true AIRZERF AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MId Id Id @ ?x ?x AId Id ML L @ ?thm ?p ^+ ?q (?thm => ?p) ^+ ?q AL ML3pt43 L3pt43 ?p == ( ~?p) | ?q ?p & ?q AL3pt43 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MLABELINTRO LABELINTRO @ ?x ?y ?x . ?y ALABELINTRO IGNOREFIRST MLAMBDAINTRO LAMBDAINTRO ?x LAMBDAINTRO2 => LAMBDAINTRO1 => ?x ALAMBDAINTRO IGNOREFIRST MLAMBDAINTRO1 LAMBDAINTRO1 ?x ^+ ?y (RL @ LAMBDAINTRO) => ?x ^+ ?y ALAMBDAINTRO1 IGNOREFIRST MLAMBDAINTRO2 LAMBDAINTRO2 [?f @ ?1] [(LABELINTRO @ ?1) => LAMBDAINTRO => ?f @ ?1] ALAMBDAINTRO2 IGNOREFIRST MLAMBDAREMOVE LAMBDAREMOVE ?x LAMBDAREMOVE2 => LAMBDAREMOVE1 => ?x ALAMBDAREMOVE IGNOREFIRST MLAMBDAREMOVE1 LAMBDAREMOVE1 ?x ^+ ?y (RL @ LAMBDAREMOVE) => ?x ^+ ?y ALAMBDAREMOVE1 IGNOREFIRST MLAMBDAREMOVE2 LAMBDAREMOVE2 [?f @ ?1] [IGNOREFIRST => LAMBDAREMOVE => ?f @ ?1] ALAMBDAREMOVE2 IGNOREFIRST MLEFT LEFT @ ?thm ?p ^+ ?q (?thm => ?p) ^+ ?q ALEFT MLEFT_CASE LEFT_CASE @ ?thm ?x || ?y , ?z ?x || (?thm => ?y) , ?z ALEFT_CASE MLEQ_0 LEQ_0 (Nat : ?n) =< 0 (Nat : ?n) = 0 ALEQ_0 AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX TYPES XOR forall forsome MLEQ_ADD LEQ_ADD bool : (Nat : ?m) =< (Nat : ?m) + Nat : ?n true ALEQ_ADD AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLEQ_ADDF LEQ_ADDF @ ?m , ?n true bool : (Nat : ?m) =< (Nat : ?m) + Nat : ?n ALEQ_ADDF AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLEQ_ANTISYM LEQ_ANTISYM ~((Nat : ?m) < Nat : ?n) & (Nat : ?n) =< Nat : ?m true ALEQ_ANTISYM AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLEQ_CASES LEQ_CASES ((Nat : ?m) =< Nat : ?n) | (Nat : ?n) =< Nat : ?m true ALEQ_CASES AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLEQ_IMP_LESS_SUC LEQ_IMP_LESS_SUC ((Nat : ?n) =< Nat : ?m) -> (Nat : ?n) < 1 + Nat : ?m true ALEQ_IMP_LESS_SUC AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLEQ_LEQ_MONO LEQ_LEQ_MONO (((Nat : ?m) =< Nat : ?p) & (Nat : ?n) =< Nat : ?q) -> ((Nat : ?m) + Nat : ?n) =< (Nat : ?p) + Nat : ?q true ALEQ_LEQ_MONO AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLEQ_LESS_TRANS LEQ_LESS_TRANS (((Nat : ?m) =< Nat : ?n) & (Nat : ?n) < Nat : ?p) -> (Nat : ?m) < Nat : ?p true ALEQ_LESS_TRANS AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLEQ_MONO_ADD_EQ LEQ_MONO_ADD_EQ ((Nat : ?m) + Nat : ?p) =< (Nat : ?n) + Nat : ?p (Nat : ?m) =< Nat : ?n ALEQ_MONO_ADD_EQ AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLEQ_MONO_ADD_EQF LEQ_MONO_ADD_EQF @ ?p (Nat : ?m) =< Nat : ?n ((Nat : ?m) + Nat : ?p) =< (Nat : ?n) + Nat : ?p ALEQ_MONO_ADD_EQF AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLEQ_REFL LEQ_REFL (Nat : ?m) =< Nat : ?m true ALEQ_REFL AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE REFLEX TYPES XOR MLEQ_SUC LEQ_SUC (Nat : ?n) =< 1 + Nat : ?m ((Nat : ?n) =< Nat : ?m) | (Nat : ?n) = 1 + Nat : ?m ALEQ_SUC AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLEQ_SUC_REFL LEQ_SUC_REFL (Nat : ?m) =< 1 + Nat : ?m true ALEQ_SUC_REFL AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLEQ_TRANS LEQ_TRANS (((Nat : ?m) =< Nat : ?n) & (Nat : ?n) =< Nat : ?p) -> (Nat : ?m) =< Nat : ?p true ALEQ_TRANS AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS1 LESS1 (Nat : ?x) < Nat : ?y forsome @ [(forall @ [(?1 @ 1 + Nat : ?2) -> ?1 @ Nat : ?2]) & (?1 @ Nat : ?x) & ~?1 @ Nat : ?y] ALESS1 LESS1 MLESSBOOL LESSBOOL (Nat : ?x) < Nat : ?y bool : (Nat : ?x) < Nat : ?y ALESSBOOL AND BOOLDEF CASEINTRO EQUATION IF LESS1 NONTRIV NOT ODDCHOICE OR PLUSTYPE REFLEX TYPES forall forsome MLESSBOOL2 LESSBOOL2 (Nat : ?x) < Nat : ?y |-(Nat : ?x) < Nat : ?y ALESSBOOL2 AND ASSERT BOOLDEF CASEINTRO EQUATION IF LESS1 NONTRIV NOT ODDCHOICE OR PLUSTYPE REFLEX TYPES forall forsome MLESSCOMP LESSCOMP (Nat : ?x) < Nat : ?y ?x forsome @ [((Nat : ?1) + Nat : ?n) = Nat : ?m] ((Nat : ?n) < Nat : ?m) || true , true ALESS_ADD AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL MINUSCOMP NATMINUSCOMP NAT_SUB NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSMINUS PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_ADD1 LESS_ADD1 ((Nat : ?n) < Nat : ?m) -> forsome @ [(Nat : ?m) = (Nat : ?n) + ?1 + 1] true ALESS_ADD1 AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR PLUSCOMM PLUSCOMP PLUSMINUS PLUSTYPE REFLEX TYPES XOR forall forsome MLESS_ADD_NZ LESS_ADD_NZ ( ~(Nat : ?n) = 0) -> (Nat : ?m) < (Nat : ?m) + Nat : ?n true ALESS_ADD_NZ AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC SUCCNOTZERO TYPES XOR forall forsome MLESS_ADD_NZF LESS_ADD_NZF @ ?n , ?m true ( ~(Nat : ?n) = 0) -> (Nat : ?m) < (Nat : ?m) + Nat : ?n ALESS_ADD_NZF AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC SUCCNOTZERO TYPES XOR forall forsome MLESS_ADD_SUC LESS_ADD_SUC (Nat : ?m) < (Nat : ?m) + 1 + Nat : ?n true ALESS_ADD_SUC AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMP PLUSID PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_ADD_SUCF LESS_ADD_SUCF @ ?m , ?n true (Nat : ?m) < (Nat : ?m) + 1 + Nat : ?n ALESS_ADD_SUCF AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMP PLUSID PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_ANTISYM LESS_ANTISYM ~((Nat : ?m) < Nat : ?n) & (Nat : ?n) < Nat : ?m true ALESS_ANTISYM AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_ANTISYMF LESS_ANTISYMF @ ?m , ?n true ~((Nat : ?m) < Nat : ?n) & (Nat : ?n) < Nat : ?m ALESS_ANTISYMF AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_CASES LESS_CASES ((Nat : ?n) < Nat : ?m) | ((Nat : ?n) = Nat : ?m) | (Nat : ?m) < Nat : ?n true ALESS_CASES AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_CASESF LESS_CASESF @ ?n , ?m true ((Nat : ?n) < Nat : ?m) | ((Nat : ?n) = Nat : ?m) | (Nat : ?m) < Nat : ?n ALESS_CASESF AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_CASES_IMP LESS_CASES_IMP ( ~((Nat : ?m) < Nat : ?n) | (Nat : ?m) = Nat : ?n) -> (Nat : ?n) < Nat : ?m true ALESS_CASES_IMP AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_EQ LESS_EQ (1 + Nat : ?m) =< Nat : ?n (Nat : ?m) < Nat : ?n ALESS_EQ AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_EQ_ADD LESS_EQ_ADD ((Nat : ?m) =< Nat : ?n) -> forsome @ [(Nat : ?n) = (Nat : ?m) + ?1] |-((Nat : ?m) < Nat : ?n) -> forsome @ [(?1 + Nat : ?m) = Nat : ?n] ALESS_EQ_ADD AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL MINUSCOMP NATMINUSCOMP NAT_SUB NONTRIV NOT ODDCHOICE OR PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_EQ_ANTISYM LESS_EQ_ANTISYM (((Nat : ?n) =< Nat : ?m) & (Nat : ?m) =< Nat : ?n) -> (Nat : ?n) = Nat : ?m true ALESS_EQ_ANTISYM AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_EQ_MONO LESS_EQ_MONO (1 + Nat : ?n) =< 1 + Nat : ?m (Nat : ?n) =< Nat : ?m ALESS_EQ_MONO AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_EQ_REAL LESS_EQ_REAL ?x =< ?y ((Real : ?x) = Real : ?y) | ?x < ?y ALESS_EQ_REAL LESS_EQ_REAL MLESS_EQ_SUC_LESS LESS_EQ_SUC_LESS ((1 + Nat : ?n) < Nat : ?m) | (1 + Nat : ?n) = Nat : ?m (Nat : ?n) < Nat : ?m ALESS_EQ_SUC_LESS AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_IMP_LEQ LESS_IMP_LEQ ((Nat : ?m) < Nat : ?n) -> (Nat : ?m) =< Nat : ?n true ALESS_IMP_LEQ AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE REFLEX TYPES XOR MLESS_LEMMA1 LESS_LEMMA1 ((Nat : ?x) < 1 + Nat : ?y) -> ((Nat : ?x) = Nat : ?y) | (Nat : ?x) < Nat : ?y true ALESS_LEMMA1 AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF LESS1 NONTRIV NOT ODDCHOICE OR PLUSTYPE PLUSTYPE2 REFLEX TYPES XOR forall forsome MLESS_LEMMA1F LESS_LEMMA1F @ ?x , ?y true ((Nat : ?x) < 1 + Nat : ?y) -> ((Nat : ?x) = Nat : ?y) | (Nat : ?x) < Nat : ?y ALESS_LEMMA1F AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF LESS1 NONTRIV NOT ODDCHOICE OR PLUSTYPE PLUSTYPE2 REFLEX TYPES XOR forall forsome MLESS_LEMMA2 LESS_LEMMA2 (((Nat : ?x) = Nat : ?y) | (Nat : ?x) < Nat : ?y) -> (Nat : ?x) < 1 + Nat : ?y true ALESS_LEMMA2 AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_LEMMA2F LESS_LEMMA2F @ ?x , ?y true (((Nat : ?x) = Nat : ?y) | (Nat : ?x) < Nat : ?y) -> (Nat : ?x) < 1 + Nat : ?y ALESS_LEMMA2F AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_LEQ_TRANS LESS_LEQ_TRANS (((Nat : ?m) < Nat : ?n) & (Nat : ?n) =< Nat : ?p) -> (Nat : ?m) < Nat : ?p true ALESS_LEQ_TRANS AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_LESS_CASES LESS_LESS_CASES ((Nat : ?m) = Nat : ?n) | ((Nat : ?m) < Nat : ?n) | (Nat : ?n) < Nat : ?m true ALESS_LESS_CASES AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_LESS_SUC LESS_LESS_SUC ~((Nat : ?m) < Nat : ?n) & (Nat : ?n) < 1 + Nat : ?m true ALESS_LESS_SUC AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_MONO LESS_MONO ((Nat : ?m) < Nat : ?n) -> (1 + Nat : ?m) < 1 + Nat : ?n true ALESS_MONO AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF LESS1 NONTRIV NOT ODDCHOICE OR PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_MONOF LESS_MONOF @ ?m , ?n true ((Nat : ?m) < Nat : ?n) -> (1 + Nat : ?m) < 1 + Nat : ?n ALESS_MONOF AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF LESS1 NONTRIV NOT ODDCHOICE OR PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_MONO_ADD LESS_MONO_ADD ((Nat : ?m) < Nat : ?n) -> ((Nat : ?m) + Nat : ?p) < (Nat : ?n) + Nat : ?p true ALESS_MONO_ADD AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_MONO_ADDF LESS_MONO_ADDF @ ?m , ?n , ?p true ((Nat : ?m) < Nat : ?n) -> ((Nat : ?m) + Nat : ?p) < (Nat : ?n) + Nat : ?p ALESS_MONO_ADDF AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_MONO_ADD_EQ LESS_MONO_ADD_EQ (Nat : ?m) < Nat : ?n ((Nat : ?m) + Nat : ?p) < (Nat : ?n) + Nat : ?p ALESS_MONO_ADD_EQ AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_MONO_ADD_INV LESS_MONO_ADD_INV (((Nat : ?m) + Nat : ?p) < (Nat : ?n) + Nat : ?p) -> (Nat : ?m) < Nat : ?n true ALESS_MONO_ADD_INV AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_MONO_ADD_INVF LESS_MONO_ADD_INVF @ ?m , ?n , ?p true (((Nat : ?m) + Nat : ?p) < (Nat : ?n) + Nat : ?p) -> (Nat : ?m) < Nat : ?n ALESS_MONO_ADD_INVF AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_MONO_EQ LESS_MONO_EQ (Nat : ?m) < Nat : ?n (1 + Nat : ?m) < 1 + Nat : ?n ALESS_MONO_EQ AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_MONO_MULT LESS_MONO_MULT ((Nat : ?m) =< Nat : ?n) -> ((Nat : ?m) * Nat : ?p) =< (Nat : ?n) * Nat : ?p true ALESS_MONO_MULT AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF DIST EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TIMESCOMM TIMESID TIMESTYPE TIMESTYPE2 TYPES XOR forall forsome MLESS_MONO_MULTF LESS_MONO_MULTF @ ?m , ?n , ?p true ((Nat : ?m) =< Nat : ?n) -> ((Nat : ?m) * Nat : ?p) =< (Nat : ?n) * Nat : ?p ALESS_MONO_MULTF AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF DIST EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TIMESCOMM TIMESID TIMESTYPE TIMESTYPE2 TYPES XOR forall forsome MLESS_MONO_REV LESS_MONO_REV ((1 + Nat : ?m) < 1 + Nat : ?n) -> (Nat : ?m) < Nat : ?n true ALESS_MONO_REV AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_MONO_REVF LESS_MONO_REVF @ ?m , ?n true ((1 + Nat : ?m) < 1 + Nat : ?n) -> (Nat : ?m) < Nat : ?n ALESS_MONO_REVF AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_MULT2 LESS_MULT2 ((0 < Nat : ?m) & 0 < Nat : ?n) -> 0 < (Nat : ?m) * Nat : ?n true ALESS_MULT2 AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF DIST EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMP PLUSID PLUSMINUS PLUSTYPE PLUSTYPE2 REALDIVTYPE REFLEX SAMESUCC TIMESASSOC TIMESCOMM TIMESDIV TIMESTYPE TIMESTYPE2 TYPES XOR forall forsome MLESS_NOT_EQ LESS_NOT_EQ ((Nat : ?x) < Nat : ?y) -> ~(Nat : ?x) = Nat : ?y true ALESS_NOT_EQ AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF LESS1 NONTRIV NOT ODDCHOICE OR PLUSTYPE REFLEX TYPES XOR forall forsome MLESS_NOT_EQF LESS_NOT_EQF @ ?x , ?y true ((Nat : ?x) < Nat : ?y) -> ~(Nat : ?x) = Nat : ?y ALESS_NOT_EQF AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF LESS1 NONTRIV NOT ODDCHOICE OR PLUSTYPE REFLEX TYPES XOR forall forsome MLESS_NOT_REFL LESS_NOT_REFL ~(Nat : ?x) < Nat : ?x true ALESS_NOT_REFL AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF LESS1 NONTRIV NOT ODDCHOICE OR PLUSTYPE REFLEX TYPES XOR forall forsome MLESS_NOT_SUC LESS_NOT_SUC (((Nat : ?m) < Nat : ?n) & ~(Nat : ?n) = 1 + Nat : ?m) -> (1 + Nat : ?m) < Nat : ?n true ALESS_NOT_SUC AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_OR LESS_OR ((Nat : ?m) < Nat : ?n) -> (1 + Nat : ?m) =< Nat : ?n true ALESS_OR AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_OR_ADD LESS_OR_ADD ((Nat : ?n) < Nat : ?m) | forsome @ [(Nat : ?n) = ?1 + Nat : ?m] |-((Nat : ?m) < Nat : ?n) -> forsome @ [(?1 + Nat : ?m) = Nat : ?n] ALESS_OR_ADD AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL MINUSCOMP NATMINUSCOMP NAT_SUB NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSID PLUSMINUS PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_OR_EQ LESS_OR_EQ (Nat : ?x) =< Nat : ?y ((Nat : ?x) < Nat : ?y) | (Nat : ?x) = Nat : ?y ALESS_OR_EQ AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE REFLEX TYPES XOR MLESS_SUC LESS_SUC ((Nat : ?x) < Nat : ?y) -> (Nat : ?x) < 1 + Nat : ?y true ALESS_SUC AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF LESS1 NONTRIV NOT ODDCHOICE OR PLUSTYPE PLUSTYPE2 REFLEX TYPES XOR forall forsome MLESS_SUCF LESS_SUCF @ ?x , ?y true ((Nat : ?x) < Nat : ?y) -> (Nat : ?x) < 1 + Nat : ?y ALESS_SUCF AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF LESS1 NONTRIV NOT ODDCHOICE OR PLUSTYPE PLUSTYPE2 REFLEX TYPES XOR forall forsome MLESS_SUC_EQ_COR LESS_SUC_EQ_COR (((Nat : ?m) < Nat : ?n) & ~(1 + Nat : ?m) = Nat : ?n) -> (1 + Nat : ?m) < Nat : ?n true ALESS_SUC_EQ_COR AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_SUC_IMP LESS_SUC_IMP ((Nat : ?m) < 1 + Nat : ?n) -> ( ~(Nat : ?m) = Nat : ?n) -> (Nat : ?m) < Nat : ?n true ALESS_SUC_IMP AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_SUC_IMPF LESS_SUC_IMPF @ ?m , ?n true ((Nat : ?m) < 1 + Nat : ?n) -> ( ~(Nat : ?m) = Nat : ?n) -> (Nat : ?m) < Nat : ?n ALESS_SUC_IMPF AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_SUC_NOT LESS_SUC_NOT ((Nat : ?m) < Nat : ?n) -> ~(Nat : ?n) < 1 + Nat : ?m true ALESS_SUC_NOT AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_SUC_REFL LESS_SUC_REFL (Nat : ?x) < 1 + Nat : ?x true ALESS_SUC_REFL AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_SUC_REFLF LESS_SUC_REFLF @ ?x true (Nat : ?x) < 1 + Nat : ?x ALESS_SUC_REFLF AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_SUC_SUC LESS_SUC_SUC (Nat : ?x) < 1 + 1 + Nat : ?x true ALESS_SUC_SUC AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_SUC_SUCF LESS_SUC_SUCF @ ?x true (Nat : ?x) < 1 + 1 + Nat : ?x ALESS_SUC_SUCF AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_THM LESS_THM (Nat : ?x) < 1 + Nat : ?y ((Nat : ?x) = Nat : ?y) | (Nat : ?x) < Nat : ?y ALESS_THM AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_TRANS LESS_TRANS (((Nat : ?m) < Nat : ?n) & (Nat : ?n) < Nat : ?p) -> (Nat : ?m) < Nat : ?p true ALESS_TRANS AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLESS_TRANSF LESS_TRANSF @ ?m , ?n , ?p true (((Nat : ?m) < Nat : ?n) & (Nat : ?n) < Nat : ?p) -> (Nat : ?m) < Nat : ?p ALESS_TRANSF AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MLISTBIND LISTBIND @ ?x , ?y ?t (PAIRBIND @ ?x , ?y) => (EVAL *> PAIRBIND @ ?y) => (EVAL *> LISTBIND @ ?y) => ?t ALISTBIND P1 P2 MLOOP_TAC LOOP_TAC @ ?ONE_STEP ?x (ALL_STEPS @ ?ONE_STEP) => STARTLOOP => ?x ALOOP_TAC IGNOREFIRST MLZ LZ (?e = ?f) & ?F @ ?e (?e = ?f) & ?F @ ?f ALZ AND BOOLDEF EQUATION ODDCHOICE MMAKE_CASE MAKE_CASE ?p ODDCHOICE <= EQUATION => BOOLDEF => (?p = bool : ?p) => ?p AMAKE_CASE BOOLDEF EQUATION ODDCHOICE MMINUSCOMP MINUSCOMP (Nat : ?x) - Nat : ?y (?x > (ASRTRIGHT @ ?p) =>> (ASRTLEFT @ ?p) =>> (ASSRTBOTH @ ?p) => ?r ^+ ?s AMKASRT MMODCOMP MODCOMP ?x % ?y ?x %! ?y AMODCOMP MODCOMP MMODSCIN MODSCIN ?x % ?y (Nat : ?x) % Nat : ?y AMODSCIN MODTYPE TYPES MMODTYPE MODTYPE ?x % ?y Nat : (Nat : ?x) % Nat : ?y AMODTYPE MODTYPE MMOP MOP (?p & ?p -> ?q) -> ?q true AMOP AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MMOPF MOPF @ ?p , ?q true (?p & ?p -> ?q) -> ?q AMOPF AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MMP_THM MP_THM ((?P @ ?x) & forall @ [(?P @ ?1) -> ?Q @ ?1]) -> ?Q @ ?x true AMP_THM AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR forall MMP_THMF MP_THMF @ ?P , ?Q , ?x true ((?P @ ?x) & forall @ [(?P @ ?1) -> ?Q @ ?1]) -> ?Q @ ?x AMP_THMF AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR forall MMULT_SUC MULT_SUC (Nat : ?x) * 1 + Nat : ?y (Nat : ?x) + (Nat : ?x) * Nat : ?y AMULT_SUC BUILTIN DIST PLUSCOMP PLUSTYPE TIMESCOMM TIMESID TYPES MMUTASSOC MUTASSOC (?p =/= ?q) == ?r ?p =/= ?q == ?r AMUTASSOC AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MMUTINT MUTINT ?p =/= ?q == ?r ?p == ?q =/= ?r AMUTINT AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MNATCALC NATCALC ?x NATCALCEXPAND <= (LEFT @ (RIGHT @ $BUILTIN) ** REFLEX ** RIGHT @ BUILTIN) => (?x = Nat : ?x) || (Nat : ?x) , ?x ANATCALC BUILTIN CASEINTRO REFLEX MNATCALCEXPAND NATCALCEXPAND ?x (?x = Nat : ?x) || (Nat : ?x) , ?x ANATCALCEXPAND CASEINTRO MNATMINUSCOMP NATMINUSCOMP (Nat : ?x) .-. Nat : ?y ?x -! ?y ANATMINUSCOMP NATMINUSCOMP MNATMINUSSCIN NATMINUSSCIN ?x .-. ?y (Nat : ?x) .-. Nat : ?y ANATMINUSSCIN NAT_SUB TYPES MNATMINUSTYPE NATMINUSTYPE ?x .-. ?y Nat : (Nat : ?x) .-. Nat : ?y ANATMINUSTYPE BUILTIN CASEINTRO NAT_SUB TYPES MNAT_SUB NAT_SUB ?x .-. ?y ((Nat : ?x) < Nat : ?y) || 0 , Nat : (Nat : ?x) - Nat : ?y ANAT_SUB NAT_SUB MNAT__SUB NAT__SUB ?x .-. ?y ((Nat : ?x) < Nat : ?y) || 0 , (Nat : ?x) - Nat : ?y ANAT__SUB LESSCOMP MINUSCOMP NATMINUSCOMP NAT_SUB TYPES MNEGF NEGF ~false true ANEGF AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MNEQ NEQ ?p == ?q ( ~?p) == ~?q ANEQ AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MNEWTAUT NEWTAUT ?x ALT_PUSH => (TOPDOWN @ ALL_EXP) => MAKE_CASE => ?x ANEWTAUT AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX XOR MNONTRIV NONTRIV true = false false ANONTRIV NONTRIV MNONTRIV2a NONTRIV2a false = true false ANONTRIV2a CASEINTRO EQUATION MNOT NOT ?x ~ ?y (true = ?y) || false , true ANOT NOT MNOT1 NOT1 ~?y (true = ?y) || false , true ANOT1 NOT MNOTBOOL NOTBOOL ?x ~ ?y bool : ?x ~ ?y ANOTBOOL BOOLDEF CASEINTRO EQUATION NONTRIV NOT ODDCHOICE REFLEX MNOTBOOLDROP NOTBOOLDROP ~bool : ?x ~?x ANOTBOOLDROP BOOLDEF CASEINTRO EQUATION NONTRIV NOT ODDCHOICE REFLEX MNOTBOTHPOS NOTBOTHPOS (Positive @ ?x) & Positive @ -?x false ANOTBOTHPOS AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF MINUSTYPE NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE POSPLUS POSTYPE REFLEX TRICHOTOMY TYPES XOR MNOTCLEAN NOTCLEAN ?x ~ ?y ~?y ANOTCLEAN NOT MNOTFORALL NOTFORALL ~forall @ [?P @ ?1] (forall @ [ ~?P @ ?1]) | ~forall @ [?P @ ?1] ANOTFORALL AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR forall MNOT_ADD_LESS NOT_ADD_LESS forall @ [ ~((Nat : ?x) + Nat : ?1) < Nat : ?1] true ANOT_ADD_LESS AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MNOT_ADD_LESSF NOT_ADD_LESSF @ ?x true forall @ [ ~((Nat : ?x) + Nat : ?1) < Nat : ?1] ANOT_ADD_LESSF AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MNOT_EQ NOT_EQ ?x ~= ?y ~?x = ?y ANOT_EQ NOT_EQ MNOT_EXP NOT_EXP ( ~?p) || ?a , ?b ?p || ?b , ?a ANOT_EXP CASEINTRO NOT ODDCHOICE MNOT_GREATER NOT_GREATER ~(Nat : ?m) > Nat : ?n (Nat : ?m) =< Nat : ?n ANOT_GREATER AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION GREATER IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MNOT_GREATER_EQ NOT_GREATER_EQ ~(Nat : ?m) >= Nat : ?n (1 + Nat : ?m) =< Nat : ?n ANOT_GREATER_EQ AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION GREATER GREATER_EQ_REAL IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MNOT_LEQ NOT_LEQ ~(Nat : ?m) =< Nat : ?n (Nat : ?n) < Nat : ?m ANOT_LEQ AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MNOT_LEQ_SUC NOT_LEQ_SUC ~(Nat : ?m) =< Nat : ?n (1 + Nat : ?n) =< Nat : ?m ANOT_LEQ_SUC AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MNOT_LESS NOT_LESS ~(Nat : ?m) < Nat : ?n (Nat : ?n) =< Nat : ?m ANOT_LESS AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MNOT_LESS_0 NOT_LESS_0 ~(Nat : ?x) < 0 true ANOT_LESS_0 AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSTYPE PLUSTYPE2 REFLEX TYPES XOR forall forsome MNOT_LESS_0F NOT_LESS_0F @ ?x true ~(Nat : ?x) < 0 ANOT_LESS_0F AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSTYPE PLUSTYPE2 REFLEX TYPES XOR forall forsome MNOT_NUM_EQ NOT_NUM_EQ ((1 + Nat : ?m) =< Nat : ?n) | (1 + Nat : ?n) =< Nat : ?m ~(Nat : ?m) = Nat : ?n ANOT_NUM_EQ AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MNOT_SUC_ADD_LEQ NOT_SUC_ADD_LEQ ~(1 + (Nat : ?m) + Nat : ?n) =< Nat : ?m (Nat : ?m) =< (Nat : ?m) + Nat : ?n ANOT_SUC_ADD_LEQ AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MNOT_SUC_LEQ NOT_SUC_LEQ ~(1 + Nat : ?n) =< Nat : ?m (Nat : ?m) =< Nat : ?n ANOT_SUC_LEQ AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MNOT_SUC_LEQ_0 NOT_SUC_LEQ_0 ~(1 + Nat : ?n) =< 0 true ANOT_SUC_LEQ_0 AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MNOT_SUC_LESS NOT_SUC_LESS ~(1 + Nat : ?m) < Nat : ?m true ANOT_SUC_LESS AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MNRULE1 NRULE1 |- ~?p ~?p ANRULE1 ASSERT BOOLDEF CASEINTRO EQUATION NONTRIV NOT ODDCHOICE REFLEX TYPES MNRULE2 NRULE2 ~ |-?p ~?p ANRULE2 ASSERT BOOLDEF CASEINTRO EQUATION NONTRIV NOT ODDCHOICE REFLEX TYPES MNTYPE NTYPE ~?p |- ~ |-?p ANTYPE ASSERT BOOLDEF CASEINTRO EQUATION NONTRIV NOT ODDCHOICE REFLEX MODDCHOICE ODDCHOICE ?x || ?y , ?z (true = ?x) || ?y , ?z AODDCHOICE ODDCHOICE MONENAT ONENAT 1 Nat : 1 AONENAT BUILTIN MONEPOINT ONEPOINT forallr @ [?1 = ?e] , [?P @ ?1] |-EVAL => ?P @ ?e AONEPOINT AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forall forallr MOR OR ?x | ?y ~( ~?x) & ~?y AOR OR MORBOOL ORBOOL ?x | ?y bool : ?x | ?y AORBOOL BOOLDEF CASEINTRO EQUATION NONTRIV NOT ODDCHOICE OR REFLEX MORSCIN ORSCIN (bool : ?x) | bool : ?y ?x | ?y AORSCIN BOOLDEF CASEINTRO EQUATION NONTRIV NOT ODDCHOICE OR REFLEX MOR_EXP OR_EXP (?p | ?q) || ?a , ?b ?p || ?a , ?q || ?a , ?b AOR_EXP AND CASEINTRO NOT ODDCHOICE OR MOR_LESS OR_LESS ((1 + Nat : ?m) =< Nat : ?n) -> (Nat : ?m) < Nat : ?n true AOR_LESS AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MP1 P1 P1 @ ?x , ?y ?x AP1 P1 MP2 P2 P2 @ ?x , ?y ?y AP2 P2 MPAIRBIND PAIRBIND @ ?x , ?y ?t (BIND @ ?x , ?y) => EVAL => (LEFT @ VALUE @ [EVAL]) => (LEFT @ VALUE @ [LEFT @ VALUE @ [EVAL]]) => (LEFT @ VALUE @ [LEFT @ VALUE @ [RIGHT @ PI2F @ ?x]]) => (LEFT @ VALUE @ [LEFT @ VALUE @ [BIND @ ?y]]) => (LEFT @ VALUE @ [RIGHT @ PI1F @ ?y]) => (LEFT @ VALUE @ [BIND @ ?x]) => (BIND @ ?x , ?y) => ?t APAIRBIND P1 P2 MPCASEINTRO PCASEINTRO @ ?p ?x ?p || ?x , ?x APCASEINTRO CASEINTRO MPI1 PI1 P1 @ ?x , ?y ?x API1 P1 MPI1F PI1F @ ?y ?x P1 @ ?x , ?y API1F P1 MPI2 PI2 P2 @ ?x , ?y ?y API2 P2 MPI2F PI2F @ ?y ?x P2 @ ?y , ?x API2F P2 MPIVOT PIVOT (?a = ?b) || ?T , ?U (LEFT_CASE @ EVAL) => HYP => (?a = ?b) || ((BIND @ ?a) => ?T) , ?U APIVOT MPLUSASSOC PLUSASSOC (?x + ?y) + ?z ?x + ?y + ?z APLUSASSOC PLUSASSOC MPLUSCOMM PLUSCOMM ?x + ?y ?y + ?x APLUSCOMM PLUSCOMM MPLUSCOMP PLUSCOMP (Nat : ?x) + Nat : ?y ?x +! ?y APLUSCOMP PLUSCOMP MPLUSID PLUSID 0 + ?x Real : ?x APLUSID PLUSID MPLUSINVDIST PLUSINVDIST -?x + ?y ( -?x) + -?y APLUSINVDIST BUILTIN CASEINTRO MINUSTYPE PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE REFLEX TYPES MPLUSINVDISTS PLUSINVDISTS -?x + ?y (PLUSINVDISTS => -?x) + PLUSINVDISTS => -?y APLUSINVDISTS BUILTIN CASEINTRO MINUSTYPE PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE REFLEX TYPES MPLUSMINUS PLUSMINUS (?x - ?y) + ?y Real : ?x APLUSMINUS PLUSMINUS MPLUSSCIN PLUSSCIN ?x + ?y (Real : ?x) + Real : ?y APLUSSCIN PLUSTYPE TYPES MPLUSTYPE PLUSTYPE ?x + ?y Real : (Real : ?x) + Real : ?y APLUSTYPE PLUSTYPE MPLUSTYPE2 PLUSTYPE2 (Nat : ?x) + Nat : ?y Nat : (Nat : ?x) + Nat : ?y APLUSTYPE2 PLUSTYPE2 MPOINTTYPE POINTTYPE [?x] : ?y ?x APOINTTYPE POINTTYPE MPOSASSERT POSASSERT Positive @ ?x |-Positive @ ?x APOSASSERT ASSERT POSTYPE TYPES MPOSPLUS POSPLUS (Positive @ ?x) & Positive @ ?y (Positive @ ?x + ?y) & (Positive @ ?x) & Positive @ ?y APOSPLUS POSPLUS MPOSTIMES POSTIMES (Positive @ ?x) & Positive @ ?y (Positive @ ?x * ?y) & (Positive @ ?x) & Positive @ ?y APOSTIMES POSTIMES MPOSTYPE POSTYPE Positive @ ?x bool : Positive @ Real : ?x APOSTYPE POSTYPE MPOS_ONE POS_ONE Positive @ 1 true APOS_ONE AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF DIST EQUATION EVALEQ IF IFF MINUSTYPE NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE POSTIMES POSTYPE REFLEX TIMESCOMM TIMESID TIMESTYPE TRICHOTOMY TYPES XOR MPOS_SIGN POS_SIGN (0 ~= Real : ?x) & Positive @ -?x (0 ~= Real : ?x) & ~Positive @ ?x APOS_SIGN AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF MINUSTYPE NONTRIV NOT NOT_EQ ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE POSPLUS POSTYPE REFLEX TRICHOTOMY TYPES XOR MPOS_ZERO POS_ZERO Positive @ 0 false APOS_ZERO AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF MINUSTYPE NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE POSTYPE REFLEX TRICHOTOMY TYPES XOR MPRE9pt12 PRE9pt12 (forall @ [(?P @ ?1) -> ?Q @ ?1]) -> (forall @ [?P @ ?1]) -> forall @ [?Q @ ?1] true APRE9pt12 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR forall MPREDSCIN PREDSCIN Pred @ ?x Pred @ Nat : ?x APREDSCIN BUILTIN NAT_SUB Pred TYPES MPREDTYPE PREDTYPE Pred @ ?x Nat : Pred @ Nat : ?x APREDTYPE BUILTIN CASEINTRO NAT_SUB Pred TYPES MPRODTYPE PRODTYPE (?t1 <*> ?t2) : ?x (?t1 : P1 @ ?x) , ?t2 : P2 @ ?x APRODTYPE PRODTYPE MPROVETAUT PROVETAUT @ ?y bool : ?x (NEWTAUT => IFF <= (bool : ?x) = bool : ?y) || (bool : ?y) , bool : ?x APROVETAUT AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX XOR MPROVETAUT2 PROVETAUT2 @ ?y ?x CNRULE1 =>> IRULE1 =>> XRULE1 =>> NRULE1 =>> DRULE1 =>> CRULE1 =>> BRULE1 => ASSERT2 => (PROVETAUT @ ?y) => ASSERT => CNRULE1 <<= IRULE1 <<= XRULE1 <<= NRULE1 <<= DRULE1 <<= CRULE1 <<= BRULE1 <= ?x APROVETAUT2 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MPred Pred Pred @ ?x ?x .-. 1 APred Pred MR R @ ?thm ?p ^+ ?q ?p ^+ ?thm => ?q AR MRAISE0 RAISE0 (?f @ ?x) ^& ?g @ ?x (?f :^& ?g) @ ?x ARAISE0 MREALDIVCOMP REALDIVCOMP (Nat : ?x) ./. Nat : ?y (?x /! ?y) + (?x %! ?y) ./. ?y AREALDIVCOMP REALDIVCOMP MREALDIVSCIN REALDIVSCIN ?x ./. ?y (Real : ?x) ./. Real : ?y AREALDIVSCIN REALDIVTYPE TYPES MREALDIVTYPE REALDIVTYPE ?x ./. ?y Real : (Real : ?x) ./. Real : ?y AREALDIVTYPE REALDIVTYPE MREALNAT REALNAT Nat : ?x Real : Nat : ?x AREALNAT BUILTIN PLUSCOMP PLUSTYPE TYPES MREALNUMERAL REALNUMERAL ?n (RIGHT @ $BUILTIN) => REALNAT => TYPENUMERAL => ?n AREALNUMERAL BUILTIN CASEINTRO PLUSCOMP PLUSTYPE REFLEX TYPES MREALNUMERAL2 REALNUMERAL2 Real : ?n BUILTIN <= REALNAT <= (RIGHT @ TYPENUMERAL) => Real : ?n AREALNUMERAL2 BUILTIN CASEINTRO PLUSCOMP PLUSTYPE REFLEX TYPES MREALSUBNATTYPE REALSUBNATTYPE Nat : (Nat : ?m) - Nat : ?n ((Nat : ?m) < Nat : ?n) || (Nat : -(Nat : ?n) - Nat : ?m) , (Nat : ?m) - Nat : ?n AREALSUBNATTYPE AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL MINUSCOMP NATMINUSCOMP NAT_SUB NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MREALZERO REALZERO 0 Real : 0 AREALZERO BUILTIN CASEINTRO PLUSCOMP PLUSTYPE REFLEX TYPES MREAL_LESS_CANCEL REAL_LESS_CANCEL (?z + ?x) < ?z + ?y ?x < ?y AREAL_LESS_CANCEL BUILTIN CASEINTRO MINUSTYPE PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE REAL_LESS_DEF REFLEX TYPES MREAL_LESS_DEF REAL_LESS_DEF ?x < ?y Positive @ ?y - ?x AREAL_LESS_DEF REAL_LESS_DEF MREAL_LESS_TRANS REAL_LESS_TRANS (?x < ?y) & ?y < ?z (?x < ?z) & (?x < ?y) & ?y < ?z AREAL_LESS_TRANS BUILTIN CASEINTRO MINUSTYPE PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE POSPLUS REAL_LESS_DEF REFLEX TYPES MREAL_NOT_LESS REAL_NOT_LESS ~?x < ?y ?y =< ?x AREAL_NOT_LESS AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF LESS_EQ_REAL MINUSTYPE NONTRIV NOT NOT_EQ ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE POSPLUS POSTYPE REAL_LESS_DEF REFLEX TRICHOTOMY TYPES XOR MREAL_TYPE REAL_TYPE ?x (EVERYWHERE @ TYPES) => (EVERYWHERE @ REAL_TYPE_1) => ?x AREAL_TYPE BUILTIN CASEINTRO MINUSTYPE PLUSCOMP PLUSTYPE REFLEX TYPES MREAL_TYPE_1 REAL_TYPE_1 ?x REALNUMERAL =>> ((RIGHT @ LEFT @ TYPES ** $REALZERO) *> MINUSTYPE) =>> PLUSTYPE => ?x AREAL_TYPE_1 BUILTIN CASEINTRO MINUSTYPE PLUSCOMP PLUSTYPE REFLEX TYPES MREAL_UNTYPE REAL_UNTYPE ?x (EVERYWHERE @ REAL_UNTYPE_1) => ?x AREAL_UNTYPE MINUSTYPE PLUSTYPE TYPES MREAL_UNTYPE_1 REAL_UNTYPE_1 ?x TYPES => (TREMBOTH @ PLUSTYPE) => (TREMBOTH @ MINUSTYPE) => (TREMTOP @ MINUSTYPE) => (TREMTOP @ PLUSTYPE) => ?x AREAL_UNTYPE_1 MINUSTYPE PLUSTYPE TYPES MREDUCE REDUCE ?f @ ?x (ABSTRACT4 @ ?x) <<= ((RL @ REDUCE) *> RAISE0) <<= ((RIGHT @ REDUCE) *> COMP) =>> ID => ?f @ ?x AREDUCE COMP Id MREFLEX REFLEX ?a = ?a true AREFLEX REFLEX MREMA REMA |- ~?p ~ |-?p AREMA ASSERT BOOLDEF CASEINTRO EQUATION NONTRIV NOT ODDCHOICE REFLEX TYPES MREMFLIP REMFLIP ?x AF =>> AT =>> XRULE1 =>> NRULE1 =>> DRULE1 =>> CRULE1 =>> BRULE1 => TWOASSERTS => DUBNEG2 => SREMFLIP => ?x AREMFLIP AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MREPL REPL (?p == ?q) & ?r == ?p (?p == ?q) & ?r == ?q AREPL AND ASSERT BOOLDEF EQUATION IFF ODDCHOICE TYPES MREVPIVOT REVPIVOT (?a = ?b) || ?T , ?U (LEFT_CASE @ EVAL) => HYP <= (?a = ?b) || ((BIND @ ?b) => ?T) , ?U AREVPIVOT MRIGHT RIGHT @ ?thm ?p ^+ ?q ?p ^+ ?thm => ?q ARIGHT MRIGHT_CASE RIGHT_CASE @ ?thm ?x || ?y , ?z ?x || ?y , ?thm => ?z ARIGHT_CASE MRL RL @ ?thm ?p ^+ ?q (?thm => ?p) ^+ ?thm => ?q ARL MRSFN RSFN ?f :^+ ?g [(?f :^+ ?g) @ ?1] ARSFN RSFN MSAMESUCC SAMESUCC (Nat : ?x) = Nat : ?y (1 + Nat : ?x) = 1 + Nat : ?y ASAMESUCC SAMESUCC MSFLIPALL SFLIPALL ?x NEGF =>> FDEF <<= FLIPPASTC =>> FLIPPASTD =>> FLIPPASTX =>> FLIPPASTB =>> FLIPPASTN =>> FLIPPASTA => ?x ASFLIPALL AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MSIGNPULL SIGNPULL ?x * -?y -?x * ?y ASIGNPULL BUILTIN CASEINTRO DIST MINUSTYPE PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE REFLEX TIMESCOMM TIMESTYPE TYPES MSQUARE_POS SQUARE_POS (0 = Real : ?x) | Positive @ ?x * ?x true ASQUARE_POS AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF DIST EQUATION IF IFF MINUSTYPE NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE POSTIMES POSTYPE REFLEX TIMESCOMM TIMESTYPE TRICHOTOMY TYPES XOR MSREMFLIP SREMFLIP ?x REMA =>> DEMb =>> DEMa =>> XORFLIP <<= BFLIP <<= NEGF <<= FDEF => NOTCLEAN => ASSERTCLEAN => (LEFT @ SREMFLIP) => (RIGHT @ SREMFLIP) => ?x ASREMFLIP AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MSTARTLOOP STARTLOOP ?x ?x . ?x ASTARTLOOP IGNOREFIRST MSTL STL ?x ^+ |-?y ((?p ^+ |-?q) = ?p ^+ ?q) => ?x ^+ |-?y ASTL MSTOPLOOP STOPLOOP ?x . ?x ?x ASTOPLOOP IGNOREFIRST MSTR STR ( |-?x) ^+ ?y ((( |-?p) ^+ ?q) = ?p ^+ ?q) => ( |-?x) ^+ ?y ASTR MSTRONG_EVERYWHERE_CASE STRONG_EVERYWHERE_CASE @ ?EVERYWHERE , ?thm ?a || ?x , ?y ?thm => ((?EVERYWHERE @ ?thm) => ?a) || ((?EVERYWHERE @ ?thm) => ?x) , (?EVERYWHERE @ ?thm) => ?y ASTRONG_EVERYWHERE_CASE MSTT STT |-?x ^+ ?y (( |-?p ^+ ?q) = ?p ^+ ?q) => |-?x ^+ ?y ASTT MSUBTRACT_DIFF SUBTRACT_DIFF ?x - ?y - ?z ?x + ( -?y) + ?z ASUBTRACT_DIFF BUILTIN CASEINTRO MINUSTYPE PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE REFLEX TYPES MSUBTRACT_SUM SUBTRACT_SUM ?x - ?y + ?z (?x - ?y) - ?z ASUBTRACT_SUM BUILTIN CASEINTRO MINUSTYPE PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE REFLEX TYPES MSUBTYPE SUBTYPE (?t |/ ?P) : ?x (?P @ ?t : ?x) || (?t : ?x) , ?t : !!![?P @ ?t : ?1] ASUBTYPE SUBTYPE MSUB_REFL SUB_REFL ?x - ?x 0 ASUB_REFL BUILTIN CASEINTRO MINUSTYPE PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE REFLEX TYPES MSUCCNOTZERO SUCCNOTZERO 0 = 1 + Nat : ?x false ASUCCNOTZERO SUCCNOTZERO MSUC_EQ_LESS SUC_EQ_LESS ((1 + Nat : ?x) = Nat : ?y) -> (Nat : ?x) < Nat : ?y true ASUC_EQ_LESS AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MSUC_EQ_LESSF SUC_EQ_LESSF @ ?x , ?y true ((1 + Nat : ?x) = Nat : ?y) -> (Nat : ?x) < Nat : ?y ASUC_EQ_LESSF AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome MSUC_ID SUC_ID (1 + Nat : ?x) = Nat : ?x false ASUC_ID BUILTIN CASEINTRO EQUATION MINUSTYPE PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE REFLEX SUCCNOTZERO TYPES MSUC_IDF SUC_IDF @ ?x false (1 + Nat : ?x) = Nat : ?x ASUC_IDF BUILTIN CASEINTRO EQUATION MINUSTYPE PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE REFLEX SUCCNOTZERO TYPES MSUC_LESS SUC_LESS ((1 + Nat : ?x) < Nat : ?y) -> (Nat : ?x) < Nat : ?y true ASUC_LESS AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF LESS1 NONTRIV NOT ODDCHOICE OR PLUSTYPE PLUSTYPE2 REFLEX TYPES XOR forall forsome MSUC_LESSF SUC_LESSF @ ?x , ?y true ((1 + Nat : ?x) < Nat : ?y) -> (Nat : ?x) < Nat : ?y ASUC_LESSF AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF LESS1 NONTRIV NOT ODDCHOICE OR PLUSTYPE PLUSTYPE2 REFLEX TYPES XOR forall forsome MTAB_ALL TAB_ALL @ ?x forall @ [?P @ ?1] (forall @ [?P @ ?1]) || ((EVAL => ?P @ ?x) || true , false) , false ATAB_ALL CASEINTRO EQUATION forall MTAB_ALL_2 TAB_ALL_2 @ ?x (forall @ [?P @ ?1]) || ?a , ?b (forall @ [?P @ ?1]) || ((EVAL => ?P @ ?x) || ?a , ?b) , ?b ATAB_ALL_2 CASEINTRO EQUATION forall MTAB_ALL_NEW_1 TAB_ALL_NEW_1 (forall @ [?P @ ?1]) || ?a , ?b (forall @ [?P @ ?1]) || ?a , ([?b] = [(EVAL => ?P @ ?1) || ?b , ?b]) || ?b , true ATAB_ALL_NEW_1 BOOLDEF CASEINTRO EQUATION NONTRIV NOT ODDCHOICE REFLEX forall forsome MTAB_ALL_NEW_2 TAB_ALL_NEW_2 (forall @ [?P @ ?1]) || ?a , ([?b] = [(?P @ ?1) || ?b , true]) || ?b , true (forall @ [?P @ ?1]) || ?a , true ATAB_ALL_NEW_2 BOOLDEF CASEINTRO EQUATION NONTRIV NOT ODDCHOICE REFLEX forall forsome MTAB_AND TAB_AND ?p & ?q ?p || (?q || true , false) , false ATAB_AND AND EQUATION ODDCHOICE MTAB_AND_2 TAB_AND_2 (?p & ?q) || ?a , ?b ?p || (?q || ?a , ?b) , ?b ATAB_AND_2 AND CASEINTRO EQUATION ODDCHOICE MTAB_CEX TAB_CEX (forall @ [?P @ ?1]) || ?a , ?b (forall @ [?P @ ?1]) || ?a , ODDCHOICE <= (BOOLDEF => CEX_TAC => forall @ [?P @ ?1]) || ?a , ?b ATAB_CEX BOOLDEF CASEINTRO CHOICE COUNTER1 EQUATION NONTRIV NOT ODDCHOICE REFLEX forall forsome MTAB_IF TAB_IF ?p -> ?q ?p || (?q || true , false) , true ATAB_IF AND CASEINTRO EQUATION IF NONTRIV NOT ODDCHOICE OR REFLEX MTAB_IFF TAB_IFF ?x == ?y ?x || (?y || true , false) , ?y || false , true ATAB_IFF AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX XOR MTAB_IFF_2 TAB_IFF_2 (?x == ?y) || ?a , ?b ?x || (?y || ?a , ?b) , ?y || ?b , ?a ATAB_IFF_2 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX XOR MTAB_IF_2 TAB_IF_2 (?p -> ?q) || ?a , ?b ?p || (?q || ?a , ?b) , ?a ATAB_IF_2 AND CASEINTRO EQUATION IF NONTRIV NOT ODDCHOICE OR REFLEX MTAB_NOT TAB_NOT ~?p ?p || false , true ATAB_NOT NOT ODDCHOICE MTAB_NOT_2 TAB_NOT_2 ( ~?p) || ?a , ?b ?p || ?b , ?a ATAB_NOT_2 CASEINTRO NOT ODDCHOICE MTAB_OR TAB_OR ?p | ?q ?p || true , ?q || true , false ATAB_OR AND CASEINTRO EQUATION NONTRIV NOT ODDCHOICE OR REFLEX MTAB_OR_2 TAB_OR_2 (?p | ?q) || ?a , ?b ?p || ?a , ?q || ?a , ?b ATAB_OR_2 AND CASEINTRO EQUATION NONTRIV NOT ODDCHOICE OR REFLEX MTAB_SOME TAB_SOME @ ?x forsome @ [?P @ ?1] (forsome @ [?P @ ?1]) || true , (EVAL => ?P @ ?x) || true , false ATAB_SOME BOOLDEF CASEINTRO EQUATION NONTRIV NOT ODDCHOICE REFLEX forall forsome MTAB_SOME_2 TAB_SOME_2 @ ?x (forsome @ [?P @ ?1]) || ?a , ?b (forsome @ [?P @ ?1]) || ?a , (EVAL => ?P @ ?x) || ?a , ?b ATAB_SOME_2 BOOLDEF CASEINTRO EQUATION NONTRIV NOT ODDCHOICE REFLEX forall forsome MTAB_SOME_NEW_1 TAB_SOME_NEW_1 (forsome @ [?P @ ?1]) || ?a , ?b (forsome @ [?P @ ?1]) || (([?a] = [(EVAL => ?P @ ?1) || ?a , ?a]) || ?a , true) , ?b ATAB_SOME_NEW_1 CASEINTRO REFLEX MTAB_SOME_NEW_2 TAB_SOME_NEW_2 (forsome @ [?P @ ?1]) || (([?a] = [(?P @ ?1) || true , ?a]) || ?a , true) , ?b (forsome @ [?P @ ?1]) || true , ?b ATAB_SOME_NEW_2 BOOLDEF CASEINTRO EQUATION NONTRIV NOT ODDCHOICE REFLEX forall forsome MTAB_WITNESS TAB_WITNESS (forsome @ [?P @ ?1]) || ?a , ?b (forsome @ [?P @ ?1]) || ((CHOICE_TAC => forsome @ [?P @ ?1]) || ?a , ?b) , ?b ATAB_WITNESS CHOICE MTAB_XOR TAB_XOR ?x =/= ?y ?x || (?y || false , true) , ?y || true , false ATAB_XOR AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MTAB_XOR_2 TAB_XOR_2 (?x =/= ?y) || ?a , ?b ?x || (?y || ?b , ?a) , ?y || ?a , ?b ATAB_XOR_2 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MTADDBOTH TADDBOTH @ ?thm ?x ?thm <= (((RIGHT @ (RIGHT @ $TYPES) ** LEFT @ $TYPES) ** $?thm) *> ?thm) => ?x ATADDBOTH TYPES MTADDLEFT TADDLEFT @ ?thm ?x ?thm <= (((RIGHT @ LEFT @ $TYPES) ** $?thm) *> ?thm) => ?x ATADDLEFT TYPES MTADDRIGHT TADDRIGHT @ ?thm ?x ?thm <= (((RIGHT @ RIGHT @ $TYPES) ** $?thm) *> ?thm) => ?x ATADDRIGHT TYPES MTADDTOP TADDTOP @ ?thm ?x ((( $TYPES) ** RIGHT @ $?thm) *> ?thm) => ?x ATADDTOP TYPES MTEMP_PIVOT TEMP_PIVOT ?a || ?b , ?c ?a || ((0 |-| 1) <= ?b) , ?c ATEMP_PIVOT MTESTSIMP TESTSIMP ?a || ?b , ?c (EVERYWHERE @ $XOR) => (EVERYWHERE @ $IDEF2) => (EVERYWHERE @ CASEPREP ** CONDSIMP) => ?a || ?b , ?c ATESTSIMP AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MTHMAP THMAP @ ?dir , ?astrm , ?thm ?x ^+ ?y (?dir @ EVAL) => ?thm => (?dir @ (MKASRT @ ?astrm) ** BIND @ |-?astrm) => ?x ^+ ?y ATHMAP MTIMESASSOC TIMESASSOC (?x * ?y) * ?z ?x * ?y * ?z ATIMESASSOC TIMESASSOC MTIMESCOMM TIMESCOMM ?x * ?y ?y * ?x ATIMESCOMM TIMESCOMM MTIMESCOMP TIMESCOMP (Nat : ?x) * Nat : ?y ?x *! ?y ATIMESCOMP TIMESCOMP MTIMESDIV TIMESDIV (?x ./. ?y) * ?y (0 = Real : ?y) || 0 , Real : ?x ATIMESDIV TIMESDIV MTIMESID TIMESID 1 * ?x Real : ?x ATIMESID TIMESID MTIMESINTDIV TIMESINTDIV (?x % ?y) + (?x / ?y) * ?y Real : ?x ATIMESINTDIV TIMESINTDIV MTIMESSCIN TIMESSCIN ?x * ?y (Real : ?x) * Real : ?y ATIMESSCIN TIMESTYPE TYPES MTIMESTYPE TIMESTYPE ?x * ?y Real : (Real : ?x) * Real : ?y ATIMESTYPE TIMESTYPE MTIMESTYPE2 TIMESTYPE2 (Nat : ?x) * Nat : ?y Nat : (Nat : ?x) * Nat : ?y ATIMESTYPE2 TIMESTYPE2 MTIMESZERO TIMESZERO 0 * ?x 0 ATIMESZERO BUILTIN CASEINTRO DIST PLUSASSOC PLUSCOMP PLUSID PLUSMINUS PLUSTYPE REFLEX TIMESCOMM TIMESTYPE TYPES MTOPDOWN TOPDOWN @ ?thm ?x ?thm =>> (TOPDOWN_INFIX @ ?thm) =>> (TOPDOWN_CASE @ ?thm) => ?x ATOPDOWN MTOPDOWN_CASE TOPDOWN_CASE @ ?thm ?a || ?x , ?y (RIGHT @ RL @ TOPDOWN @ ?thm) => ?thm => ?a || ?x , ?y ATOPDOWN_CASE MTOPDOWN_INFIX TOPDOWN_INFIX @ ?thm ?x ^+ ?y (RL @ TOPDOWN @ ?thm) => ?thm => ?x ^+ ?y ATOPDOWN_INFIX MTREMBOTH TREMBOTH @ ?thm ?x ^+ ?y (((RIGHT @ (RIGHT @ TYPES) ** LEFT @ TYPES) ** $?thm) *> ?thm) => ?x ^+ ?y ATREMBOTH TYPES MTREMLEFT TREMLEFT @ ?thm ?x ^+ ?y (((RIGHT @ LEFT @ TYPES) ** $?thm) *> ?thm) => ?x ^+ ?y ATREMLEFT TYPES MTREMRIGHT TREMRIGHT @ ?thm ?x ^+ ?y (((RIGHT @ RIGHT @ TYPES) ** $?thm) *> ?thm) => ?x ^+ ?y ATREMRIGHT TYPES MTREMTOP TREMTOP @ ?thm ?t : ?x ?thm <= TYPES => (RIGHT @ ?thm) => ?t : ?x ATREMTOP TYPES MTRICHOTOMY TRICHOTOMY (Positive @ ?x) | Positive @ -?x ~0 = Real : ?x ATRICHOTOMY TRICHOTOMY MTRUEBOOL TRUEBOOL true bool : true ATRUEBOOL BOOLDEF EQUATION ODDCHOICE REFLEX MTWOASSERTS TWOASSERTS |- |-?p |-?p ATWOASSERTS ASSERT TYPES MTYPENUMERAL TYPENUMERAL ?n (TEMP_PIVOT ** $CASEINTRO) => (REFLEX => ?n = BUILTIN => BUILTIN <= Nat : ?n) || (Nat : ?n) , ?n ATYPENUMERAL BUILTIN CASEINTRO REFLEX MTYPES TYPES ?t : ?t : ?x ?t : ?x ATYPES TYPES MUNIONTYPE UNIONTYPE (?t1 <+> ?t2) : ?x (?x = ?t1 : ?x) || (?t1 : ?x) , ?t2 : ?x AUNIONTYPE UNIONTYPE MUNIV_EQ UNIV_EQ forall @ [(?P @ ?1) = ?Q @ ?1] [?P @ ?1] = [?Q @ ?1] AUNIV_EQ BOOLDEF CASEINTRO EQUATION ODDCHOICE REFLEX forall MUNIV_EQ_TAC UNIV_EQ_TAC (forall @ [(?P @ ?1) = ?Q @ ?1]) || ?t , ?u (LEFT @ $UNIV_EQ) => ([?P @ ?1] = [?Q @ ?1]) || ((EVERYWHERE @ EVAL) => (EVERYWHERE @ 0 |-| 1) => (EVERYWHERE @ UNEVAL @ [?P @ ?1]) => ?t) , ?u AUNIV_EQ_TAC BOOLDEF CASEINTRO EQUATION ODDCHOICE REFLEX forall MUNIV_RANGE_1 UNIV_RANGE_1 forallr @ [true] , [?P @ ?1] forall @ [?P @ ?1] AUNIV_RANGE_1 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forall forallr MUNIV_RANGE_2 UNIV_RANGE_2 forsomer @ [true] , [?P @ ?1] forsome @ [?P @ ?1] AUNIV_RANGE_2 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forall forallr forsome forsomer MUNIV_TAC UNIV_TAC (forall @ ?t) || ?x , ?y (LEFT @ $forall) => (RIGHT @ LEFT @ EVERYWHERE2 @ EVAL) => PIVOT => (RIGHT @ LEFT @ EVERYWHERE2 @ UNEVAL @ ?t) => (LEFT @ forall) => (forall @ ?t) || ?x , ?y AUNIV_TAC forall MUNPACK UNPACK (?x || ?y , ?z) || ?u , ?v ?x || (?y || ?u , ?v) , ?z || ?u , ?v AUNPACK CASEINTRO MX X ?x X2 =>> X1 => ?x AX DIST PLUSASSOC TIMESASSOC TIMESCOMM MX1 X1 ?x + ?y (ALLASSOCS @ PLUSASSOC) => (X => ?x) + X => ?y AX1 DIST PLUSASSOC TIMESASSOC TIMESCOMM MX2 X2 ?x * ?y X1 => COMMDIST =>> DIST => (ALLASSOCS @ TIMESASSOC) => (X => ?x) * X => ?y AX2 DIST PLUSASSOC TIMESASSOC TIMESCOMM MXALTDEF XALTDEF ?p =/= ?q (( ~?p) & ?q) | ?p & ~?q AXALTDEF AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MXOR XOR ?x =/= ?y ~?x == ?y AXOR XOR MXORALTDEF XORALTDEF (?a & ~?b) | ( ~?a) & ?b ~?a == ?b AXORALTDEF AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MXORASSOC XORASSOC (?p =/= ?q) =/= ?r ?p =/= ?q =/= ?r AXORASSOC AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MXORBOOL XORBOOL ?x =/= ?y bool : ?x =/= ?y AXORBOOL BOOLDEF CASEINTRO EQUATION NONTRIV NOT ODDCHOICE REFLEX XOR MXORDEF XORDEF ?p =/= ?q ~?p == ?q AXORDEF AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MXORFLIP XORFLIP ~?p =/= ?q ( ~?p) == ~?q AXORFLIP AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MXORSCIN XORSCIN (bool : ?x) =/= bool : ?y ?x =/= ?y AXORSCIN ASSERT BOOLDEF CASEINTRO EQUATION IFF NONTRIV NOT ODDCHOICE REFLEX TYPES XOR MXORSYM XORSYM ?p =/= ?q ?q =/= ?p AXORSYM AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR MXORTYPE XORTYPE ?x =/= ?y |-( |-?x) =/= |-?y AXORTYPE ASSERT BOOLDEF CASEINTRO EQUATION IFF NONTRIV NOT ODDCHOICE REFLEX TYPES XOR MXOR_EXP XOR_EXP (?p =/= ?q) || ?a , ?b ?p || (?q || ?b , ?a) , ?q || ?a , ?b AXOR_EXP BOOLDEF CASEINTRO EQUATION IFF NONTRIV NOT ODDCHOICE REFLEX XOR MXRULE1 XRULE1 |-?p =/= ?q ?p =/= ?q AXRULE1 ASSERT BOOLDEF CASEINTRO EQUATION IFF NONTRIV NOT ODDCHOICE REFLEX TYPES XOR MXRULE2 XRULE2 ( |-?p) =/= ?q ?p =/= ?q AXRULE2 ASSERT BOOLDEF CASEINTRO EQUATION IFF NONTRIV NOT ODDCHOICE REFLEX TYPES XOR MXRULE3 XRULE3 ?p =/= |-?q ?p =/= ?q AXRULE3 ASSERT BOOLDEF CASEINTRO EQUATION IFF NONTRIV NOT ODDCHOICE REFLEX TYPES XOR MZERONAT ZERONAT 0 Nat : 0 AZERONAT BUILTIN MZERONOTONE ZERONOTONE 0 = 1 false AZERONOTONE BUILTIN EVALEQ MZERONOTPOS ZERONOTPOS Positive @ 0 false AZERONOTPOS AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF MINUSTYPE NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE POSTYPE REFLEX TRICHOTOMY TYPES XOR MZEROORSUCC ZEROORSUCC forall @ [(0 = Nat : ?1) | forsome @ [(Nat : ?1) = 1 + Nat : ?2]] true AZEROORSUCC AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF INDUCTION NONTRIV NOT ODDCHOICE OR PLUSTYPE REFLEX TYPES XOR forall forsome Meven even even @ ?x forsome @ [(Nat : ?x) = (Nat : ?1) + Nat : ?1] Aeven even Mforall forall forall @ ?P [?P @ ?1] = [true] Aforall forall Mforall2 forall2 forall @ [?P @ ?1] [?P @ ?1] = [true] Aforall2 forall Mforallcase forallcase forall @ [?P @ ?1] (forall @ [?P @ ?1]) || true , false Aforallcase BOOLDEF EQUATION ODDCHOICE forall Mforallr forallr forallr @ ?x forall @ [((P1 @ ?x) @ ?1) -> (P2 @ ?x) @ ?1] Aforallr forallr Mforallr2 forallr2 forallr @ [?R @ ?1] , [?P @ ?1] forall @ [(?R @ ?1) -> ?P @ ?1] Aforallr2 BOOLDEF CASEINTRO EQUATION IF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX forallr Mforsome forsome forsome @ ?P ~forall @ [ ~?P @ ?1] Aforsome forsome Mforsome2 forsome2 forsome @ [?P @ ?1] ~forall @ [ ~?P @ ?1] Aforsome2 BOOLDEF CASEINTRO EQUATION NONTRIV NOT ODDCHOICE REFLEX forsome Mforsomecase forsomecase forsome @ [?P @ ?1] (forsome @ [?P @ ?1]) || true , false Aforsomecase BOOLDEF CASEINTRO EQUATION NONTRIV NOT ODDCHOICE REFLEX forsome Mforsomer forsomer forsomer @ ?x ~forallr @ (P1 @ ?x) , [ ~(P2 @ ?x) @ ?1] Aforsomer forsomer Mforsomer2 forsomer2 forsomer @ [?R @ ?1] , [?P @ ?1] ~forallr @ [?R @ ?1] , [ ~?P @ ?1] Aforsomer2 BOOLDEF CASEINTRO EQUATION NONTRIV NOT ODDCHOICE P1 P2 REFLEX forsomer Mforsomer3 forsomer3 forsomer @ [?R @ ?1] , [?P @ ?1] forsome @ [(?R @ ?1) & ?P @ ?1] Aforsomer3 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR P1 P2 REFLEX TYPES XOR forallr forsome forsomer Modd odd odd @ ?x forsome @ [(Nat : ?x) = 1 + (Nat : ?1) + Nat : ?1] Aodd odd M}3pt15b saved_environment : 3pt15b false ( ~?p) == ?p A}3pt15b AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M}3pt32 saved_environment : 3pt32 |-?p (?p | ?q) == ?p | ~?q A}3pt32 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M}3pt43a saved_environment : 3pt43a |-?p ?p & ?p | ?q A}3pt43a AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M}3pt43b saved_environment : 3pt43b |-?p ?p | ?p & ?q A}3pt43b AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M}3pt67 saved_environment : 3pt67 |-?p ?p & ?q -> ?p A}3pt67 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M}3pt68 saved_environment : 3pt68 true ?p | ?p -> ?q A}3pt68 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M}3pt75 saved_environment : 3pt75 true false -> ?p A}3pt75 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M}3pt76a saved_environment : 3pt76a true ?p -> ?p | ?q A}3pt76a AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M}3pt76b saved_environment : 3pt76b true (?p & ?q) -> ?p A}3pt76b AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M}3pt76c saved_environment : 3pt76c true (?p & ?q) -> ?p | ?q A}3pt76c AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M}3pt76d saved_environment : 3pt76d true (?p | ?q & ?r) -> ?p | ?q A}3pt76d AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M}3pt76e saved_environment : 3pt76e true (?p & ?q) -> ?p & ?q | ?r A}3pt76e AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M}3pt79 saved_environment : 3pt79 |-?r (?p -> ?r) & ( ~?p) -> ?r A}3pt79 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M}3pt81 saved_environment : 3pt81 true ((?p -> ?q) & ?q -> ?p) -> ?p == ?q A}3pt81 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M}3pt82a saved_environment : 3pt82a true ((?p -> ?q) & ?q -> ?r) -> ?p -> ?r A}3pt82a AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M}3pt82b saved_environment : 3pt82b true ((?p == ?q) & ?q -> ?r) -> ?p -> ?r A}3pt82b AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M}3pt82c saved_environment : 3pt82c true ((?p -> ?q) & ?q == ?r) -> ?p -> ?r A}3pt82c AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M}3pt83 saved_environment : 3pt83 true (?e = ?f) -> (?F @ ?e) = ?F @ ?f A}3pt83 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M}BID saved_environment : BID true ?p == ?p A}BID AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX XOR M}CONDCASESL1 saved_environment : CONDCASESL1 true (?a || ?b , ?c) == (?a & ?b) | ( ~?a) & ?c A}CONDCASESL1 AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M}CZER saved_environment : CZER false ?p & false A}CZER AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M}DINSTANTIATE saved_environment : DINSTANTIATE forsome @ ?P (?P @ ?x) | forsome @ [?P @ ?1] A}DINSTANTIATE AND BOOLDEF CASEINTRO EQUATION NONTRIV NOT ODDCHOICE OR REFLEX forall forsome M}DXM saved_environment : DXM true ?p | ~?p A}DXM AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX XOR M}DZER saved_environment : DZER true ?p | true A}DZER AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M}EQ_NOT_LESS saved_environment : EQ_NOT_LESS true ((Nat : ?x) = Nat : ?y) -> ~(Nat : ?x) < Nat : ?y A}EQ_NOT_LESS AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF LESS1 NONTRIV NOT ODDCHOICE OR PLUSTYPE REFLEX TYPES XOR forall forsome M}FORALL_LESS_MONO_ADD saved_environment : FORALL_LESS_MONO_ADD true forall @ [((Nat : ?m) < Nat : ?n) -> ((Nat : ?m) + Nat : ?1) < (Nat : ?n) + Nat : ?1] A}FORALL_LESS_MONO_ADD AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome M}FORALL_LESS_MONO_ADD_INV saved_environment : FORALL_LESS_MONO_ADD_INV true forall @ [(((Nat : ?m) + Nat : ?1) < (Nat : ?n) + Nat : ?1) -> (Nat : ?m) < Nat : ?n] A}FORALL_LESS_MONO_ADD_INV AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome M}INSTANTIATE saved_environment : INSTANTIATE forall @ [?P @ ?1] (?P @ ?x) & forall @ [?P @ ?1] A}INSTANTIATE AND BOOLDEF CASEINTRO EQUATION NONTRIV ODDCHOICE REFLEX forall M}IREF saved_environment : IREF true ?p -> ?p A}IREF AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M}IRZER saved_environment : IRZER true ?p -> true A}IRZER AND ASSERT BOOLDEF CASEINTRO CONVIF EQUATION IF IFF NONTRIV NOT ODDCHOICE OR REFLEX TYPES XOR M}Id saved_environment : Id Id @ ?x ?x A}Id Id M}LEFT saved_environment : LEFT @ ?thm ?p ^+ ?q (?thm => ?p) ^+ ?q A}LEFT M}LEQ_ADD saved_environment : LEQ_ADD true bool : (Nat : ?m) =< (Nat : ?m) + Nat : ?n A}LEQ_ADD AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome M}LEQ_MONO_ADD_EQ saved_environment : LEQ_MONO_ADD_EQ (Nat : ?m) =< Nat : ?n ((Nat : ?m) + Nat : ?p) =< (Nat : ?n) + Nat : ?p A}LEQ_MONO_ADD_EQ AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE LESS_EQ_REAL NONTRIV NOT ODDCHOICE OR PLUSASSOC PLUSCOMM PLUSCOMP PLUSID PLUSMINUS PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome M}LESS_0 saved_environment : LESS_0 true 0 < 1 + Nat : ?x A}LESS_0 AND ASSERT BOOLDEF BUILTIN CASEINTRO CONVIF EQUATION IF IFF INDUCTION LESS1 LESSCOMP LESSTYPE NONTRIV NOT ODDCHOICE OR PLUSCOMP PLUSTYPE PLUSTYPE2 REFLEX SAMESUCC TYPES XOR forall forsome M}LESS_