gf-3.1.6: examples/SUMO/TPTP/FinancialOntologyLemAx.p
fof(axFinancialLem0, axiom,
( ! [Var_ASSET] :
(hasType(type_FinancialAsset, Var_ASSET) =>
(( ? [Var_VALUE] :
(hasType(type_CurrencyMeasure, Var_VALUE) &
(f_monetaryValue(Var_ASSET,Var_VALUE)))))))).
fof(axFinancialLem1, axiom,
( ! [Var_ACCOUNT] :
(hasType(type_FinancialAccount, Var_ACCOUNT) =>
(( ? [Var_ORGANIZATION] :
(hasType(type_FinancialOrganization, Var_ORGANIZATION) &
(f_accountAt(Var_ACCOUNT,Var_ORGANIZATION)))))))).
fof(axFinancialLem2, axiom,
( ! [Var_CHECK] :
(hasType(type_Check, Var_CHECK) =>
(( ? [Var_VALUE] :
(hasType(type_CurrencyMeasure, Var_VALUE) &
(f_monetaryValue(Var_CHECK,Var_VALUE)))))))).
fof(axFinancialLem3, axiom,
( ! [Var_CHECK] :
(hasType(type_Check, Var_CHECK) =>
(( ? [Var_ACCOUNT] :
(hasType(type_FinancialAccount, Var_ACCOUNT) &
(f_checkAccount(Var_CHECK,Var_ACCOUNT)))))))).
fof(axFinancialLem4, axiom,
( ! [Var_PROCESSING] :
(hasType(type_ProcessingACheck, Var_PROCESSING) =>
(( ! [Var_WITHDRAWALTIME] :
((hasType(type_Entity, Var_WITHDRAWALTIME) & hasType(type_TimeInterval, Var_WITHDRAWALTIME)) =>
(( ! [Var_PROCESSINGTIME] :
((hasType(type_Entity, Var_PROCESSINGTIME) & hasType(type_TimeInterval, Var_PROCESSINGTIME)) =>
(( ! [Var_ACCOUNT] :
((hasType(type_FinancialAccount, Var_ACCOUNT) & hasType(type_Object, Var_ACCOUNT)) =>
(( ! [Var_AMOUNT] :
(hasType(type_CurrencyMeasure, Var_AMOUNT) =>
(( ! [Var_CHECK] :
((hasType(type_Physical, Var_CHECK) & hasType(type_Check, Var_CHECK) & hasType(type_Entity, Var_CHECK) & hasType(type_Object, Var_CHECK)) =>
(((((f_monetaryValue(Var_CHECK,Var_AMOUNT)) & (((f_checkAccount(Var_CHECK,Var_ACCOUNT)) & (((f_patient(Var_PROCESSING,Var_CHECK)) & (f_WhenFn(Var_PROCESSING) = Var_PROCESSINGTIME))))))) => (( ? [Var_WITHDRAWAL] :
(hasType(type_Withdrawal, Var_WITHDRAWAL) &
(((f_instrument(Var_WITHDRAWAL,Var_CHECK)) & (((f_WhenFn(Var_WITHDRAWAL) = Var_WITHDRAWALTIME) & (((f_meetsTemporally(Var_PROCESSINGTIME,Var_WITHDRAWALTIME)) & (((f_transactionAmount(Var_WITHDRAWAL,Var_AMOUNT)) & (f_origin(Var_WITHDRAWAL,Var_ACCOUNT))))))))))))))))))))))))))))))))).
fof(axFinancialLem5, axiom,
( ! [Var_PROCESSING] :
(hasType(type_ProcessingACheck, Var_PROCESSING) =>
(( ! [Var_ACCOUNT] :
(hasType(type_FinancialAccount, Var_ACCOUNT) =>
(( ! [Var_DEPOSITTIME] :
((hasType(type_Entity, Var_DEPOSITTIME) & hasType(type_TimeInterval, Var_DEPOSITTIME)) =>
(( ! [Var_PROCESSINGTIME] :
((hasType(type_Entity, Var_PROCESSINGTIME) & hasType(type_TimeInterval, Var_PROCESSINGTIME)) =>
(( ! [Var_AMOUNT] :
(hasType(type_CurrencyMeasure, Var_AMOUNT) =>
(( ! [Var_CHECK] :
((hasType(type_Physical, Var_CHECK) & hasType(type_Entity, Var_CHECK) & hasType(type_Object, Var_CHECK)) =>
(((((f_monetaryValue(Var_CHECK,Var_AMOUNT)) & (((f_patient(Var_PROCESSING,Var_CHECK)) & (((f_destination(Var_PROCESSING,f_CurrencyFn(Var_ACCOUNT))) & (f_WhenFn(Var_PROCESSING) = Var_PROCESSINGTIME))))))) => (( ? [Var_DEPOSIT] :
(hasType(type_Deposit, Var_DEPOSIT) &
(((f_instrument(Var_DEPOSIT,Var_CHECK)) & (((f_WhenFn(Var_DEPOSIT) = Var_DEPOSITTIME) & (((f_meetsTemporally(Var_PROCESSINGTIME,Var_DEPOSITTIME)) & (((f_transactionAmount(Var_DEPOSIT,Var_AMOUNT)) & (f_destination(Var_DEPOSIT,f_CurrencyFn(Var_ACCOUNT)))))))))))))))))))))))))))))))))).
fof(axFinancialLem6, axiom,
( ! [Var_CHECK] :
(hasType(type_Check, Var_CHECK) =>
(( ! [Var_PROCESSING] :
(hasType(type_ProcessingACheck, Var_PROCESSING) =>
(((f_patient(Var_PROCESSING,Var_CHECK)) => (( ? [Var_DEPOSITING] :
(hasType(type_DepositingACheck, Var_DEPOSITING) &
(((f_patient(Var_DEPOSITING,Var_CHECK)) & (f_time(Var_DEPOSITING,f_ImmediatePastFn(f_WhenFn(Var_PROCESSING))))))))))))))))).
fof(axFinancialLem7, axiom,
( ! [Var_DEPOSITING] :
(hasType(type_DepositingACheck, Var_DEPOSITING) =>
(( ! [Var_CHECK] :
(hasType(type_Check, Var_CHECK) =>
(( ! [Var_AGENT] :
((hasType(type_Agent, Var_AGENT) & hasType(type_CognitiveAgent, Var_AGENT)) =>
(((f_agent(Var_DEPOSITING,Var_AGENT)) => (f_signedBy(Var_CHECK,Var_AGENT))))))))))))).
fof(axFinancialLem8, axiom,
( ! [Var_DRAWING] :
(hasType(type_DrawingACheck, Var_DRAWING) =>
(( ! [Var_PROCESSING] :
(hasType(type_ProcessingACheck, Var_PROCESSING) =>
(( ! [Var_DURATION] :
(hasType(type_Quantity, Var_DURATION) =>
(( ! [Var_DUATION] :
(hasType(type_TimeDuration, Var_DUATION) =>
(( ! [Var_TIME] :
(hasType(type_TimeInterval, Var_TIME) =>
(( ! [Var_PROCESSINGTIME] :
((hasType(type_Entity, Var_PROCESSINGTIME) & hasType(type_TimeInterval, Var_PROCESSINGTIME)) =>
(( ! [Var_PROCESING] :
(hasType(type_Physical, Var_PROCESING) =>
(( ! [Var_DRAWINGTIME] :
((hasType(type_Entity, Var_DRAWINGTIME) & hasType(type_TimeInterval, Var_DRAWINGTIME)) =>
(( ! [Var_CHECK] :
(hasType(type_Entity, Var_CHECK) =>
(((((f_patient(Var_DRAWING,Var_CHECK)) & (((f_patient(Var_PROCESSING,Var_CHECK)) & (((f_WhenFn(Var_DRAWING) = Var_DRAWINGTIME) & (((f_WhenFn(Var_PROCESING) = Var_PROCESSINGTIME) & (((f_meetsTemporally(Var_DRAWINGTIME,Var_TIME)) & (((f_meetsTemporally(Var_TIME,Var_PROCESSINGTIME)) & (f_duration(Var_TIME,Var_DUATION)))))))))))))) => (f_lessThan(Var_DURATION,f_MeasureFn(6,inst_MonthDuration)))))))))))))))))))))))))))))))).
fof(axFinancialLem9, axiom,
( ! [Var_CHECK] :
(hasType(type_PayCheck, Var_CHECK) =>
(( ! [Var_GIVE] :
(hasType(type_Giving, Var_GIVE) =>
(( ! [Var_AGENT] :
((hasType(type_Entity, Var_AGENT) & hasType(type_Organization, Var_AGENT)) =>
(( ! [Var_ORGANIZATION] :
(hasType(type_CognitiveAgent, Var_ORGANIZATION) =>
(((((f_issuedBy(Var_CHECK,Var_ORGANIZATION)) & (f_destination(Var_GIVE,Var_AGENT)))) => (f_employs(Var_AGENT,Var_ORGANIZATION)))))))))))))))).
fof(axFinancialLem10, axiom,
( ! [Var_CARD] :
(hasType(type_BankCard, Var_CARD) =>
(( ? [Var_ORGANIZATION] :
(hasType(type_CognitiveAgent, Var_ORGANIZATION) &
(f_issuedBy(Var_CARD,Var_ORGANIZATION)))))))).
fof(axFinancialLem11, axiom,
( ! [Var_CARD] :
(hasType(type_BankCard, Var_CARD) =>
(( ! [Var_BANK] :
((hasType(type_CognitiveAgent, Var_BANK) & hasType(type_FinancialOrganization, Var_BANK)) =>
(((f_issuedBy(Var_CARD,Var_BANK)) => (( ? [Var_ACCOUNT] :
(hasType(type_FinancialAccount, Var_ACCOUNT) &
(((f_cardAccount(Var_CARD,Var_ACCOUNT)) & (f_accountAt(Var_ACCOUNT,Var_BANK))))))))))))))).
fof(axFinancialLem12, axiom,
( ! [Var_CARD] :
(hasType(type_DebitCard, Var_CARD) =>
(( ! [Var_AGENT] :
((hasType(type_Agent, Var_AGENT) & hasType(type_CognitiveAgent, Var_AGENT)) =>
(((f_possesses(Var_AGENT,Var_CARD)) => (( ? [Var_ACCOUNT] :
(hasType(type_DepositAccount, Var_ACCOUNT) &
(((f_cardAccount(Var_CARD,Var_ACCOUNT)) & (f_accountHolder(Var_ACCOUNT,Var_AGENT))))))))))))))).
fof(axFinancialLem13, axiom,
( ! [Var_CARD] :
(hasType(type_CreditCard, Var_CARD) =>
(( ! [Var_AGENT] :
((hasType(type_Agent, Var_AGENT) & hasType(type_CognitiveAgent, Var_AGENT)) =>
(((f_possesses(Var_AGENT,Var_CARD)) => (( ? [Var_ACCOUNT] :
(hasType(type_CreditCardAccount, Var_ACCOUNT) &
(((f_cardAccount(Var_CARD,Var_ACCOUNT)) & (f_accountHolder(Var_ACCOUNT,Var_AGENT))))))))))))))).
fof(axFinancialLem14, axiom,
( ! [Var_OPENING] :
(hasType(type_OpeningAnAccount, Var_OPENING) =>
(( ! [Var_BANK] :
(hasType(type_FinancialOrganization, Var_BANK) =>
(( ! [Var_OPENINGTIME] :
((hasType(type_Entity, Var_OPENINGTIME) & hasType(type_TimeInterval, Var_OPENINGTIME)) =>
(( ! [Var_AGENT] :
((hasType(type_Agent, Var_AGENT) & hasType(type_CognitiveAgent, Var_AGENT)) =>
(((((f_located(Var_OPENING,Var_BANK)) & (((f_agent(Var_OPENING,Var_AGENT)) & (f_WhenFn(Var_OPENING) = Var_OPENINGTIME))))) => (( ? [Var_ACCOUNT] :
(hasType(type_FinancialAccount, Var_ACCOUNT) &
(( ? [Var_ACCOUNTPERIOD] :
(hasType(type_TimeInterval, Var_ACCOUNTPERIOD) &
(((f_agreementPeriod(Var_ACCOUNT,Var_ACCOUNTPERIOD)) & (((f_meetsTemporally(Var_OPENINGTIME,Var_ACCOUNTPERIOD)) & (((f_accountAt(Var_ACCOUNT,Var_BANK)) & (f_accountHolder(Var_ACCOUNT,Var_AGENT)))))))))))))))))))))))))))).
fof(axFinancialLem15, axiom,
( ! [Var_USING] :
(hasType(type_UsingAnAccount, Var_USING) =>
(( ! [Var_AGENT] :
((hasType(type_CognitiveAgent, Var_AGENT) & hasType(type_Agent, Var_AGENT)) =>
(( ! [Var_ACCOUNT] :
((hasType(type_Entity, Var_ACCOUNT) & hasType(type_FinancialAccount, Var_ACCOUNT)) =>
(((((f_patient(Var_USING,Var_ACCOUNT)) & (f_accountHolder(Var_ACCOUNT,Var_AGENT)))) => (f_agent(Var_USING,Var_AGENT))))))))))))).
fof(axFinancialLem16, axiom,
( ! [Var_DRAWING] :
(hasType(type_DrawingACheck, Var_DRAWING) =>
(( ! [Var_ACCOUNT] :
(hasType(type_FinancialAccount, Var_ACCOUNT) =>
(( ! [Var_AGENT] :
((hasType(type_Agent, Var_AGENT) & hasType(type_CognitiveAgent, Var_AGENT)) =>
(( ! [Var_CHECK] :
((hasType(type_Entity, Var_CHECK) & hasType(type_Check, Var_CHECK)) =>
(((((f_patient(Var_DRAWING,Var_CHECK)) & (((f_agent(Var_DRAWING,Var_AGENT)) & (f_checkAccount(Var_CHECK,Var_ACCOUNT)))))) => (f_accountHolder(Var_ACCOUNT,Var_AGENT)))))))))))))))).
fof(axFinancialLem17, axiom,
( ! [Var_DEPOSITING] :
(hasType(type_DepositingACheck, Var_DEPOSITING) =>
(( ? [Var_CHECK] :
(hasType(type_Check, Var_CHECK) &
(f_patient(Var_DEPOSITING,Var_CHECK)))))))).
fof(axFinancialLem18, axiom,
( ! [Var_DEPOSITING] :
(hasType(type_DepositingACheck, Var_DEPOSITING) =>
(( ! [Var_CHECK] :
(hasType(type_Check, Var_CHECK) =>
(( ! [Var_AMOUNT] :
(hasType(type_CurrencyMeasure, Var_AMOUNT) =>
(( ! [Var_ACCOUNT] :
(hasType(type_FinancialAccount, Var_ACCOUNT) =>
(((((f_patient(Var_DEPOSITING,Var_CHECK)) & (((f_checkAccount(Var_CHECK,Var_ACCOUNT)) & (f_monetaryValue(Var_CHECK,Var_AMOUNT)))))) => (( ? [Var_DEPOSIT] :
(hasType(type_Deposit, Var_DEPOSIT) &
(((f_destination(Var_DEPOSIT,f_CurrencyFn(Var_ACCOUNT))) & (f_transactionAmount(Var_DEPOSIT,Var_AMOUNT))))))))))))))))))))).
fof(axFinancialLem19, axiom,
( ! [Var_CONTROLLING] :
(hasType(type_ControllingAnAccount, Var_CONTROLLING) =>
(( ! [Var_BANK] :
((hasType(type_FinancialOrganization, Var_BANK) & hasType(type_Agent, Var_BANK)) =>
(( ! [Var_ACCOUNT] :
((hasType(type_Entity, Var_ACCOUNT) & hasType(type_FinancialAccount, Var_ACCOUNT)) =>
(((((f_patient(Var_CONTROLLING,Var_ACCOUNT)) & (f_accountAt(Var_ACCOUNT,Var_BANK)))) => (f_agent(Var_CONTROLLING,Var_BANK))))))))))))).
fof(axFinancialLem20, axiom,
( ! [Var_PROCESSING] :
(hasType(type_ProcessingACheck, Var_PROCESSING) =>
(( ! [Var_PROCESING] :
(hasType(type_Process, Var_PROCESING) =>
(( ? [Var_CHECK] :
(hasType(type_Check, Var_CHECK) &
(f_patient(Var_PROCESING,Var_CHECK))))))))))).
fof(axFinancialLem21, axiom,
( ! [Var_PROCESSING] :
(hasType(type_ProcessingACheck, Var_PROCESSING) =>
(( ? [Var_AUTHORIZATION] :
(hasType(type_AuthorizationOfTransaction, Var_AUTHORIZATION) &
(f_subProcess(Var_AUTHORIZATION,Var_PROCESSING)))))))).
fof(axFinancialLem22, axiom,
( ! [Var_PAYMENT] :
(hasType(type_Payment, Var_PAYMENT) =>
(( ! [Var_ACCOUNT] :
(hasType(type_FinancialAccount, Var_ACCOUNT) =>
(( ! [Var_BALANCE2] :
((hasType(type_Entity, Var_BALANCE2) & hasType(type_CurrencyMeasure, Var_BALANCE2)) =>
(( ! [Var_BALANCE1] :
((hasType(type_CurrencyMeasure, Var_BALANCE1) & hasType(type_Quantity, Var_BALANCE1)) =>
(( ! [Var_AMOUNT] :
((hasType(type_CurrencyMeasure, Var_AMOUNT) & hasType(type_Quantity, Var_AMOUNT)) =>
(((((f_origin(Var_PAYMENT,f_CurrencyFn(Var_ACCOUNT))) & (((f_transactionAmount(Var_PAYMENT,Var_AMOUNT)) & (((f_currentAccountBalance(Var_ACCOUNT,f_ImmediatePastFn(f_WhenFn(Var_PAYMENT)),Var_BALANCE1)) & (Var_BALANCE2 = f_SubtractionFn(Var_BALANCE1,Var_AMOUNT)))))))) => (f_currentAccountBalance(Var_ACCOUNT,f_ImmediateFutureFn(f_WhenFn(Var_PAYMENT)),Var_BALANCE2))))))))))))))))))).
fof(axFinancialLem23, axiom,
( ! [Var_DEPOSIT] :
(hasType(type_Deposit, Var_DEPOSIT) =>
(( ? [Var_ACCOUNT] :
(hasType(type_FinancialAccount, Var_ACCOUNT) &
(f_destination(Var_DEPOSIT,f_CurrencyFn(Var_ACCOUNT))))))))).
fof(axFinancialLem24, axiom,
( ! [Var_DEPOSIT] :
(hasType(type_Deposit, Var_DEPOSIT) =>
(( ! [Var_ACCOUNT] :
(hasType(type_FinancialAccount, Var_ACCOUNT) =>
(( ! [Var_BALANCE2] :
((hasType(type_Entity, Var_BALANCE2) & hasType(type_CurrencyMeasure, Var_BALANCE2)) =>
(( ! [Var_BALANCE1] :
((hasType(type_CurrencyMeasure, Var_BALANCE1) & hasType(type_Quantity, Var_BALANCE1)) =>
(( ! [Var_AMOUNT] :
((hasType(type_CurrencyMeasure, Var_AMOUNT) & hasType(type_Quantity, Var_AMOUNT)) =>
(( ! [Var_TIMEOFDEPOSIT] :
(hasType(type_TimePosition, Var_TIMEOFDEPOSIT) =>
(((((f_time(Var_DEPOSIT,Var_TIMEOFDEPOSIT)) & (((f_destination(Var_DEPOSIT,f_CurrencyFn(Var_ACCOUNT))) & (((f_transactionAmount(Var_DEPOSIT,Var_AMOUNT)) & (((f_currentAccountBalance(Var_ACCOUNT,f_ImmediatePastFn(f_WhenFn(Var_DEPOSIT)),Var_BALANCE1)) & (Var_BALANCE2 = f_AdditionFn(Var_BALANCE1,Var_AMOUNT)))))))))) => (f_currentAccountBalance(Var_ACCOUNT,f_ImmediateFutureFn(f_FutureFn(Var_DEPOSIT)),Var_BALANCE2)))))))))))))))))))))).
fof(axFinancialLem25, axiom,
( ! [Var_WITHDRAWAL] :
(hasType(type_Withdrawal, Var_WITHDRAWAL) =>
(( ? [Var_ACCOUNT] :
(hasType(type_FinancialAccount, Var_ACCOUNT) &
(f_origin(Var_WITHDRAWAL,f_CurrencyFn(Var_ACCOUNT))))))))).
fof(axFinancialLem26, axiom,
( ! [Var_WITHDRAWAL] :
(hasType(type_Withdrawal, Var_WITHDRAWAL) =>
(( ! [Var_ACCOUNT] :
(hasType(type_FinancialAccount, Var_ACCOUNT) =>
(( ! [Var_BALANCE2] :
((hasType(type_Entity, Var_BALANCE2) & hasType(type_CurrencyMeasure, Var_BALANCE2)) =>
(( ! [Var_BALANCE1] :
((hasType(type_CurrencyMeasure, Var_BALANCE1) & hasType(type_Quantity, Var_BALANCE1)) =>
(( ! [Var_AMOUNT] :
((hasType(type_CurrencyMeasure, Var_AMOUNT) & hasType(type_Quantity, Var_AMOUNT)) =>
(( ! [Var_TIMEOFWITHDRAWAL] :
(hasType(type_TimePosition, Var_TIMEOFWITHDRAWAL) =>
(((((f_time(Var_WITHDRAWAL,Var_TIMEOFWITHDRAWAL)) & (((f_origin(Var_WITHDRAWAL,Var_ACCOUNT)) & (((f_transactionAmount(Var_WITHDRAWAL,Var_AMOUNT)) & (((f_currentAccountBalance(Var_ACCOUNT,f_ImmediatePastFn(f_WhenFn(Var_WITHDRAWAL)),Var_BALANCE1)) & (Var_BALANCE2 = f_SubtractionFn(Var_BALANCE1,Var_AMOUNT)))))))))) => (f_currentAccountBalance(Var_ACCOUNT,f_ImmediateFutureFn(f_FutureFn(Var_WITHDRAWAL)),Var_BALANCE2)))))))))))))))))))))).
fof(axFinancialLem27, axiom,
( ! [Var_MONEY] :
(hasType(type_CurrencyMeasure, Var_MONEY) =>
(( ! [Var_OBJECT] :
((hasType(type_Entity, Var_OBJECT) & hasType(type_Physical, Var_OBJECT)) =>
(( ! [Var_SELLER] :
((hasType(type_Object, Var_SELLER) & hasType(type_Entity, Var_SELLER)) =>
(( ! [Var_BUYER] :
(hasType(type_Agent, Var_BUYER) =>
(( ! [Var_PURCHASE] :
(hasType(type_Process, Var_PURCHASE) =>
(((((f_agent(Var_PURCHASE,Var_BUYER)) & (((f_origin(Var_PURCHASE,Var_SELLER)) & (((f_patient(Var_PURCHASE,Var_OBJECT)) & (f_monetaryValue(Var_OBJECT,Var_MONEY)))))))) => (( ? [Var_PAYMENT] :
(hasType(type_Payment, Var_PAYMENT) &
(((f_subProcess(Var_PAYMENT,Var_PURCHASE)) & (((f_transactionAmount(Var_PAYMENT,Var_MONEY)) & (f_destination(Var_PAYMENT,Var_SELLER)))))))))))))))))))))))))).
fof(axFinancialLem28, axiom,
( ! [Var_RATE_DECIMAL] :
((hasType(type_Entity, Var_RATE_DECIMAL) & hasType(type_Quantity, Var_RATE_DECIMAL)) =>
(( ! [Var_PERIOD] :
((hasType(type_TimeInterval, Var_PERIOD) & hasType(type_PhysicalQuantity, Var_PERIOD)) =>
(( ! [Var_AMOUNT] :
((hasType(type_Interest, Var_AMOUNT) & hasType(type_Entity, Var_AMOUNT)) =>
(( ! [Var_RATE] :
((hasType(type_InterestRate, Var_RATE) & hasType(type_PhysicalQuantity, Var_RATE)) =>
(( ! [Var_BALANCE] :
((hasType(type_CurrencyMeasure, Var_BALANCE) & hasType(type_Quantity, Var_BALANCE)) =>
(( ! [Var_ACCOUNT] :
(hasType(type_FinancialAccount, Var_ACCOUNT) =>
(((((f_principalAmount(Var_ACCOUNT,Var_BALANCE)) & (((f_fixedInterestRate(Var_ACCOUNT,Var_RATE)) & (((f_simpleInterest(Var_ACCOUNT,Var_AMOUNT,Var_PERIOD)) & (Var_RATE_DECIMAL = f_DivisionFn(f_MagnitudeFn(Var_RATE),100)))))))) => (Var_AMOUNT = f_MultiplicationFn(f_MultiplicationFn(f_MagnitudeFn(Var_PERIOD),Var_BALANCE),Var_RATE_DECIMAL)))))))))))))))))))))).
fof(axFinancialLem29, axiom,
( ! [Var_MULTIPLY] :
((hasType(type_Entity, Var_MULTIPLY) & hasType(type_Quantity, Var_MULTIPLY)) =>
(( ! [Var_EXPONENT] :
((hasType(type_Entity, Var_EXPONENT) & hasType(type_Quantity, Var_EXPONENT)) =>
(( ! [Var_ADD] :
((hasType(type_Entity, Var_ADD) & hasType(type_Quantity, Var_ADD)) =>
(( ! [Var_RATE_DECIMAL] :
((hasType(type_Entity, Var_RATE_DECIMAL) & hasType(type_Quantity, Var_RATE_DECIMAL)) =>
(( ! [Var_PERIOD] :
((hasType(type_TimeInterval, Var_PERIOD) & hasType(type_PhysicalQuantity, Var_PERIOD)) =>
(( ! [Var_INTEREST] :
((hasType(type_Interest, Var_INTEREST) & hasType(type_Entity, Var_INTEREST)) =>
(( ! [Var_RATE] :
((hasType(type_InterestRate, Var_RATE) & hasType(type_Quantity, Var_RATE)) =>
(( ! [Var_BALANCE] :
((hasType(type_CurrencyMeasure, Var_BALANCE) & hasType(type_Quantity, Var_BALANCE)) =>
(( ! [Var_ACCOUNT] :
(hasType(type_FinancialAccount, Var_ACCOUNT) =>
(((((f_principalAmount(Var_ACCOUNT,Var_BALANCE)) & (((f_fixedInterestRate(Var_ACCOUNT,Var_RATE)) & (((f_compoundInterest(Var_ACCOUNT,Var_INTEREST,Var_PERIOD)) & (((Var_RATE_DECIMAL = f_DivisionFn(Var_RATE,100)) & (((Var_ADD = f_AdditionFn(1,Var_RATE_DECIMAL)) & (((Var_EXPONENT = f_ExponentiationFn(Var_ADD,f_MagnitudeFn(Var_PERIOD))) & (Var_MULTIPLY = f_MultiplicationFn(Var_EXPONENT,Var_BALANCE)))))))))))))) => (Var_INTEREST = f_SubtractionFn(Var_MULTIPLY,Var_BALANCE))))))))))))))))))))))))))))))).
fof(axFinancialLem30, axiom,
( ! [Var_RATE] :
((hasType(type_Entity, Var_RATE) & hasType(type_InterestRate, Var_RATE)) =>
(( ! [Var_RATE_DECIMAL] :
((hasType(type_Entity, Var_RATE_DECIMAL) & hasType(type_Quantity, Var_RATE_DECIMAL)) =>
(( ! [Var_PRINCIPAL] :
((hasType(type_CurrencyMeasure, Var_PRINCIPAL) & hasType(type_Quantity, Var_PRINCIPAL)) =>
(( ! [Var_PERIOD] :
(hasType(type_TimeInterval, Var_PERIOD) =>
(( ! [Var_INTEREST] :
((hasType(type_Interest, Var_INTEREST) & hasType(type_Quantity, Var_INTEREST)) =>
(( ! [Var_ACCOUNT] :
(hasType(type_FinancialAccount, Var_ACCOUNT) =>
(((((f_simpleInterest(Var_ACCOUNT,Var_INTEREST,Var_PERIOD)) & (((f_principalAmount(Var_ACCOUNT,Var_PRINCIPAL)) & (((Var_RATE_DECIMAL = f_DivisionFn(Var_INTEREST,Var_PRINCIPAL)) & (Var_RATE = f_MultiplicationFn(Var_RATE_DECIMAL,100)))))))) => (f_interestRatePerPeriod(Var_ACCOUNT,Var_RATE,Var_PERIOD)))))))))))))))))))))).
fof(axFinancialLem31, axiom,
( ! [Var_ACCOUNT] :
(hasType(type_PersonalAccount, Var_ACCOUNT) =>
(( ! [Var_PRIMERATE] :
((hasType(type_InterestRate, Var_PRIMERATE) & hasType(type_Quantity, Var_PRIMERATE)) =>
(( ! [Var_RATE] :
((hasType(type_InterestRate, Var_RATE) & hasType(type_Quantity, Var_RATE)) =>
(( ! [Var_DATE] :
(hasType(type_Day, Var_DATE) =>
(((((f_currentInterestRate(Var_ACCOUNT,Var_DATE,Var_RATE)) & (f_primeInterestRate(Var_DATE,Var_PRIMERATE)))) => (f_greaterThan(Var_RATE,Var_PRIMERATE)))))))))))))))).
fof(axFinancialLem32, axiom,
( ! [Var_DATE] :
((hasType(type_TimeInterval, Var_DATE) & hasType(type_TimePosition, Var_DATE)) =>
(( ! [Var_PERIOD] :
(hasType(type_TimeInterval, Var_PERIOD) =>
(( ! [Var_AGREEMENT] :
(hasType(type_Contract, Var_AGREEMENT) =>
(((((f_agreementPeriod(Var_AGREEMENT,Var_PERIOD)) & (f_overlapsTemporally(Var_DATE,Var_PERIOD)))) <=> (f_agreementActive(Var_AGREEMENT,Var_DATE))))))))))))).
fof(axFinancialLem33, axiom,
( ! [Var_PRINCIPAL] :
(hasType(type_CurrencyMeasure, Var_PRINCIPAL) =>
(( ! [Var_DATE] :
((hasType(type_Day, Var_DATE) & hasType(type_TimePosition, Var_DATE)) =>
(( ! [Var_ACCOUNT] :
(hasType(type_FinancialAccount, Var_ACCOUNT) =>
(((((f_maturityDate(Var_ACCOUNT,Var_DATE)) & (f_principalAmount(Var_ACCOUNT,Var_PRINCIPAL)))) => (f_amountDue(Var_ACCOUNT,Var_PRINCIPAL,Var_DATE))))))))))))).
fof(axFinancialLem34, axiom,
( ! [Var_END] :
((hasType(type_TimeInterval, Var_END) & hasType(type_Day, Var_END)) =>
(( ! [Var_PERIOD] :
(hasType(type_TimeInterval, Var_PERIOD) =>
(( ! [Var_ACCOUNT] :
((hasType(type_Contract, Var_ACCOUNT) & hasType(type_FinancialAccount, Var_ACCOUNT)) =>
(((((f_agreementPeriod(Var_ACCOUNT,Var_PERIOD)) & (f_finishes(Var_END,Var_PERIOD)))) <=> (f_maturityDate(Var_ACCOUNT,Var_END))))))))))))).
fof(axFinancialLem35, axiom,
( ! [Var_BALANCE] :
(hasType(type_CurrencyMeasure, Var_BALANCE) =>
(( ! [Var_DATE] :
(hasType(type_Day, Var_DATE) =>
(( ! [Var_ACCOUNT] :
((hasType(type_Contract, Var_ACCOUNT) & hasType(type_FinancialAccount, Var_ACCOUNT)) =>
(((((f_effectiveDate(Var_ACCOUNT,Var_DATE)) & (f_currentAccountBalance(Var_ACCOUNT,Var_DATE,Var_BALANCE)))) => (f_originalBalance(Var_ACCOUNT,Var_BALANCE))))))))))))).
fof(axFinancialLem36, axiom,
( ! [Var_ACCOUNT] :
(hasType(type_LiabilityAccount, Var_ACCOUNT) =>
(( ! [Var_AMOUNT] :
((hasType(type_CurrencyMeasure, Var_AMOUNT) & hasType(type_Quantity, Var_AMOUNT)) =>
(( ! [Var_MINPAYMENT] :
((hasType(type_CurrencyMeasure, Var_MINPAYMENT) & hasType(type_Quantity, Var_MINPAYMENT)) =>
(((((f_minimumPayment(Var_ACCOUNT,Var_MINPAYMENT,inst_MonthDuration)) & (( ? [Var_MONTH] :
(hasType(type_Month, Var_MONTH) &
(( ? [Var_PAYMENT] :
(hasType(type_Process, Var_PAYMENT) &
(((f_destination(Var_PAYMENT,f_CurrencyFn(Var_ACCOUNT))) & (((f_paymentsPerPeriod(Var_ACCOUNT,Var_AMOUNT,Var_MONTH)) & (f_lessThan(Var_AMOUNT,Var_MINPAYMENT)))))))))))))) => (( ? [Var_PENALTY] :
(hasType(type_Penalty, Var_PENALTY) &
(f_destination(Var_PENALTY,f_CurrencyFn(Var_ACCOUNT))))))))))))))))).
fof(axFinancialLem37, axiom,
( ! [Var_OVERDRAFT] :
((hasType(type_Entity, Var_OVERDRAFT) & hasType(type_RealNumber, Var_OVERDRAFT)) =>
(( ! [Var_BALANCE] :
((hasType(type_RealNumber, Var_BALANCE) & hasType(type_Quantity, Var_BALANCE)) =>
(( ! [Var_DATE] :
(hasType(type_Day, Var_DATE) =>
(( ! [Var_ACCOUNT] :
(hasType(type_FinancialAccount, Var_ACCOUNT) =>
(((((f_currentAccountBalance(Var_ACCOUNT,Var_DATE,f_MeasureFn(Var_BALANCE,inst_UnitedStatesDollar))) & (((f_lessThan(Var_BALANCE,0)) & (Var_OVERDRAFT = f_SubtractionFn(0,Var_BALANCE)))))) => (f_overdraft(Var_ACCOUNT,f_MeasureFn(Var_OVERDRAFT,inst_UnitedStatesDollar),Var_DATE)))))))))))))))).
fof(axFinancialLem38, axiom,
( ! [Var_DATE] :
(hasType(type_Day, Var_DATE) =>
(( ! [Var_AMOUNT] :
(hasType(type_CurrencyMeasure, Var_AMOUNT) =>
(( ! [Var_LOAN] :
((hasType(type_Loan, Var_LOAN) & hasType(type_Contract, Var_LOAN) & hasType(type_FinancialAccount, Var_LOAN)) =>
(((((f_downPayment(Var_LOAN,Var_AMOUNT)) & (f_effectiveDate(Var_LOAN,Var_DATE)))) => (( ? [Var_PAYMENT] :
((hasType(type_FinancialTransaction, Var_PAYMENT) & hasType(type_Physical, Var_PAYMENT) & hasType(type_Process, Var_PAYMENT)) &
(((f_transactionAmount(Var_PAYMENT,Var_AMOUNT)) & (((f_date(Var_PAYMENT,Var_DATE)) & (f_destination(Var_PAYMENT,f_CurrencyFn(Var_LOAN))))))))))))))))))))).
fof(axFinancialLem39, axiom,
( ! [Var_BALANCE] :
((hasType(type_Entity, Var_BALANCE) & hasType(type_CurrencyMeasure, Var_BALANCE)) =>
(( ! [Var_VALUE] :
((hasType(type_CurrencyMeasure, Var_VALUE) & hasType(type_Quantity, Var_VALUE)) =>
(( ! [Var_PURCHASE] :
((hasType(type_Object, Var_PURCHASE) & hasType(type_Physical, Var_PURCHASE)) =>
(( ! [Var_AMOUNT] :
((hasType(type_CurrencyMeasure, Var_AMOUNT) & hasType(type_Quantity, Var_AMOUNT)) =>
(( ! [Var_LOAN] :
((hasType(type_Loan, Var_LOAN) & hasType(type_FinancialAccount, Var_LOAN)) =>
(((((f_downPayment(Var_LOAN,Var_AMOUNT)) & (((f_loanForPurchase(Var_LOAN,Var_PURCHASE)) & (((f_monetaryValue(Var_PURCHASE,Var_VALUE)) & (Var_BALANCE = f_SubtractionFn(Var_VALUE,Var_AMOUNT)))))))) => (f_originalBalance(Var_LOAN,Var_BALANCE))))))))))))))))))).
fof(axFinancialLem40, axiom,
( ! [Var_AMOUNT] :
(hasType(type_CurrencyMeasure, Var_AMOUNT) =>
(( ! [Var_ACTION] :
((hasType(type_FinancialTransaction, Var_ACTION) & hasType(type_Process, Var_ACTION)) =>
(( ! [Var_BANK] :
((hasType(type_FinancialOrganization, Var_BANK) & hasType(type_Agent, Var_BANK)) =>
(((f_serviceFee(Var_BANK,Var_ACTION,Var_AMOUNT)) => (( ? [Var_FEE] :
(hasType(type_ChargingAFee, Var_FEE) &
(((f_agent(Var_FEE,Var_BANK)) & (((f_causes(Var_ACTION,Var_FEE)) & (f_amountCharged(Var_FEE,Var_AMOUNT)))))))))))))))))))).
fof(axFinancialLem41, axiom,
( ! [Var_TAX] :
(hasType(type_Tax, Var_TAX) =>
(( ? [Var_ORG] :
(hasType(type_Government, Var_ORG) &
(f_agent(Var_TAX,Var_ORG)))))))).
fof(axFinancialLem42, axiom,
( ! [Var_ACCOUNT] :
(hasType(type_InterestBearingAccount, Var_ACCOUNT) =>
(( ? [Var_PERIOD] :
(hasType(type_TimeInterval, Var_PERIOD) &
(( ? [Var_RATE] :
(hasType(type_InterestRate, Var_RATE) &
(f_interestRatePerPeriod(Var_ACCOUNT,Var_RATE,Var_PERIOD))))))))))).
fof(axFinancialLem43, axiom,
( ! [Var_ACCOUNT] :
(hasType(type_PersonalAccount, Var_ACCOUNT) =>
(( ! [Var_AGENT] :
(hasType(type_Human, Var_AGENT) =>
(f_accountHolder(Var_ACCOUNT,Var_AGENT)))))))).
fof(axFinancialLem44, axiom,
( ! [Var_ACCOUNT] :
(hasType(type_SavingsAccount, Var_ACCOUNT) =>
(( ! [Var_TRANSACTION] :
(hasType(type_FinancialTransaction, Var_TRANSACTION) =>
(((f_origin(Var_TRANSACTION,f_CurrencyFn(Var_ACCOUNT))) => (( ? [Var_AUTHORIZATION] :
(hasType(type_AuthorizationOfTransaction, Var_AUTHORIZATION) &
(f_subProcess(Var_AUTHORIZATION,Var_TRANSACTION))))))))))))).
fof(axFinancialLem45, axiom,
( ! [Var_ACCOUNT] :
(hasType(type_SavingsAccount, Var_ACCOUNT) =>
(( ! [Var_PERIOD] :
(hasType(type_TimeInterval, Var_PERIOD) =>
(( ! [Var_INTEREST] :
((hasType(type_Interest, Var_INTEREST) & hasType(type_CurrencyMeasure, Var_INTEREST)) =>
(( ! [Var_AGENT] :
((hasType(type_CognitiveAgent, Var_AGENT) & hasType(type_Entity, Var_AGENT)) =>
(((((f_accountHolder(Var_ACCOUNT,Var_AGENT)) & (f_interestEarned(Var_ACCOUNT,Var_INTEREST,Var_PERIOD)))) => (( ? [Var_PAYMENT] :
((hasType(type_Process, Var_PAYMENT) & hasType(type_FinancialTransaction, Var_PAYMENT)) &
(((f_destination(Var_PAYMENT,f_CurrencyFn(Var_ACCOUNT))) & (((f_transactionAmount(Var_PAYMENT,Var_INTEREST)) & (f_destination(Var_PAYMENT,Var_AGENT))))))))))))))))))))))).
fof(axFinancialLem46, axiom,
( ! [Var_CD] :
(hasType(type_CertificateOfDeposit, Var_CD) =>
(( ? [Var_DATE] :
(hasType(type_Day, Var_DATE) &
(f_maturityDate(Var_CD,Var_DATE)))))))).
fof(axFinancialLem47, axiom,
( ! [Var_CD] :
(hasType(type_CertificateOfDeposit, Var_CD) =>
(( ! [Var_WITHDRAWAL] :
(hasType(type_Withdrawal, Var_WITHDRAWAL) =>
(( ! [Var_DATEOFWITHDRAWAL] :
((hasType(type_Day, Var_DATEOFWITHDRAWAL) & hasType(type_TimeInterval, Var_DATEOFWITHDRAWAL)) =>
(( ! [Var_MATURITYDATE] :
((hasType(type_Day, Var_MATURITYDATE) & hasType(type_TimeInterval, Var_MATURITYDATE)) =>
(((((f_maturityDate(Var_CD,Var_MATURITYDATE)) & (((f_origin(Var_WITHDRAWAL,f_CurrencyFn(Var_CD))) & (((f_date(Var_WITHDRAWAL,Var_DATEOFWITHDRAWAL)) & (f_before(f_EndFn(Var_DATEOFWITHDRAWAL),f_BeginFn(Var_MATURITYDATE))))))))) => (( ? [Var_PENALTY] :
(hasType(type_Penalty, Var_PENALTY) &
(((f_destination(Var_PENALTY,f_CurrencyFn(Var_CD))) & (f_causes(Var_WITHDRAWAL,Var_PENALTY))))))))))))))))))))).
fof(axFinancialLem48, axiom,
( ! [Var_ACCOUNT] :
(hasType(type_TraditionalSavingsAccount, Var_ACCOUNT) =>
(( ~ ( ? [Var_DATE] :
(hasType(type_Day, Var_DATE) &
(f_maturityDate(Var_ACCOUNT,Var_DATE))))))))).
fof(axFinancialLem49, axiom,
( ! [Var_ACCOUNT] :
(hasType(type_TraditionalSavingsAccount, Var_ACCOUNT) =>
(( ! [Var_WITHDRAWAL] :
(hasType(type_Withdrawal, Var_WITHDRAWAL) =>
(((f_origin(Var_WITHDRAWAL,f_CurrencyFn(Var_ACCOUNT))) => (( ? [Var_PENALTY] :
(hasType(type_Penalty, Var_PENALTY) &
(((f_destination(Var_PENALTY,f_CurrencyFn(Var_ACCOUNT))) & (f_causes(Var_WITHDRAWAL,Var_PENALTY))))))))))))))).
fof(axFinancialLem50, axiom,
( ! [Var_ACCOUNT] :
(hasType(type_CheckingAccount, Var_ACCOUNT) =>
(( ! [Var_TRANSACTION] :
(hasType(type_FinancialTransaction, Var_TRANSACTION) =>
(((f_origin(Var_TRANSACTION,f_CurrencyFn(Var_ACCOUNT))) => (((( ? [Var_CHECK] :
(hasType(type_Check, Var_CHECK) &
(f_instrument(Var_TRANSACTION,Var_CHECK))))) | (( ? [Var_DEBITCARD] :
(hasType(type_DebitCard, Var_DEBITCARD) &
(f_instrument(Var_TRANSACTION,Var_DEBITCARD))))))))))))))).
fof(axFinancialLem51, axiom,
( ! [Var_ACCOUNT] :
(hasType(type_LiabilityAccount, Var_ACCOUNT) =>
(( ! [Var_BANK] :
((hasType(type_FinancialOrganization, Var_BANK) & hasType(type_CognitiveAgent, Var_BANK)) =>
(( ! [Var_AGENT] :
(hasType(type_CognitiveAgent, Var_AGENT) =>
(((((f_accountHolder(Var_ACCOUNT,Var_AGENT)) & (f_accountAt(Var_ACCOUNT,Var_BANK)))) => (( ? [Var_DEBT] :
(hasType(type_Liability, Var_DEBT) &
(((f_agreementMember(Var_DEBT,Var_AGENT)) & (f_agreementMember(Var_DEBT,Var_BANK)))))))))))))))))).
fof(axFinancialLem52, axiom,
( ! [Var_ACCOUNT] :
(hasType(type_CreditAccount, Var_ACCOUNT) =>
(( ! [Var_PERIOD] :
(hasType(type_TimeInterval, Var_PERIOD) =>
(( ! [Var_INTEREST] :
((hasType(type_Interest, Var_INTEREST) & hasType(type_CurrencyMeasure, Var_INTEREST)) =>
(( ! [Var_AGENT] :
((hasType(type_CognitiveAgent, Var_AGENT) & hasType(type_Object, Var_AGENT)) =>
(( ! [Var_ORGANIZATION] :
((hasType(type_FinancialOrganization, Var_ORGANIZATION) & hasType(type_Entity, Var_ORGANIZATION)) =>
(((((f_accountAt(Var_ACCOUNT,Var_ORGANIZATION)) & (((f_accountHolder(Var_ACCOUNT,Var_AGENT)) & (f_interestEarned(Var_ACCOUNT,Var_INTEREST,Var_PERIOD)))))) => (( ? [Var_PAYMENT] :
((hasType(type_Process, Var_PAYMENT) & hasType(type_FinancialTransaction, Var_PAYMENT)) &
(((f_origin(Var_PAYMENT,Var_AGENT)) & (((f_transactionAmount(Var_PAYMENT,Var_INTEREST)) & (f_destination(Var_PAYMENT,Var_ORGANIZATION)))))))))))))))))))))))))).
fof(axFinancialLem53, axiom,
( ! [Var_ACCOUNT] :
(hasType(type_CreditCardAccount, Var_ACCOUNT) =>
(( ! [Var_TRANSACTION] :
(hasType(type_FinancialTransaction, Var_TRANSACTION) =>
(((f_origin(Var_TRANSACTION,f_CurrencyFn(Var_ACCOUNT))) => (( ? [Var_CARD] :
(hasType(type_CreditCard, Var_CARD) &
(f_instrument(Var_TRANSACTION,Var_CARD))))))))))))).
fof(axFinancialLem54, axiom,
( ! [Var_LOAN] :
(hasType(type_Loan, Var_LOAN) =>
(( ? [Var_LENDER] :
(hasType(type_CognitiveAgent, Var_LENDER) &
(( ? [Var_BORROWER] :
(hasType(type_CognitiveAgent, Var_BORROWER) &
(((f_borrower(Var_LOAN,Var_BORROWER)) & (f_lender(Var_LOAN,Var_LENDER))))))))))))).
fof(axFinancialLem55, axiom,
( ! [Var_INTEREST] :
((hasType(type_Interest, Var_INTEREST) & hasType(type_CurrencyMeasure, Var_INTEREST)) =>
(( ! [Var_PERIOD] :
(hasType(type_TimeInterval, Var_PERIOD) =>
(( ! [Var_LENDER] :
((hasType(type_CognitiveAgent, Var_LENDER) & hasType(type_Entity, Var_LENDER)) =>
(( ! [Var_BORROWER] :
((hasType(type_CognitiveAgent, Var_BORROWER) & hasType(type_Object, Var_BORROWER)) =>
(( ! [Var_LOAN] :
((hasType(type_Loan, Var_LOAN) & hasType(type_Contract, Var_LOAN) & hasType(type_FinancialAccount, Var_LOAN)) =>
(((((f_borrower(Var_LOAN,Var_BORROWER)) & (((f_lender(Var_LOAN,Var_LENDER)) & (((f_agreementPeriod(Var_LOAN,Var_PERIOD)) & (f_interestEarned(Var_LOAN,Var_INTEREST,Var_PERIOD)))))))) => (( ? [Var_PAYMENT] :
((hasType(type_Process, Var_PAYMENT) & hasType(type_FinancialTransaction, Var_PAYMENT)) &
(((f_origin(Var_PAYMENT,Var_BORROWER)) & (((f_transactionAmount(Var_PAYMENT,Var_INTEREST)) & (f_destination(Var_PAYMENT,Var_LENDER)))))))))))))))))))))))))).
fof(axFinancialLem56, axiom,
( ! [Var_AGENT] :
((hasType(type_CognitiveAgent, Var_AGENT) & hasType(type_Agent, Var_AGENT)) =>
(( ! [Var_LOAN] :
(hasType(type_Loan, Var_LOAN) =>
(((f_lender(Var_LOAN,Var_AGENT)) => (( ? [Var_LENDING] :
(hasType(type_Lending, Var_LENDING) &
(f_agent(Var_LENDING,Var_AGENT))))))))))))).
fof(axFinancialLem57, axiom,
( ! [Var_AGENT] :
((hasType(type_CognitiveAgent, Var_AGENT) & hasType(type_Agent, Var_AGENT)) =>
(( ! [Var_LOAN] :
(hasType(type_Loan, Var_LOAN) =>
(((f_borrower(Var_LOAN,Var_AGENT)) => (( ? [Var_BORROWING] :
(hasType(type_Borrowing, Var_BORROWING) &
(f_agent(Var_BORROWING,Var_AGENT))))))))))))).
fof(axFinancialLem58, axiom,
( ! [Var_COLLATERAL] :
(hasType(type_Collateral, Var_COLLATERAL) =>
(( ? [Var_LOAN] :
(hasType(type_SecuredLoan, Var_LOAN) &
(f_securedBy(Var_LOAN,Var_COLLATERAL)))))))).
fof(axFinancialLem59, axiom,
( ! [Var_LOAN] :
(hasType(type_Loan, Var_LOAN) =>
(( ! [Var_DEFAULT] :
(hasType(type_FinancialDefault, Var_DEFAULT) =>
(( ! [Var_BANK] :
((hasType(type_CognitiveAgent, Var_BANK) & hasType(type_Agent, Var_BANK)) =>
(( ! [Var_SECURITY] :
((hasType(type_Collateral, Var_SECURITY) & hasType(type_Object, Var_SECURITY)) =>
(((((f_securedBy(Var_LOAN,Var_SECURITY)) & (((f_lender(Var_LOAN,Var_BANK)) & (f_patient(Var_DEFAULT,Var_LOAN)))))) => (f_holdsDuring(f_ImmediateFutureFn(f_WhenFn(Var_DEFAULT)),possesses(Var_BANK,Var_SECURITY))))))))))))))))).
fof(axFinancialLem60, axiom,
( ! [Var_LOAN] :
(hasType(type_SecuredLoan, Var_LOAN) =>
(( ? [Var_SECURITY] :
(hasType(type_Collateral, Var_SECURITY) &
(f_securedBy(Var_LOAN,Var_SECURITY)))))))).
fof(axFinancialLem61, axiom,
( ! [Var_LOAN] :
(hasType(type_Mortgage, Var_LOAN) =>
(( ? [Var_ESTATE] :
(hasType(type_RealEstate, Var_ESTATE) &
(f_loanForPurchase(Var_LOAN,Var_ESTATE)))))))).
fof(axFinancialLem62, axiom,
( ! [Var_LOAN] :
(hasType(type_Mortgage, Var_LOAN) =>
(( ! [Var_REALESTATE] :
((hasType(type_Object, Var_REALESTATE) & hasType(type_Collateral, Var_REALESTATE)) =>
(((f_loanForPurchase(Var_LOAN,Var_REALESTATE)) => (f_securedBy(Var_LOAN,Var_REALESTATE)))))))))).
fof(axFinancialLem63, axiom,
( ! [Var_REFINANCING] :
(hasType(type_Refinancing, Var_REFINANCING) =>
(( ! [Var_LOAN] :
(hasType(type_Loan, Var_LOAN) =>
(( ! [Var_AMOUNT] :
(hasType(type_CurrencyMeasure, Var_AMOUNT) =>
(( ! [Var_DATE] :
(hasType(type_Day, Var_DATE) =>
(( ! [Var_BORROWER] :
(hasType(type_CognitiveAgent, Var_BORROWER) =>
(( ! [Var_COLLATERAL] :
(hasType(type_Collateral, Var_COLLATERAL) =>
(( ! [Var_TIME] :
(hasType(type_TimePosition, Var_TIME) =>
(((((f_time(Var_REFINANCING,Var_TIME)) & (((f_securedBy(Var_LOAN,Var_COLLATERAL)) & (((f_borrower(Var_LOAN,Var_BORROWER)) & (((f_currentAccountBalance(Var_LOAN,Var_DATE,Var_AMOUNT)) & (f_patient(Var_REFINANCING,Var_LOAN)))))))))) => (( ? [Var_NEWLOAN] :
(hasType(type_Loan, Var_NEWLOAN) &
(( ? [Var_PAYMENT] :
((hasType(type_Process, Var_PAYMENT) & hasType(type_Physical, Var_PAYMENT) & hasType(type_FinancialTransaction, Var_PAYMENT)) &
(((f_borrower(Var_NEWLOAN,Var_BORROWER)) & (((f_securedBy(Var_LOAN,Var_COLLATERAL)) & (((f_destination(Var_PAYMENT,f_CurrencyFn(Var_LOAN))) & (((f_time(Var_PAYMENT,Var_TIME)) & (((f_origin(Var_PAYMENT,f_CurrencyFn(Var_NEWLOAN))) & (f_transactionAmount(Var_PAYMENT,Var_AMOUNT))))))))))))))))))))))))))))))))))))))))).
fof(axFinancialLem64, axiom,
( ! [Var_COMMITMENT] :
(hasType(type_LoanCommitment, Var_COMMITMENT) =>
(( ? [Var_LOAN] :
(hasType(type_Loan, Var_LOAN) &
(( ? [Var_BORROWER] :
(hasType(type_CognitiveAgent, Var_BORROWER) &
(( ? [Var_LENDER] :
(hasType(type_CognitiveAgent, Var_LENDER) &
(((f_lender(Var_LOAN,Var_LENDER)) & (((f_borrower(Var_LOAN,Var_BORROWER)) & (((f_agreementMember(Var_COMMITMENT,Var_LENDER)) & (f_agreementMember(Var_COMMITMENT,Var_BORROWER)))))))))))))))))))).
fof(axFinancialLem65, axiom,
( ! [Var_LOAN] :
(hasType(type_BankTermLoan, Var_LOAN) =>
(( ! [Var_DURATION] :
((hasType(type_RealNumber, Var_DURATION) & hasType(type_Quantity, Var_DURATION)) =>
(( ! [Var_PERIOD] :
(hasType(type_TimeInterval, Var_PERIOD) =>
(((((f_agreementPeriod(Var_LOAN,Var_PERIOD)) & (f_duration(Var_PERIOD,f_MeasureFn(Var_DURATION,inst_YearDuration))))) => (f_greaterThanOrEqualTo(Var_DURATION,1))))))))))))).
fof(axFinancialLem66, axiom,
( ! [Var_LOAN] :
(hasType(type_ConsolidationLoan, Var_LOAN) =>
(( ? [Var_LOAN1] :
(hasType(type_Loan, Var_LOAN1) &
(( ? [Var_LOAN2] :
(hasType(type_Loan, Var_LOAN2) &
(( ? [Var_PAYMENT2] :
(hasType(type_Process, Var_PAYMENT2) &
(( ? [Var_PAYMENT1] :
(hasType(type_Process, Var_PAYMENT1) &
(((f_destination(Var_PAYMENT1,f_CurrencyFn(Var_LOAN1))) & (((f_destination(Var_PAYMENT2,f_CurrencyFn(Var_LOAN2))) & (((f_origin(Var_PAYMENT1,f_CurrencyFn(Var_LOAN))) & (f_origin(Var_PAYMENT2,f_CurrencyFn(Var_LOAN)))))))))))))))))))))))).
fof(axFinancialLem67, axiom,
( ! [Var_MORTGAGE] :
(hasType(type_ConventionalMortgage, Var_MORTGAGE) =>
(( ? [Var_GOVERNMENT] :
(hasType(type_Government, Var_GOVERNMENT) &
(f_insured(Var_MORTGAGE,Var_GOVERNMENT)))))))).
fof(axFinancialLem68, axiom,
( ! [Var_LOAN] :
(hasType(type_DayLoan, Var_LOAN) =>
(( ! [Var_PERIOD] :
(hasType(type_TimeInterval, Var_PERIOD) =>
(((f_agreementPeriod(Var_LOAN,Var_PERIOD)) & (f_duration(Var_PERIOD,f_MeasureFn(1,inst_DayDuration))))))))))).
fof(axFinancialLem69, axiom,
( ! [Var_LOAN] :
(hasType(type_SinglePaymentLoan, Var_LOAN) =>
(( ! [Var_MATURITY] :
((hasType(type_Day, Var_MATURITY) & hasType(type_TimePosition, Var_MATURITY)) =>
(( ! [Var_PRINCIPAL] :
(hasType(type_CurrencyMeasure, Var_PRINCIPAL) =>
(((((f_principalAmount(Var_LOAN,Var_PRINCIPAL)) & (f_maturityDate(Var_LOAN,Var_MATURITY)))) => (f_amountDue(Var_LOAN,Var_PRINCIPAL,Var_MATURITY))))))))))))).
fof(axFinancialLem70, axiom,
( ! [Var_LOAN] :
(hasType(type_InterestOnlyLoan, Var_LOAN) =>
(( ! [Var_DATE] :
((hasType(type_TimePosition, Var_DATE) & hasType(type_TimeInterval, Var_DATE)) =>
(( ! [Var_INTEREST] :
((hasType(type_Interest, Var_INTEREST) & hasType(type_CurrencyMeasure, Var_INTEREST)) =>
(( ! [Var_PRINCIPAL] :
(hasType(type_CurrencyMeasure, Var_PRINCIPAL) =>
(( ! [Var_PERIOD] :
(hasType(type_TimeInterval, Var_PERIOD) =>
(((((f_agreementPeriod(Var_LOAN,Var_PERIOD)) & (((f_principalAmount(Var_LOAN,Var_PRINCIPAL)) & (f_interestEarned(Var_LOAN,Var_INTEREST,Var_PERIOD)))))) => (((f_amountDue(Var_LOAN,Var_PRINCIPAL,f_EndFn(Var_PERIOD))) & (((f_amountDue(Var_LOAN,Var_INTEREST,Var_DATE)) & (f_before(f_EndFn(Var_DATE),f_EndFn(Var_PERIOD)))))))))))))))))))))))).
fof(axFinancialLem71, axiom,
( ! [Var_INDEX] :
(hasType(type_Index, Var_INDEX) =>
(( ? [Var_PERFORMANCE] :
(hasType(type_EconomicIndicator, Var_PERFORMANCE) &
(f_benchmark(Var_PERFORMANCE,Var_INDEX)))))))).
fof(axFinancialLem72, axiom,
( ! [Var_INFLATION] :
(hasType(type_Inflation, Var_INFLATION) =>
(( ! [Var_CPI] :
(hasType(type_ConsumerPriceIndex, Var_CPI) =>
(( ! [Var_PPI] :
(hasType(type_ProducerPriceIndex, Var_PPI) =>
(((f_benchmark(Var_INFLATION,Var_CPI)) | (f_benchmark(Var_INFLATION,Var_PPI))))))))))))).
fof(axFinancialLem73, axiom,
( ! [Var_INDEX] :
(hasType(type_InflationIndex, Var_INDEX) =>
(( ? [Var_INFLATION] :
(hasType(type_Inflation, Var_INFLATION) &
(f_benchmark(Var_INFLATION,Var_INDEX)))))))).
fof(axFinancialLem74, axiom,
( ! [Var_R] :
(hasType(type_RealNumber, Var_R) =>
(( ! [Var_N] :
((hasType(type_Nation, Var_N) & hasType(type_Entity, Var_N)) =>
(((f_inflationRateInCountry(Var_N,Var_R)) => (( ? [Var_I] :
(hasType(type_Inflation, Var_I) &
(((f_duration(f_WhenFn(Var_I),inst_YearDuration)) & (((f_experiencer(Var_I,Var_N)) & (f_inflationRate(Var_I,Var_R))))))))))))))))).
fof(axFinancialLem75, axiom,
( ! [Var_INDEX] :
(hasType(type_StockIndex, Var_INDEX) =>
(( ? [Var_STOCK] :
(hasType(type_Stock, Var_STOCK) &
(f_benchmark(Var_INDEX,Var_STOCK)))))))).
fof(axFinancialLem76, axiom,
( ! [Var_INVESTMENT] :
(hasType(type_Investment, Var_INVESTMENT) =>
(( ? [Var_AGENT] :
(hasType(type_Agent, Var_AGENT) &
(( ? [Var_INVESTING] :
(hasType(type_Process, Var_INVESTING) &
(((f_agent(Var_INVESTING,Var_AGENT)) & (f_possesses(Var_AGENT,Var_INVESTMENT))))))))))))).
fof(axFinancialLem77, axiom,
( ! [Var_ATTRIBUTE] :
(hasType(type_InvestmentAttribute, Var_ATTRIBUTE) =>
(( ? [Var_ACCOUNT] :
(hasType(type_InvestmentAccount, Var_ACCOUNT) &
(f_attribute(Var_ACCOUNT,Var_ATTRIBUTE)))))))).
fof(axFinancialLem78, axiom,
( ! [Var_AGENT] :
(hasType(type_Agent, Var_AGENT) =>
(( ! [Var_MONEY] :
(hasType(type_CurrencyMeasure, Var_MONEY) =>
(( ! [Var_OBJ] :
((hasType(type_Physical, Var_OBJ) & hasType(type_Entity, Var_OBJ)) =>
(((f_price(Var_OBJ,Var_MONEY,Var_AGENT)) => (( ? [Var_BUYING] :
(hasType(type_Buying, Var_BUYING) &
(((f_agent(Var_BUYING,Var_AGENT)) & (((f_patient(Var_BUYING,Var_OBJ)) & (f_transactionAmount(Var_BUYING,Var_MONEY)))))))))))))))))))).
fof(axFinancialLem79, axiom,
( ! [Var_PLACE] :
(hasType(type_PlacingAnOrder, Var_PLACE) =>
(( ! [Var_TIME] :
((hasType(type_Entity, Var_TIME) & hasType(type_TimeInterval, Var_TIME)) =>
(((f_WhenFn(Var_PLACE) = Var_TIME) => (( ? [Var_PERIOD] :
((hasType(type_Entity, Var_PERIOD) & hasType(type_TimeInterval, Var_PERIOD)) &
(( ? [Var_ORDER] :
(hasType(type_Physical, Var_ORDER) &
(((f_WhenFn(Var_ORDER) = Var_PERIOD) & (f_meetsTemporally(Var_TIME,Var_PERIOD)))))))))))))))))).
fof(axFinancialLem80, axiom,
( ! [Var_ORDER] :
(hasType(type_LimitOrder, Var_ORDER) =>
(( ? [Var_PRICE] :
(hasType(type_CurrencyMeasure, Var_PRICE) &
(f_limitPrice(Var_ORDER,Var_PRICE)))))))).
fof(axFinancialLem81, axiom,
( ! [Var_BROKER] :
(hasType(type_Broker, Var_BROKER) =>
(( ? [Var_CONTRACT] :
(hasType(type_ServiceContract, Var_CONTRACT) &
(f_agreementMember(Var_CONTRACT,Var_BROKER)))))))).
fof(axFinancialLem82, axiom,
( ! [Var_INVESTMENT] :
(hasType(type_TaxFreeInvestment, Var_INVESTMENT) =>
(( ? [Var_TAX] :
(hasType(type_Tax, Var_TAX) &
(f_origin(Var_TAX,Var_INVESTMENT)))))))).
fof(axFinancialLem83, axiom,
( ! [Var_INVESTMENT] :
(hasType(type_TaxableInvestment, Var_INVESTMENT) =>
(( ? [Var_TAX] :
(hasType(type_Tax, Var_TAX) &
(f_origin(Var_TAX,Var_INVESTMENT)))))))).
fof(axFinancialLem84, axiom,
( ! [Var_STOCK] :
(hasType(type_PreferredStock, Var_STOCK) =>
(( ? [Var_DIVIDEND] :
(hasType(type_Dividend, Var_DIVIDEND) &
(( ? [Var_AMOUNT] :
(hasType(type_CurrencyMeasure, Var_AMOUNT) &
(f_transactionAmount(Var_DIVIDEND,Var_AMOUNT))))))))))).
fof(axFinancialLem85, axiom,
( ! [Var_STOCK] :
(hasType(type_PennyStock, Var_STOCK) =>
(( ! [Var_DATE] :
(hasType(type_Agent, Var_DATE) =>
(( ! [Var_PRICE] :
((hasType(type_RealNumber, Var_PRICE) & hasType(type_Quantity, Var_PRICE)) =>
(((f_askPrice(Var_STOCK,f_MeasureFn(Var_PRICE,inst_UnitedStatesDollar),Var_DATE)) => (f_lessThan(Var_PRICE,5))))))))))))).
fof(axFinancialLem86, axiom,
( ! [Var_TIMEAFTERSPLIT] :
((hasType(type_Agent, Var_TIMEAFTERSPLIT) & hasType(type_TimeInterval, Var_TIMEAFTERSPLIT)) =>
(( ! [Var_NEWNUMBER] :
((hasType(type_Entity, Var_NEWNUMBER) & hasType(type_RealNumber, Var_NEWNUMBER)) =>
(( ! [Var_N3] :
((hasType(type_Entity, Var_N3) & hasType(type_Quantity, Var_N3)) =>
(( ! [Var_TIMEOFSPLIT] :
((hasType(type_Entity, Var_TIMEOFSPLIT) & hasType(type_TimeInterval, Var_TIMEOFSPLIT)) =>
(( ! [Var_N2] :
((hasType(type_Integer, Var_N2) & hasType(type_Quantity, Var_N2)) =>
(( ! [Var_N1] :
((hasType(type_Integer, Var_N1) & hasType(type_Quantity, Var_N1)) =>
(( ! [Var_TIME] :
((hasType(type_Agent, Var_TIME) & hasType(type_TimeInterval, Var_TIME)) =>
(( ! [Var_NUMBER] :
((hasType(type_RealNumber, Var_NUMBER) & hasType(type_Quantity, Var_NUMBER)) =>
(( ! [Var_STOCKS] :
(hasType(type_Physical, Var_STOCKS) =>
(((((f_price(Var_STOCKS,f_MeasureFn(Var_NUMBER,inst_UnitedStatesDollar),Var_TIME)) & (( ? [Var_EVENT] :
((hasType(type_StockSplit, Var_EVENT) & hasType(type_Physical, Var_EVENT)) &
(((f_splitFor(Var_EVENT,Var_N1,Var_N2)) & (f_WhenFn(Var_EVENT) = Var_TIMEOFSPLIT)))))))) => (((Var_N3 = f_MultiplicationFn(Var_NUMBER,Var_N1)) & (((Var_NEWNUMBER = f_DivisionFn(Var_N3,Var_N2)) & (((f_price(Var_STOCKS,f_MeasureFn(Var_NEWNUMBER,inst_UnitedStatesDollar),Var_TIMEAFTERSPLIT)) & (((f_meetsTemporally(Var_TIME,Var_TIMEOFSPLIT)) & (f_meetsTemporally(Var_TIMEOFSPLIT,Var_TIMEAFTERSPLIT))))))))))))))))))))))))))))))))))))))).
fof(axFinancialLem87, axiom,
( ! [Var_BOND] :
(hasType(type_Bond, Var_BOND) =>
(( ? [Var_DATE] :
(hasType(type_Day, Var_DATE) &
(f_maturityDate(Var_BOND,Var_DATE)))))))).
fof(axFinancialLem88, axiom,
( ! [Var_BOND] :
(hasType(type_Bond, Var_BOND) =>
(( ! [Var_BONDHOLDER] :
((hasType(type_Agent, Var_BONDHOLDER) & hasType(type_Entity, Var_BONDHOLDER)) =>
(( ! [Var_INTEREST] :
((hasType(type_Interest, Var_INTEREST) & hasType(type_CurrencyMeasure, Var_INTEREST)) =>
(((((f_couponInterest(Var_BOND,Var_INTEREST)) & (f_possesses(Var_BONDHOLDER,Var_BOND)))) => (( ? [Var_PAYMENT] :
(hasType(type_Process, Var_PAYMENT) &
(( ? [Var_PERIOD] :
(hasType(type_TimeDuration, Var_PERIOD) &
(((f_periodicPayment(f_AccountFn(Var_BOND),Var_INTEREST,Var_PERIOD)) & (f_destination(Var_PAYMENT,Var_BONDHOLDER))))))))))))))))))))).
fof(axFinancialLem89, axiom,
( ! [Var_ACCOUNT] :
(hasType(type_FinancialAccount, Var_ACCOUNT) =>
(( ! [Var_ASSET] :
((hasType(type_Object, Var_ASSET) & hasType(type_FinancialAsset, Var_ASSET)) =>
(( ! [Var_AGENT] :
((hasType(type_Agent, Var_AGENT) & hasType(type_CognitiveAgent, Var_AGENT)) =>
(((((f_possesses(Var_AGENT,Var_ASSET)) & (Var_ACCOUNT = f_AccountFn(Var_ASSET)))) <=> (f_accountHolder(Var_ACCOUNT,Var_AGENT))))))))))))).
fof(axFinancialLem90, axiom,
( ! [Var_BOND] :
(hasType(type_ZeroCouponBond, Var_BOND) =>
(( ! [Var_BONDACCOUNT] :
(hasType(type_FinancialAccount, Var_BONDACCOUNT) =>
(( ! [Var_TOTAL] :
((hasType(type_Entity, Var_TOTAL) & hasType(type_CurrencyMeasure, Var_TOTAL)) =>
(( ! [Var_INTEREST] :
((hasType(type_Interest, Var_INTEREST) & hasType(type_Quantity, Var_INTEREST)) =>
(( ! [Var_PERIOD] :
(hasType(type_TimeInterval, Var_PERIOD) =>
(( ! [Var_PRINCIPAL] :
((hasType(type_CurrencyMeasure, Var_PRINCIPAL) & hasType(type_Quantity, Var_PRINCIPAL)) =>
(( ! [Var_BONDHOLDER] :
((hasType(type_Agent, Var_BONDHOLDER) & hasType(type_Entity, Var_BONDHOLDER)) =>
(( ! [Var_DATE] :
(hasType(type_Day, Var_DATE) =>
(((((f_maturityDate(f_AccountFn(Var_BOND),Var_DATE)) & (((f_possesses(Var_BONDHOLDER,Var_BOND)) & (((f_principalAmount(f_AccountFn(Var_BOND),Var_PRINCIPAL)) & (((f_agreementPeriod(f_AccountFn(Var_BOND),Var_PERIOD)) & (((f_interestEarned(f_AccountFn(Var_BOND),Var_INTEREST,Var_PERIOD)) & (Var_TOTAL = f_AdditionFn(Var_PRINCIPAL,Var_INTEREST)))))))))))) => (( ? [Var_PAYMENT] :
(hasType(type_Payment, Var_PAYMENT) &
(((f_destination(Var_PAYMENT,Var_BONDHOLDER)) & (((f_origin(Var_PAYMENT,f_CurrencyFn(Var_BONDACCOUNT))) & (f_transactionAmount(Var_PAYMENT,Var_TOTAL))))))))))))))))))))))))))))))))))).
fof(axFinancialLem91, axiom,
( ! [Var_BOND] :
(hasType(type_MunicipalBond, Var_BOND) =>
(( ? [Var_AGENT] :
(hasType(type_Government, Var_AGENT) &
(f_issuedBy(Var_BOND,Var_AGENT)))))))).
fof(axFinancialLem92, axiom,
( ! [Var_BOND] :
(hasType(type_CorporateBond, Var_BOND) =>
(( ? [Var_AGENT] :
(hasType(type_Corporation, Var_AGENT) &
(f_issuedBy(Var_BOND,Var_AGENT)))))))).
fof(axFinancialLem93, axiom,
( ! [Var_BOND] :
(hasType(type_SecuredBond, Var_BOND) =>
(( ? [Var_SECURITY] :
(hasType(type_Collateral, Var_SECURITY) &
(f_securedBy(Var_BOND,Var_SECURITY)))))))).
fof(axFinancialLem94, axiom,
( ! [Var_BOND] :
(hasType(type_SecuredBond, Var_BOND) =>
(( ! [Var_DEFAULT] :
(hasType(type_FinancialDefault, Var_DEFAULT) =>
(( ! [Var_AGENT] :
(hasType(type_Agent, Var_AGENT) =>
(( ! [Var_SECURITY] :
((hasType(type_Collateral, Var_SECURITY) & hasType(type_Object, Var_SECURITY)) =>
(((((f_securedBy(Var_BOND,Var_SECURITY)) & (((f_possesses(Var_AGENT,Var_BOND)) & (f_patient(Var_DEFAULT,Var_BOND)))))) => (f_holdsDuring(f_ImmediateFutureFn(f_WhenFn(Var_DEFAULT)),possesses(Var_AGENT,Var_SECURITY))))))))))))))))).
fof(axFinancialLem95, axiom,
( ! [Var_BOND] :
(hasType(type_TreasuryBond, Var_BOND) =>
(( ? [Var_AGENT] :
(hasType(type_Government, Var_AGENT) &
(f_issuedBy(Var_BOND,Var_AGENT)))))))).
fof(axFinancialLem96, axiom,
( ! [Var_BOND] :
(hasType(type_CallableBond, Var_BOND) =>
(( ! [Var_AMOUNT] :
(hasType(type_CurrencyMeasure, Var_AMOUNT) =>
(( ! [Var_DATE] :
((hasType(type_Day, Var_DATE) & hasType(type_TimePosition, Var_DATE)) =>
(((((f_currentAccountBalance(f_AccountFn(Var_BOND),Var_DATE,Var_AMOUNT)) & (f_callDate(Var_BOND,Var_DATE)))) => (f_amountDue(f_AccountFn(Var_BOND),Var_AMOUNT,Var_DATE))))))))))))).
fof(axFinancialLem97, axiom,
( ! [Var_OPTION] :
(hasType(type_ConventionalOption, Var_OPTION) =>
(( ! [Var_PERIOD] :
(hasType(type_TimeInterval, Var_PERIOD) =>
(( ? [Var_NUMBER] :
((hasType(type_RealNumber, Var_NUMBER) & hasType(type_Quantity, Var_NUMBER)) &
(((f_agreementPeriod(Var_OPTION,Var_PERIOD)) & (((f_duration(Var_PERIOD,f_MeasureFn(Var_NUMBER,inst_MonthDuration))) & (f_lessThan(Var_NUMBER,9))))))))))))))).
fof(axFinancialLem98, axiom,
( ! [Var_OPTION] :
(hasType(type_ConventionalOption, Var_OPTION) =>
(( ! [Var_PERIOD] :
(hasType(type_TimeInterval, Var_PERIOD) =>
(( ? [Var_NUMBER] :
((hasType(type_RealNumber, Var_NUMBER) & hasType(type_Quantity, Var_NUMBER)) &
(((f_agreementPeriod(Var_OPTION,Var_PERIOD)) & (((f_duration(Var_PERIOD,f_MeasureFn(Var_NUMBER,inst_MonthDuration))) & (f_lessThan(Var_NUMBER,39))))))))))))))).
fof(axFinancialLem99, axiom,
( ! [Var_DATE] :
((hasType(type_Day, Var_DATE) & hasType(type_TimeInterval, Var_DATE)) =>
(( ! [Var_CONTRACT] :
(hasType(type_Contract, Var_CONTRACT) =>
(((f_expirationDate(Var_CONTRACT,Var_DATE)) => (( ? [Var_PERIOD] :
(hasType(type_TimeInterval, Var_PERIOD) &
(((f_agreementPeriod(Var_CONTRACT,Var_PERIOD)) & (f_finishes(Var_DATE,Var_PERIOD))))))))))))))).
fof(axFinancialLem100, axiom,
( ! [Var_AGENT] :
(hasType(type_CognitiveAgent, Var_AGENT) =>
(( ! [Var_PREMIUM] :
(hasType(type_CurrencyMeasure, Var_PREMIUM) =>
(( ! [Var_OPTION] :
((hasType(type_Option, Var_OPTION) & hasType(type_Investment, Var_OPTION)) =>
(((((f_premium(Var_OPTION,Var_PREMIUM)) & (f_optionHolder(Var_OPTION,Var_AGENT)))) => (f_potentialLoss(Var_AGENT,Var_OPTION,Var_PREMIUM))))))))))))).
fof(axFinancialLem101, axiom,
( ! [Var_KILL] :
(hasType(type_CancellingAnOrder, Var_KILL) =>
(( ! [Var_ORDER] :
((hasType(type_Entity, Var_ORDER) & hasType(type_Contract, Var_ORDER)) =>
(((f_patient(Var_KILL,Var_ORDER)) => (( ~ (f_agreementActive(Var_ORDER,f_ImmediateFutureFn(f_WhenFn(Var_KILL)))))))))))))).
fof(axFinancialLem102, axiom,
( ! [Var_ORDER] :
(hasType(type_IOCOrder, Var_ORDER) =>
(( ! [Var_PERIOD] :
(hasType(type_TimeInterval, Var_PERIOD) =>
(((f_agreementPeriod(Var_ORDER,Var_PERIOD)) => (((( ? [Var_FILL] :
(hasType(type_FillingAnOrder, Var_FILL) &
(( ? [Var_TIME1] :
((hasType(type_Entity, Var_TIME1) & hasType(type_TimeInterval, Var_TIME1)) &
(((f_patient(Var_FILL,Var_ORDER)) & (((f_WhenFn(Var_FILL) = Var_TIME1) & (f_starts(Var_TIME1,Var_PERIOD)))))))))))) | (( ? [Var_KILL] :
(hasType(type_CancellingAnOrder, Var_KILL) &
(( ? [Var_TIME2] :
((hasType(type_Entity, Var_TIME2) & hasType(type_TimeInterval, Var_TIME2)) &
(((f_patient(Var_KILL,Var_ORDER)) & (((f_WhenFn(Var_KILL) = Var_TIME2) & (f_starts(Var_TIME2,Var_PERIOD)))))))))))))))))))))).
fof(axFinancialLem103, axiom,
( ! [Var_ORDER] :
(hasType(type_FOKOrder, Var_ORDER) =>
(( ! [Var_PERIOD] :
(hasType(type_TimeInterval, Var_PERIOD) =>
(((f_agreementPeriod(Var_ORDER,Var_PERIOD)) => (((( ? [Var_FILL] :
(hasType(type_FillingAnOrder, Var_FILL) &
(( ? [Var_TIME1] :
((hasType(type_Entity, Var_TIME1) & hasType(type_TimeInterval, Var_TIME1)) &
(((f_patient(Var_FILL,Var_ORDER)) & (((f_WhenFn(Var_FILL) = Var_TIME1) & (f_starts(Var_TIME1,Var_PERIOD)))))))))))) | (( ? [Var_KILL] :
(hasType(type_CancellingAnOrder, Var_KILL) &
(( ? [Var_TIME2] :
((hasType(type_Entity, Var_TIME2) & hasType(type_TimeInterval, Var_TIME2)) &
(((f_patient(Var_KILL,Var_ORDER)) & (((f_WhenFn(Var_KILL) = Var_TIME2) & (f_starts(Var_TIME2,Var_PERIOD)))))))))))))))))))))).
fof(axFinancialLem104, axiom,
( ! [Var_ORDER] :
(hasType(type_GTCOrder, Var_ORDER) =>
(( ! [Var_END] :
((hasType(type_Entity, Var_END) & hasType(type_TimeInterval, Var_END)) =>
(( ! [Var_TIME] :
((hasType(type_Entity, Var_TIME) & hasType(type_TimeInterval, Var_TIME)) =>
(( ! [Var_PERIOD] :
(hasType(type_TimeInterval, Var_PERIOD) =>
(((f_agreementPeriod(Var_ORDER,Var_PERIOD)) => (((( ? [Var_EXECUTE] :
(hasType(type_FillingAnOrder, Var_EXECUTE) &
(((f_patient(Var_EXECUTE,Var_ORDER)) & (((f_WhenFn(Var_EXECUTE) = Var_TIME) & (f_overlapsTemporally(Var_TIME,Var_PERIOD))))))))) | (( ? [Var_CANCEL] :
(hasType(type_CancellingAnOrder, Var_CANCEL) &
(((f_patient(Var_CANCEL,Var_ORDER)) & (((f_WhenFn(Var_CANCEL) = Var_END) & (f_finishes(Var_END,Var_PERIOD))))))))))))))))))))))))).
fof(axFinancialLem105, axiom,
( ! [Var_ORDER] :
(hasType(type_DayOrder, Var_ORDER) =>
(( ! [Var_PERIOD] :
(hasType(type_TimeInterval, Var_PERIOD) =>
(((f_agreementPeriod(Var_ORDER,Var_PERIOD)) & (f_duration(Var_PERIOD,f_MeasureFn(1,inst_DayDuration))))))))))).
fof(axFinancialLem106, axiom,
( ! [Var_OPTION] :
(hasType(type_CallOption, Var_OPTION) =>
(( ! [Var_TIME] :
((hasType(type_Agent, Var_TIME) & hasType(type_TimePosition, Var_TIME)) =>
(((( ? [Var_STRIKEPRICE] :
((hasType(type_CurrencyMeasure, Var_STRIKEPRICE) & hasType(type_Quantity, Var_STRIKEPRICE)) &
(( ? [Var_STOCKPRICE] :
((hasType(type_CurrencyMeasure, Var_STOCKPRICE) & hasType(type_Quantity, Var_STOCKPRICE)) &
(( ? [Var_STOCK] :
((hasType(type_FinancialInstrument, Var_STOCK) & hasType(type_Physical, Var_STOCK)) &
(((f_underlier(Var_OPTION,Var_STOCK)) & (((f_price(Var_STOCK,Var_STOCKPRICE,Var_TIME)) & (((f_strikePrice(Var_OPTION,Var_STRIKEPRICE)) & (f_lessThan(Var_STRIKEPRICE,Var_STOCKPRICE))))))))))))))))) <=> (f_inTheMoney(Var_OPTION,Var_TIME)))))))))).
fof(axFinancialLem107, axiom,
( ! [Var_OPTION] :
(hasType(type_PutOption, Var_OPTION) =>
(( ! [Var_TIME] :
((hasType(type_Agent, Var_TIME) & hasType(type_TimePosition, Var_TIME)) =>
(((( ? [Var_STRIKEPRICE] :
((hasType(type_CurrencyMeasure, Var_STRIKEPRICE) & hasType(type_Quantity, Var_STRIKEPRICE)) &
(( ? [Var_STOCKPRICE] :
((hasType(type_CurrencyMeasure, Var_STOCKPRICE) & hasType(type_Quantity, Var_STOCKPRICE)) &
(( ? [Var_STOCK] :
((hasType(type_FinancialInstrument, Var_STOCK) & hasType(type_Physical, Var_STOCK)) &
(((f_underlier(Var_OPTION,Var_STOCK)) & (((f_price(Var_STOCK,Var_STOCKPRICE,Var_TIME)) & (((f_strikePrice(Var_OPTION,Var_STRIKEPRICE)) & (f_lessThan(Var_STOCKPRICE,Var_STRIKEPRICE))))))))))))))))) <=> (f_inTheMoney(Var_OPTION,Var_TIME)))))))))).
fof(axFinancialLem108, axiom,
( ! [Var_OPTION] :
(hasType(type_Option, Var_OPTION) =>
(( ! [Var_TIME] :
((hasType(type_Agent, Var_TIME) & hasType(type_TimePosition, Var_TIME)) =>
(((( ? [Var_STRIKEPRICE] :
((hasType(type_CurrencyMeasure, Var_STRIKEPRICE) & hasType(type_Entity, Var_STRIKEPRICE)) &
(( ? [Var_STOCKPRICE] :
((hasType(type_CurrencyMeasure, Var_STOCKPRICE) & hasType(type_Entity, Var_STOCKPRICE)) &
(( ? [Var_STOCK] :
((hasType(type_FinancialInstrument, Var_STOCK) & hasType(type_Physical, Var_STOCK)) &
(((f_underlier(Var_OPTION,Var_STOCK)) & (((f_price(Var_STOCK,Var_STOCKPRICE,Var_TIME)) & (((f_strikePrice(Var_OPTION,Var_STRIKEPRICE)) & (Var_STOCKPRICE = Var_STRIKEPRICE)))))))))))))))) <=> (f_atTheMoney(Var_OPTION,Var_TIME)))))))))).
fof(axFinancialLem109, axiom,
( ! [Var_OPTION] :
(hasType(type_CallOption, Var_OPTION) =>
(( ! [Var_TIME] :
((hasType(type_Agent, Var_TIME) & hasType(type_TimePosition, Var_TIME)) =>
(((( ? [Var_STRIKEPRICE] :
((hasType(type_CurrencyMeasure, Var_STRIKEPRICE) & hasType(type_Quantity, Var_STRIKEPRICE)) &
(( ? [Var_STOCKPRICE] :
((hasType(type_CurrencyMeasure, Var_STOCKPRICE) & hasType(type_Quantity, Var_STOCKPRICE)) &
(( ? [Var_STOCK] :
((hasType(type_FinancialInstrument, Var_STOCK) & hasType(type_Physical, Var_STOCK)) &
(((f_underlier(Var_OPTION,Var_STOCK)) & (((f_price(Var_STOCK,Var_STOCKPRICE,Var_TIME)) & (((f_strikePrice(Var_OPTION,Var_STRIKEPRICE)) & (f_lessThan(Var_STOCKPRICE,Var_STRIKEPRICE))))))))))))))))) <=> (f_outOfTheMoney(Var_OPTION,Var_TIME)))))))))).
fof(axFinancialLem110, axiom,
( ! [Var_OPTION] :
(hasType(type_PutOption, Var_OPTION) =>
(( ! [Var_TIME] :
((hasType(type_Agent, Var_TIME) & hasType(type_TimePosition, Var_TIME)) =>
(((( ? [Var_STRIKEPRICE] :
((hasType(type_CurrencyMeasure, Var_STRIKEPRICE) & hasType(type_Quantity, Var_STRIKEPRICE)) &
(( ? [Var_STOCKPRICE] :
((hasType(type_CurrencyMeasure, Var_STOCKPRICE) & hasType(type_Quantity, Var_STOCKPRICE)) &
(( ? [Var_STOCK] :
((hasType(type_FinancialInstrument, Var_STOCK) & hasType(type_Physical, Var_STOCK)) &
(((f_underlier(Var_OPTION,Var_STOCK)) & (((f_price(Var_STOCK,Var_STOCKPRICE,Var_TIME)) & (((f_strikePrice(Var_OPTION,Var_STRIKEPRICE)) & (f_lessThan(Var_STRIKEPRICE,Var_STOCKPRICE))))))))))))))))) <=> (f_outOfTheMoney(Var_OPTION,Var_TIME)))))))))).
fof(axFinancialLem111, axiom,
( ! [Var_SPREAD] :
(hasType(type_SpreadOption, Var_SPREAD) =>
(( ? [Var_OPTION1] :
(hasType(type_Option, Var_OPTION1) &
(( ? [Var_OPTION2] :
(hasType(type_Option, Var_OPTION2) &
(( ? [Var_BUY] :
(hasType(type_Buying, Var_BUY) &
(( ? [Var_SELL] :
(hasType(type_Selling, Var_SELL) &
(( ? [Var_TIME] :
(hasType(type_TimePosition, Var_TIME) &
(((f_patient(Var_BUY,Var_OPTION1)) & (((f_patient(Var_SELL,Var_OPTION2)) & (((f_time(Var_BUY,Var_TIME)) & (f_time(Var_SELL,Var_TIME)))))))))))))))))))))))))).
fof(axFinancialLem112, axiom,
( ! [Var_SPREAD] :
(hasType(type_ButterflySpread, Var_SPREAD) =>
(( ? [Var_CALL1] :
(hasType(type_CallOption, Var_CALL1) &
(( ? [Var_CALL2] :
(hasType(type_CallOption, Var_CALL2) &
(( ? [Var_CALL3] :
(hasType(type_CallOption, Var_CALL3) &
(( ? [Var_CALL4] :
(hasType(type_CallOption, Var_CALL4) &
(( ? [Var_PRICE4] :
((hasType(type_CurrencyMeasure, Var_PRICE4) & hasType(type_Quantity, Var_PRICE4)) &
(( ? [Var_PRICE3] :
((hasType(type_CurrencyMeasure, Var_PRICE3) & hasType(type_Quantity, Var_PRICE3)) &
(( ? [Var_PRICE2] :
((hasType(type_CurrencyMeasure, Var_PRICE2) & hasType(type_Quantity, Var_PRICE2)) &
(( ? [Var_PRICE1] :
((hasType(type_CurrencyMeasure, Var_PRICE1) & hasType(type_Quantity, Var_PRICE1)) &
(((f_strikePrice(Var_CALL1,Var_PRICE1)) & (((f_strikePrice(Var_CALL2,Var_PRICE2)) & (((f_strikePrice(Var_CALL3,Var_PRICE3)) & (((f_strikePrice(Var_CALL4,Var_PRICE4)) & (((f_lessThan(Var_PRICE1,Var_PRICE2)) & (((f_lessThan(Var_PRICE1,Var_PRICE3)) & (((f_greaterThan(Var_PRICE4,Var_PRICE2)) & (f_greaterThan(Var_PRICE4,Var_PRICE2))))))))))))))))))))))))))))))))))))))))))).
fof(axFinancialLem113, axiom,
( ! [Var_TRANSACTION] :
(hasType(type_StockMarketTransaction, Var_TRANSACTION) =>
(( ? [Var_MARKET] :
(hasType(type_StockMarket, Var_MARKET) &
(f_located(Var_TRANSACTION,Var_MARKET)))))))).
fof(axFinancialLem114, axiom,
( ! [Var_UPTICK] :
(hasType(type_Uptick, Var_UPTICK) =>
(( ! [Var_PRICE2] :
((hasType(type_CurrencyMeasure, Var_PRICE2) & hasType(type_Quantity, Var_PRICE2)) =>
(( ! [Var_PRICE1] :
((hasType(type_CurrencyMeasure, Var_PRICE1) & hasType(type_Quantity, Var_PRICE1)) =>
(( ! [Var_TIME1] :
((hasType(type_Entity, Var_TIME1) & hasType(type_Agent, Var_TIME1) & hasType(type_TimeInterval, Var_TIME1)) =>
(( ! [Var_STOCK] :
((hasType(type_Entity, Var_STOCK) & hasType(type_Physical, Var_STOCK)) =>
(((((f_patient(Var_UPTICK,Var_STOCK)) & (((f_WhenFn(Var_UPTICK) = Var_TIME1) & (f_price(Var_STOCK,Var_PRICE1,Var_TIME1)))))) => (( ? [Var_TRANSACTION] :
(hasType(type_StockMarketTransaction, Var_TRANSACTION) &
(( ? [Var_TIME2] :
((hasType(type_Entity, Var_TIME2) & hasType(type_TimeInterval, Var_TIME2) & hasType(type_Agent, Var_TIME2)) &
(((f_patient(Var_TRANSACTION,Var_STOCK)) & (((f_WhenFn(Var_TRANSACTION) = Var_TIME2) & (((f_meetsTemporally(Var_TIME2,Var_TIME1)) & (((f_price(Var_STOCK,Var_PRICE2,Var_TIME2)) & (f_lessThan(Var_PRICE2,Var_PRICE1))))))))))))))))))))))))))))))))).
fof(axFinancialLem115, axiom,
( ! [Var_DOWNTICK] :
(hasType(type_Downtick, Var_DOWNTICK) =>
(( ! [Var_PRICE2] :
((hasType(type_CurrencyMeasure, Var_PRICE2) & hasType(type_Quantity, Var_PRICE2)) =>
(( ! [Var_PRICE1] :
((hasType(type_CurrencyMeasure, Var_PRICE1) & hasType(type_Quantity, Var_PRICE1)) =>
(( ! [Var_TIME1] :
((hasType(type_Entity, Var_TIME1) & hasType(type_Agent, Var_TIME1) & hasType(type_TimeInterval, Var_TIME1)) =>
(( ! [Var_STOCK] :
((hasType(type_Entity, Var_STOCK) & hasType(type_Physical, Var_STOCK)) =>
(((((f_patient(Var_DOWNTICK,Var_STOCK)) & (((f_WhenFn(Var_DOWNTICK) = Var_TIME1) & (f_price(Var_STOCK,Var_PRICE1,Var_TIME1)))))) => (( ? [Var_TRANSACTION] :
(hasType(type_StockMarketTransaction, Var_TRANSACTION) &
(( ? [Var_TIME2] :
((hasType(type_Entity, Var_TIME2) & hasType(type_TimeInterval, Var_TIME2) & hasType(type_Agent, Var_TIME2)) &
(((f_patient(Var_TRANSACTION,Var_STOCK)) & (((f_WhenFn(Var_TRANSACTION) = Var_TIME2) & (((f_meetsTemporally(Var_TIME2,Var_TIME1)) & (((f_price(Var_STOCK,Var_PRICE2,Var_TIME2)) & (f_greaterThan(Var_PRICE2,Var_PRICE1))))))))))))))))))))))))))))))))).
fof(axFinancialLem116, axiom,
( ! [Var_AGENT] :
(hasType(type_CognitiveAgent, Var_AGENT) =>
(( ! [Var_ORG] :
((hasType(type_Organization, Var_ORG) & hasType(type_CognitiveAgent, Var_ORG)) =>
(((f_employs(Var_ORG,Var_AGENT)) <=> (( ? [Var_EMPLOYMENT] :
(hasType(type_Employment, Var_EMPLOYMENT) &
(((f_agreementMember(Var_EMPLOYMENT,Var_ORG)) & (f_agreementMember(Var_EMPLOYMENT,Var_AGENT))))))))))))))).
fof(axFinancialLem117, axiom,
( ! [Var_MONEY] :
(hasType(type_CurrencyMeasure, Var_MONEY) =>
(( ! [Var_AGENT] :
(hasType(type_Human, Var_AGENT) =>
(((f_monthlyIncome(Var_AGENT,Var_MONEY)) <=> (( ? [Var_MONTH] :
(hasType(type_Month, Var_MONTH) &
(f_income(Var_AGENT,Var_MONEY,Var_MONTH))))))))))))).
fof(axFinancialLem118, axiom,
( ! [Var_ACTIVITY] :
((hasType(type_OrganizationalProcess, Var_ACTIVITY) & hasType(type_Process, Var_ACTIVITY)) =>
(( ! [Var_MONEY] :
(hasType(type_CurrencyMeasure, Var_MONEY) =>
(( ! [Var_AGENT] :
((hasType(type_Human, Var_AGENT) & hasType(type_Agent, Var_AGENT)) =>
(((f_incomeEarned(Var_AGENT,Var_MONEY,Var_ACTIVITY)) => (f_agent(Var_ACTIVITY,Var_AGENT))))))))))))).
fof(axFinancialLem119, axiom,
( ! [Var_TIME] :
(hasType(type_TimePosition, Var_TIME) =>
(( ! [Var_ACTIVITY] :
((hasType(type_OrganizationalProcess, Var_ACTIVITY) & hasType(type_Physical, Var_ACTIVITY) & hasType(type_Process, Var_ACTIVITY)) =>
(( ! [Var_INCOME] :
(hasType(type_CurrencyMeasure, Var_INCOME) =>
(( ! [Var_AGENT] :
(hasType(type_Human, Var_AGENT) =>
(((((f_taxDeferredIncome(Var_AGENT,Var_INCOME,Var_ACTIVITY)) & (f_time(Var_ACTIVITY,Var_TIME)))) => (( ? [Var_TAX] :
(hasType(type_Tax, Var_TAX) &
(((f_causes(Var_ACTIVITY,Var_TAX)) & (f_time(Var_TAX,Var_TIME))))))))))))))))))))).
fof(axFinancialLem120, axiom,
( ! [Var_ATINCOME] :
((hasType(type_Entity, Var_ATINCOME) & hasType(type_OrganizationalProcess, Var_ATINCOME)) =>
(( ! [Var_ACTIVITY] :
((hasType(type_OrganizationalProcess, Var_ACTIVITY) & hasType(type_Process, Var_ACTIVITY) & hasType(type_CurrencyMeasure, Var_ACTIVITY)) =>
(( ! [Var_AGENT] :
(hasType(type_Human, Var_AGENT) =>
(((( ? [Var_TAXAMOUNT] :
((hasType(type_CurrencyMeasure, Var_TAXAMOUNT) & hasType(type_Quantity, Var_TAXAMOUNT)) &
(( ? [Var_TAX] :
((hasType(type_ChargingAFee, Var_TAX) & hasType(type_Process, Var_TAX)) &
(( ? [Var_INCOME] :
((hasType(type_CurrencyMeasure, Var_INCOME) & hasType(type_Quantity, Var_INCOME)) &
(((f_incomeEarned(Var_AGENT,Var_INCOME,Var_ACTIVITY)) & (((f_amountCharged(Var_TAX,Var_TAXAMOUNT)) & (((f_causes(Var_ACTIVITY,Var_TAX)) & (Var_ATINCOME = f_SubtractionFn(Var_INCOME,Var_TAXAMOUNT))))))))))))))))) <=> (f_afterTaxIncome(Var_AGENT,Var_ACTIVITY,Var_ATINCOME))))))))))))).
fof(axFinancialLem121, axiom,
( ! [Var_PERIOD] :
(hasType(type_TimeInterval, Var_PERIOD) =>
(( ! [Var_MONEY] :
(hasType(type_CurrencyMeasure, Var_MONEY) =>
(( ! [Var_AGENT] :
((hasType(type_Human, Var_AGENT) & hasType(type_CognitiveAgent, Var_AGENT) & hasType(type_Entity, Var_AGENT)) =>
(((f_employeeContribution(Var_AGENT,Var_MONEY,Var_PERIOD)) => (( ? [Var_PLAN] :
(hasType(type_PensionPlan, Var_PLAN) &
(( ? [Var_ORG] :
((hasType(type_Organization, Var_ORG) & hasType(type_Agent, Var_ORG)) &
(((f_employs(Var_ORG,Var_AGENT)) & (((f_agent(Var_PLAN,Var_ORG)) & (f_destination(Var_PLAN,Var_AGENT))))))))))))))))))))))).
fof(axFinancialLem122, axiom,
( ! [Var_PERIOD] :
((hasType(type_TimePosition, Var_PERIOD) & hasType(type_Entity, Var_PERIOD)) =>
(( ! [Var_MONEY] :
(hasType(type_CurrencyMeasure, Var_MONEY) =>
(( ! [Var_AGENT] :
((hasType(type_Human, Var_AGENT) & hasType(type_Agent, Var_AGENT)) =>
(((f_compensationPackage(Var_AGENT,Var_MONEY,Var_PERIOD)) => (( ? [Var_ACTIVITY] :
(hasType(type_Working, Var_ACTIVITY) &
(((f_agent(Var_ACTIVITY,Var_AGENT)) & (((Var_PERIOD = f_WhenFn(Var_ACTIVITY)) & (f_incomeEarned(Var_AGENT,Var_MONEY,Var_ACTIVITY)))))))))))))))))))).
fof(axFinancialLem123, axiom,
( ! [Var_STARTDATE] :
((hasType(type_Day, Var_STARTDATE) & hasType(type_TimeInterval, Var_STARTDATE)) =>
(( ! [Var_AGREEMENT] :
(hasType(type_Contract, Var_AGREEMENT) =>
(((f_effectiveDate(Var_AGREEMENT,Var_STARTDATE)) <=> (( ? [Var_PERIOD] :
(hasType(type_TimeInterval, Var_PERIOD) &
(((f_agreementPeriod(Var_AGREEMENT,Var_PERIOD)) & (f_starts(Var_STARTDATE,Var_PERIOD))))))))))))))).
fof(axFinancialLem124, axiom,
( ! [Var_CASH] :
(hasType(type_Cash, Var_CASH) =>
(( ? [Var_VALUE] :
(hasType(type_CurrencyMeasure, Var_VALUE) &
(f_monetaryValue(Var_CASH,Var_VALUE)))))))).
fof(axFinancialLem125, axiom,
( ! [Var_INVESTMENT] :
(hasType(type_Investment, Var_INVESTMENT) =>
(( ! [Var_LEVEL] :
(hasType(type_RiskAttribute, Var_LEVEL) =>
(( ! [Var_AGENT] :
((hasType(type_Investor, Var_AGENT) & hasType(type_Agent, Var_AGENT)) =>
(((((f_riskTolerance(Var_AGENT,Var_LEVEL)) & (f_possesses(Var_AGENT,Var_INVESTMENT)))) => (f_riskLevel(Var_INVESTMENT,Var_LEVEL))))))))))))).
fof(axFinancialLem126, axiom,
( ! [Var_ACCOUNT] :
((hasType(type_FinancialAccount, Var_ACCOUNT) & hasType(type_Entity, Var_ACCOUNT)) =>
(( ! [Var_CARD] :
(hasType(type_BankCard, Var_CARD) =>
(( ! [Var_CODE] :
(hasType(type_ContentBearingObject, Var_CODE) =>
(((((f_cardCode(Var_CODE,Var_CARD)) & (f_cardAccount(Var_CARD,Var_ACCOUNT)))) => (( ? [Var_ENCODING] :
(hasType(type_Encoding, Var_ENCODING) &
(f_patient(Var_ENCODING,Var_ACCOUNT)))))))))))))))).
fof(axFinancialLem127, axiom,
( ! [Var_CARD] :
(hasType(type_DebitCard, Var_CARD) =>
(( ! [Var_TRANSACTION] :
(hasType(type_FinancialTransaction, Var_TRANSACTION) =>
(( ! [Var_AGENT] :
(hasType(type_Agent, Var_AGENT) =>
(((((f_possesses(Var_AGENT,Var_CARD)) & (f_instrument(Var_TRANSACTION,Var_CARD)))) => (( ? [Var_ENTER] :
(hasType(type_EnteringAPin, Var_ENTER) &
(( ? [Var_PIN] :
((hasType(type_SymbolicString, Var_PIN) & hasType(type_Entity, Var_PIN)) &
(((f_pin(Var_PIN,Var_CARD)) & (((f_patient(Var_ENTER,Var_PIN)) & (f_agent(Var_ENTER,Var_AGENT))))))))))))))))))))))).
fof(axFinancialLem128, axiom,
( ! [Var_ENTER] :
(hasType(type_EnteringAPin, Var_ENTER) =>
(( ? [Var_CARD] :
(hasType(type_BankCard, Var_CARD) &
(( ? [Var_PIN] :
((hasType(type_SymbolicString, Var_PIN) & hasType(type_Entity, Var_PIN)) &
(((f_pin(Var_PIN,Var_CARD)) & (f_patient(Var_ENTER,Var_PIN))))))))))))).
fof(axFinancialLem129, axiom,
( ! [Var_CHECK] :
(hasType(type_VerifyingCardCode, Var_CHECK) =>
(( ! [Var_CARD] :
(hasType(type_BankCard, Var_CARD) =>
(( ! [Var_CODE] :
((hasType(type_Entity, Var_CODE) & hasType(type_ContentBearingObject, Var_CODE)) =>
(((((f_patient(Var_CHECK,Var_CODE)) & (f_cardCode(Var_CODE,Var_CARD)))) => (( ? [Var_DECODE] :
(hasType(type_Decoding, Var_DECODE) &
(((f_subProcess(Var_DECODE,Var_CHECK)) & (f_patient(Var_DECODE,Var_CODE)))))))))))))))))).
fof(axFinancialLem130, axiom,
( ! [Var_AGENT2] :
((hasType(type_CognitiveAgent, Var_AGENT2) & hasType(type_Agent, Var_AGENT2)) =>
(( ! [Var_AGENT1] :
((hasType(type_CognitiveAgent, Var_AGENT1) & hasType(type_Entity, Var_AGENT1)) =>
(((f_customer(Var_AGENT1,Var_AGENT2)) <=> (( ? [Var_SERVICE] :
(hasType(type_FinancialTransaction, Var_SERVICE) &
(((f_agent(Var_SERVICE,Var_AGENT2)) & (f_destination(Var_SERVICE,Var_AGENT1))))))))))))))).
fof(axFinancialLem131, axiom,
( ! [Var_BANK] :
((hasType(type_FinancialOrganization, Var_BANK) & hasType(type_CognitiveAgent, Var_BANK)) =>
(( ! [Var_AGENT] :
(hasType(type_CognitiveAgent, Var_AGENT) =>
(( ! [Var_ACCOUNT] :
(hasType(type_FinancialAccount, Var_ACCOUNT) =>
(((((f_accountHolder(Var_ACCOUNT,Var_AGENT)) & (f_accountAt(Var_ACCOUNT,Var_BANK)))) => (f_customer(Var_AGENT,Var_BANK))))))))))))).
fof(axFinancialLem132, axiom,
( ! [Var_ORG] :
(hasType(type_Organization, Var_ORG) =>
(( ! [Var_PERSON2] :
((hasType(type_CognitiveAgent, Var_PERSON2) & hasType(type_Entity, Var_PERSON2)) =>
(( ! [Var_PERSON1] :
((hasType(type_CognitiveAgent, Var_PERSON1) & hasType(type_Agent, Var_PERSON1)) =>
(((f_customerRepresentative(Var_PERSON1,Var_PERSON2,Var_ORG)) <=> (( ? [Var_SERVICE] :
(hasType(type_FinancialTransaction, Var_SERVICE) &
(((f_employs(Var_ORG,Var_PERSON1)) & (((f_agent(Var_SERVICE,Var_PERSON1)) & (f_destination(Var_SERVICE,Var_PERSON2)))))))))))))))))))).
fof(axFinancialLem133, axiom,
( ! [Var_SLOT] :
(hasType(type_ATMSlot, Var_SLOT) =>
(( ? [Var_ATM] :
(hasType(type_ATMMachine, Var_ATM) &
(f_hole(Var_SLOT,Var_ATM)))))))).
fof(axFinancialLem134, axiom,
( ! [Var_SLOT] :
(hasType(type_ATMSlot, Var_SLOT) =>
(( ? [Var_INSERT] :
(hasType(type_Putting, Var_INSERT) &
(( ? [Var_CARD] :
(hasType(type_BankCard, Var_CARD) &
(((f_patient(Var_INSERT,Var_CARD)) & (f_destination(Var_INSERT,Var_SLOT))))))))))))).
fof(axFinancialLem135, axiom,
( ! [Var_FAX] :
(hasType(type_Fax, Var_FAX) =>
(( ? [Var_FAXMACHINE] :
(hasType(type_FaxMachine, Var_FAXMACHINE) &
(f_instrument(Var_FAX,Var_FAXMACHINE)))))))).
fof(axFinancialLem136, axiom,
( ! [Var_AMOUNT1] :
(hasType(type_Quantity, Var_AMOUNT1) =>
(( ! [Var_DAY] :
(hasType(type_Day, Var_DAY) =>
(( ! [Var_AMOUNT] :
(hasType(type_CurrencyMeasure, Var_AMOUNT) =>
(( ! [Var_ACCOUNT] :
(hasType(type_FinancialAccount, Var_ACCOUNT) =>
(((( ? [Var_TRANSACTION] :
(hasType(type_FinancialTransaction, Var_TRANSACTION) &
(((f_origin(Var_TRANSACTION,f_CurrencyFn(Var_ACCOUNT))) & (((f_transactionAmount(Var_TRANSACTION,Var_AMOUNT)) & (f_date(Var_TRANSACTION,Var_DAY))))))))) => (( ? [Var_AMOUNT2] :
((hasType(type_CurrencyMeasure, Var_AMOUNT2) & hasType(type_Quantity, Var_AMOUNT2)) &
(((f_availableBalance(Var_ACCOUNT,Var_DAY,Var_AMOUNT2)) & (f_greaterThanOrEqualTo(Var_AMOUNT1,Var_AMOUNT2))))))))))))))))))))).
fof(axFinancialLem137, axiom,
( ! [Var_CASH] :
(hasType(type_Cash, Var_CASH) =>
(( ! [Var_AMOUNT1] :
(hasType(type_Quantity, Var_AMOUNT1) =>
(( ! [Var_DAY] :
(hasType(type_Day, Var_DAY) =>
(( ! [Var_AMOUNT] :
(hasType(type_CurrencyMeasure, Var_AMOUNT) =>
(( ! [Var_ACCOUNT] :
(hasType(type_FinancialAccount, Var_ACCOUNT) =>
(((( ? [Var_TRANSACTION] :
(hasType(type_FinancialTransaction, Var_TRANSACTION) &
(((f_origin(Var_TRANSACTION,f_CurrencyFn(Var_ACCOUNT))) & (((f_transactionAmount(Var_TRANSACTION,Var_AMOUNT)) & (((f_instrument(Var_TRANSACTION,Var_CASH)) & (f_date(Var_TRANSACTION,Var_DAY))))))))))) => (( ? [Var_AMOUNT2] :
((hasType(type_CurrencyMeasure, Var_AMOUNT2) & hasType(type_Quantity, Var_AMOUNT2)) &
(((f_availableCash(Var_ACCOUNT,Var_DAY,Var_AMOUNT2)) & (f_greaterThanOrEqualTo(Var_AMOUNT1,Var_AMOUNT2)))))))))))))))))))))))).
fof(axFinancialLem138, axiom,
( ! [Var_STATEMENT] :
(hasType(type_BankStatement, Var_STATEMENT) =>
(( ! [Var_ACCOUNT] :
(hasType(type_FinancialAccount, Var_ACCOUNT) =>
(((f_statementAccount(Var_STATEMENT,Var_ACCOUNT)) => (( ? [Var_TRANSACTION] :
(hasType(type_FinancialTransaction, Var_TRANSACTION) &
(((((f_origin(Var_TRANSACTION,f_CurrencyFn(Var_ACCOUNT))) | (f_destination(Var_TRANSACTION,f_CurrencyFn(Var_ACCOUNT))))) & (f_realization(Var_STATEMENT,Var_TRANSACTION))))))))))))))).
fof(axFinancialLem139, axiom,
( ! [Var_TRANSACTION1] :
(hasType(type_FinancialTransaction, Var_TRANSACTION1) =>
(( ! [Var_TRANSACTION2] :
(hasType(type_FinancialTransaction, Var_TRANSACTION2) =>
(( ! [Var_STATEMENT] :
((hasType(type_BankStatement, Var_STATEMENT) & hasType(type_Process, Var_STATEMENT)) =>
(( ! [Var_ACCOUNT] :
(hasType(type_FinancialAccount, Var_ACCOUNT) =>
(((((f_lastStatement(Var_ACCOUNT,Var_STATEMENT)) & (((( ~ (f_realization(Var_STATEMENT,Var_TRANSACTION1)))) & (f_realization(Var_STATEMENT,Var_TRANSACTION2)))))) => (f_earlier(f_WhenFn(Var_TRANSACTION2),f_WhenFn(Var_TRANSACTION1))))))))))))))))).
fof(axFinancialLem140, axiom,
( ! [Var_LOAN] :
(hasType(type_Loan, Var_LOAN) =>
(( ! [Var_AMOUNT] :
((hasType(type_Interest, Var_AMOUNT) & hasType(type_CurrencyMeasure, Var_AMOUNT)) =>
(((( ? [Var_PERIOD] :
(hasType(type_TimeInterval, Var_PERIOD) &
(((f_agreementPeriod(Var_LOAN,Var_PERIOD)) & (f_interestEarned(Var_LOAN,Var_AMOUNT,Var_PERIOD))))))) <=> (f_loanInterest(Var_LOAN,Var_AMOUNT)))))))))).
fof(axFinancialLem141, axiom,
( ! [Var_DATE] :
(hasType(type_Day, Var_DATE) =>
(( ! [Var_STATEMENT] :
((hasType(type_BankStatement, Var_STATEMENT) & hasType(type_Proposition, Var_STATEMENT)) =>
(((f_dateOfStatement(Var_STATEMENT,Var_DATE)) => (( ? [Var_COPY] :
((hasType(type_ContentBearingPhysical, Var_COPY) & hasType(type_Physical, Var_COPY)) &
(((f_containsInformation(Var_COPY,Var_STATEMENT)) & (f_date(Var_COPY,Var_DATE))))))))))))))).
fof(axFinancialLem142, axiom,
( ! [Var_DATE] :
(hasType(type_Day, Var_DATE) =>
(( ! [Var_BALANCE] :
(hasType(type_CurrencyMeasure, Var_BALANCE) =>
(( ! [Var_ACCOUNT] :
(hasType(type_FinancialAccount, Var_ACCOUNT) =>
(((f_lastStatementBalance(Var_ACCOUNT,Var_BALANCE)) => (( ? [Var_STATEMENT] :
(hasType(type_BankStatement, Var_STATEMENT) &
(((f_lastStatement(Var_ACCOUNT,Var_STATEMENT)) & (((f_dateOfStatement(Var_STATEMENT,Var_DATE)) & (f_currentAccountBalance(Var_ACCOUNT,Var_DATE,Var_ACCOUNT)))))))))))))))))))).
fof(axFinancialLem143, axiom,
( ! [Var_DURATION] :
((hasType(type_TimeDuration, Var_DURATION) & hasType(type_Entity, Var_DURATION)) =>
(( ! [Var_PERIOD] :
(hasType(type_TimeInterval, Var_PERIOD) =>
(( ! [Var_STATEMENT] :
(hasType(type_BankStatement, Var_STATEMENT) =>
(((((f_statementPeriod(Var_STATEMENT,Var_PERIOD)) & (f_duration(Var_PERIOD,Var_DURATION)))) => (Var_DURATION = inst_MonthDuration)))))))))))).
fof(axFinancialLem144, axiom,
( ! [Var_DATE] :
((hasType(type_Day, Var_DATE) & hasType(type_TimeInterval, Var_DATE)) =>
(( ! [Var_PERIOD] :
(hasType(type_TimeInterval, Var_PERIOD) =>
(( ! [Var_STATEMENT] :
(hasType(type_BankStatement, Var_STATEMENT) =>
(((((f_statementPeriod(Var_STATEMENT,Var_PERIOD)) & (f_dateOfStatement(Var_STATEMENT,Var_DATE)))) => (f_finishes(Var_DATE,Var_PERIOD))))))))))))).
fof(axFinancialLem145, axiom,
( ! [Var_ACCOUNT] :
(hasType(type_FinancialAccount, Var_ACCOUNT) =>
(( ! [Var_PERIOD] :
(hasType(type_TimeInterval, Var_PERIOD) =>
(( ! [Var_INTEREST] :
(hasType(type_CurrencyMeasure, Var_INTEREST) =>
(( ! [Var_STATEMENT] :
(hasType(type_BankStatement, Var_STATEMENT) =>
(((((f_statementInterest(Var_STATEMENT,Var_INTEREST)) & (((f_statementPeriod(Var_STATEMENT,Var_PERIOD)) & (f_statementAccount(Var_STATEMENT,Var_ACCOUNT)))))) => (( ? [Var_AMOUNT] :
(hasType(type_Interest, Var_AMOUNT) &
(f_interestEarned(Var_ACCOUNT,Var_AMOUNT,Var_PERIOD))))))))))))))))))).
fof(axFinancialLem146, axiom,
( ! [Var_TRANSFER] :
(hasType(type_ExternalTransfer, Var_TRANSFER) =>
(( ! [Var_ORGANIZATION1] :
(hasType(type_FinancialOrganization, Var_ORGANIZATION1) =>
(( ! [Var_ORGANIZATION2] :
(hasType(type_FinancialOrganization, Var_ORGANIZATION2) =>
(((((f_origin(Var_TRANSFER,Var_ORGANIZATION1)) & (f_destination(Var_TRANSFER,Var_ORGANIZATION2)))) => (Var_ORGANIZATION1 != Var_ORGANIZATION2)))))))))))).
fof(axFinancialLem147, axiom,
( ! [Var_TRANSFER] :
(hasType(type_ExternalTransfer, Var_TRANSFER) =>
(( ! [Var_ORGANIZATION1] :
(hasType(type_FinancialOrganization, Var_ORGANIZATION1) =>
(( ! [Var_ORGANIZATION2] :
(hasType(type_FinancialOrganization, Var_ORGANIZATION2) =>
(( ! [Var_ORGANIZATION2] :
(hasType(type_Entity, Var_ORGANIZATION2) =>
(((((f_origin(Var_TRANSFER,Var_ORGANIZATION1)) & (f_destination(Var_TRANSFER,Var_ORGANIZATION2)))) => (Var_ORGANIZATION1 = Var_ORGANIZATION2))))))))))))))).
fof(axFinancialLem148, axiom,
( ! [Var_PERIOD] :
(hasType(type_TimeInterval, Var_PERIOD) =>
(( ! [Var_AMOUNT] :
((hasType(type_CurrencyMeasure, Var_AMOUNT) & hasType(type_Interest, Var_AMOUNT)) =>
(( ! [Var_LOAN] :
((hasType(type_Loan, Var_LOAN) & hasType(type_Contract, Var_LOAN) & hasType(type_FinancialAccount, Var_LOAN)) =>
(((((f_loanFeeAmount(Var_LOAN,Var_AMOUNT)) & (f_agreementPeriod(Var_LOAN,Var_PERIOD)))) => (f_interestEarned(Var_LOAN,Var_AMOUNT,Var_PERIOD))))))))))))).