1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
|
% This is an initial Test Comment
fof ( typeDef_FunctionType , axiom , ! [ A ] : ( t_FunctionType ( A ) <=> ( object ( A ) & ( ( e_Root_FunctionType ( A ) & ( ~ e_Intermediate_FunctionType ( A ) & ~ e_Leaf_FunctionType ( A ) ) ) | ( ( ~ e_Root_FunctionType ( A ) & ( e_Intermediate_FunctionType ( A ) & ~ e_Leaf_FunctionType ( A ) ) ) | ( ~ e_Root_FunctionType ( A ) & ( ~ e_Intermediate_FunctionType ( A ) & e_Leaf_FunctionType ( A ) ) ) ) ) ) ) ) .
fof ( enumScope_FunctionType_Root , axiom , ! [ A ] : ( A = eo1 <=> e_Root_FunctionType ( A ) ) ) .
fof ( enumScope_FunctionType_Intermediate , axiom , ! [ A ] : ( A = eo2 <=> e_Intermediate_FunctionType ( A ) ) ) .
fof ( enumScope_FunctionType_Leaf , axiom , ! [ A ] : ( A = eo3 <=> e_Leaf_FunctionType ( A ) ) ) .
fof ( notObjectHandler , axiom , ! [ A ] : ( ~ object ( A ) <=> ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalData ( A ) & ~ t_FunctionType ( A ) ) ) ) ) ) ) ) ) ) ) ) .
fof ( inheritanceHierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionalInterface ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalArchitectureModel ( A ) & ( t_FunctionalInput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( t_FunctionalData ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionalInterface ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ( t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionalInterface ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_Function ( A ) & ( t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionalInterface ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionalInterface ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( t_FunctionalOutput ( A ) & ( t_FunctionalData ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionalInterface ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalData ( A ) & ( t_InformationLink ( A ) & ~ t_FunctionalInterface ( A ) ) ) ) ) ) ) ) ) ) | ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_InformationLink ( A ) & t_FunctionalInterface ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
fof ( typeScope_min_object , axiom , ! [ A ] : ( ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | ( A = eo1 | ( A = eo2 | A = eo3 ) ) ) ) ) ) => object ( A ) ) ) .
fof ( typeScope_max_object , axiom , ! [ A ] : ( object ( A ) => ( A = eo1 | ( A = eo2 | ( A = eo3 | ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | A = o5 ) ) ) ) ) ) ) ) ) .
fof ( typeScope_min_t_Function , axiom , ! [ A ] : ( A = o2 => ( t_Function ( A ) & object ( A ) ) ) ) .
fof ( typeScope_min_t_FunctionalOutput , axiom , ! [ A ] : ( ( A = o3 | ( A = o4 | A = o5 ) ) => ( t_FunctionalOutput ( A ) & object ( A ) ) ) ) .
fof ( typeScope_min_t_FunctionalInterface , axiom , ! [ A ] : ( ( A = o6 | A = o7 ) => ( t_FunctionalInterface ( A ) & object ( A ) ) ) ) .
fof ( typeScope_max_t_Function , axiom , ! [ A ] : ( ( t_Function ( A ) & object ( A ) ) => A = o2 ) ) .
fof ( typeScope_max_t_FunctionalOutput , axiom , ! [ A ] : ( ( t_FunctionalOutput ( A ) & object ( A ) ) => ( A = o3 | ( A = o4 | A = o5 ) ) ) ) .
fof ( t_uniqueness_eo1 , axiom , eo1 != eo2 & ( eo1 != eo3 & ( eo1 != o1 & ( eo1 != o2 & ( eo1 != o3 & ( eo1 != o4 & eo1 != o5 ) ) ) ) ) ) .
fof ( t_uniqueness_eo2 , axiom , eo2 != eo3 & ( eo2 != o1 & ( eo2 != o2 & ( eo2 != o3 & ( eo2 != o4 & eo2 != o5 ) ) ) ) ) .
fof ( t_uniqueness_eo3 , axiom , eo3 != o1 & ( eo3 != o2 & ( eo3 != o3 & ( eo3 != o4 & eo3 != o5 ) ) ) ) .
fof ( t_uniqueness_o1 , axiom , o1 != o2 & ( o1 != o3 & ( o1 != o4 & o1 != o5 ) ) ) .
fof ( t_uniqueness_o2 , axiom , o2 != o3 & ( o2 != o4 & o2 != o5 ) ) .
fof ( t_uniqueness_o3 , axiom , o3 != o4 & o3 != o5 ) .
fof ( t_uniqueness_o4 , axiom , o4 != o5 ) .
fof ( compliance_interface_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_interface_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) .
fof ( compliance_model_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_model_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalArchitectureModel ( V_1 ) ) ) ) .
fof ( compliance_parent_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_parent_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_Function ( V_1 ) ) ) ) .
fof ( compliance_rootElements_FunctionalArchitectureModel , axiom , ! [ V_0 , V_1 ] : ( r_rootElements_FunctionalArchitectureModel ( V_0 , V_1 ) => ( t_FunctionalArchitectureModel ( V_0 ) & t_FunctionalElement ( V_1 ) ) ) ) .
fof ( compliance_subElements_Function , axiom , ! [ V_0 , V_1 ] : ( r_subElements_Function ( V_0 , V_1 ) => ( t_Function ( V_0 ) & t_FunctionalElement ( V_1 ) ) ) ) .
fof ( compliance_data_FAMTerminator , axiom , ! [ V_0 , V_1 ] : ( r_data_FAMTerminator ( V_0 , V_1 ) => ( t_FAMTerminator ( V_0 ) & t_FunctionalData ( V_1 ) ) ) ) .
fof ( compliance_from_InformationLink , axiom , ! [ V_0 , V_1 ] : ( r_from_InformationLink ( V_0 , V_1 ) => ( t_InformationLink ( V_0 ) & t_FunctionalOutput ( V_1 ) ) ) ) .
fof ( compliance_to_InformationLink , axiom , ! [ V_0 , V_1 ] : ( r_to_InformationLink ( V_0 , V_1 ) => ( t_InformationLink ( V_0 ) & t_FunctionalInput ( V_1 ) ) ) ) .
fof ( compliance_data_FunctionalInterface , axiom , ! [ V_0 , V_1 ] : ( r_data_FunctionalInterface ( V_0 , V_1 ) => ( t_FunctionalInterface ( V_0 ) & t_FunctionalData ( V_1 ) ) ) ) .
fof ( compliance_element_FunctionalInterface , axiom , ! [ V_0 , V_1 ] : ( r_element_FunctionalInterface ( V_0 , V_1 ) => ( t_FunctionalInterface ( V_0 ) & t_FunctionalElement ( V_1 ) ) ) ) .
fof ( compliance_IncomingLinks_FunctionalInput , axiom , ! [ V_0 , V_1 ] : ( r_IncomingLinks_FunctionalInput ( V_0 , V_1 ) => ( t_FunctionalInput ( V_0 ) & t_InformationLink ( V_1 ) ) ) ) .
fof ( compliance_outgoingLinks_FunctionalOutput , axiom , ! [ V_0 , V_1 ] : ( r_outgoingLinks_FunctionalOutput ( V_0 , V_1 ) => ( t_FunctionalOutput ( V_0 ) & t_InformationLink ( V_1 ) ) ) ) .
fof ( compliance_terminator_FunctionalData , axiom , ! [ V_0 , V_1 ] : ( r_terminator_FunctionalData ( V_0 , V_1 ) => ( t_FunctionalData ( V_0 ) & t_FAMTerminator ( V_1 ) ) ) ) .
fof ( compliance_interface_FunctionalData , axiom , ! [ V_0 , V_1 ] : ( r_interface_FunctionalData ( V_0 , V_1 ) => ( t_FunctionalData ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) .
fof ( compliance_type_Function , axiom , ! [ V_0 , V_1 ] : ( r_type_Function ( V_0 , V_1 ) => ( t_Function ( V_0 ) & t_FunctionType ( V_1 ) ) ) ) .
fof ( containment_topLevel_t_FunctionalArchitectureModel , axiom , ! [ A ] : ( t_FunctionalArchitectureModel ( A ) <=> A = o1 ) ) .
fof ( containment_noDup_r_interface_FunctionalElement , axiom , ? [ A , B ] : ( r_interface_FunctionalElement ( A , B ) => ~ ? [ C , B ] : r_interface_FunctionalElement ( C , B ) ) ) .
fof ( containment_noDup_r_rootElements_FunctionalArchitectureModel , axiom , ? [ A , B ] : ( r_rootElements_FunctionalArchitectureModel ( A , B ) => ~ ? [ C , B ] : r_rootElements_FunctionalArchitectureModel ( C , B ) ) ) .
fof ( containment_noDup_r_subElements_Function , axiom , ? [ A , B ] : ( r_subElements_Function ( A , B ) => ~ ? [ C , B ] : r_subElements_Function ( C , B ) ) ) .
fof ( containment_noDup_r_data_FunctionalInterface , axiom , ? [ A , B ] : ( r_data_FunctionalInterface ( A , B ) => ~ ? [ C , B ] : r_data_FunctionalInterface ( C , B ) ) ) .
fof ( containment_noDup_r_outgoingLinks_FunctionalOutput , axiom , ? [ A , B ] : ( r_outgoingLinks_FunctionalOutput ( A , B ) => ~ ? [ C , B ] : r_outgoingLinks_FunctionalOutput ( C , B ) ) ) .
fof ( containment_noDup_r_terminator_FunctionalData , axiom , ? [ A , B ] : ( r_terminator_FunctionalData ( A , B ) => ~ ? [ C , B ] : r_terminator_FunctionalData ( C , B ) ) ) .
fof ( containment_t_FunctionalElement , axiom , ! [ A ] : ( t_FunctionalElement ( A ) => ? [ B ] : ( ( r_rootElements_FunctionalArchitectureModel ( B , A ) & ~ r_subElements_Function ( B , A ) ) | ( ~ r_rootElements_FunctionalArchitectureModel ( B , A ) & r_subElements_Function ( B , A ) ) ) ) ) .
fof ( containment_t_FunctionalData , axiom , ! [ A ] : ( t_FunctionalData ( A ) => ? [ B ] : r_data_FunctionalInterface ( B , A ) ) ) .
fof ( containment_t_InformationLink , axiom , ! [ A ] : ( t_InformationLink ( A ) => ? [ B ] : r_outgoingLinks_FunctionalOutput ( B , A ) ) ) .
fof ( containment_t_FunctionalInterface , axiom , ! [ A ] : ( t_FunctionalInterface ( A ) => ? [ B ] : r_interface_FunctionalElement ( B , A ) ) ) .
fof ( containment_t_FAMTerminator , axiom , ! [ A ] : ( t_FAMTerminator ( A ) => ? [ B ] : r_terminator_FunctionalData ( B , A ) ) ) .
fof ( containment_noCycle_1 , axiom , ~ ? [ V1 ] : ( r_interface_FunctionalElement ( V1 , V1 ) | ( r_rootElements_FunctionalArchitectureModel ( V1 , V1 ) | ( r_subElements_Function ( V1 , V1 ) | ( r_data_FunctionalInterface ( V1 , V1 ) | ( r_outgoingLinks_FunctionalOutput ( V1 , V1 ) | r_terminator_FunctionalData ( V1 , V1 ) ) ) ) ) ) ) .
fof ( containment_noCycle_2 , axiom , ~ ? [ V1 , V2 ] : ( ( r_interface_FunctionalElement ( V1 , V2 ) | ( r_rootElements_FunctionalArchitectureModel ( V1 , V2 ) | ( r_subElements_Function ( V1 , V2 ) | ( r_data_FunctionalInterface ( V1 , V2 ) | ( r_outgoingLinks_FunctionalOutput ( V1 , V2 ) | r_terminator_FunctionalData ( V1 , V2 ) ) ) ) ) ) & ( r_interface_FunctionalElement ( V2 , V1 ) | ( r_rootElements_FunctionalArchitectureModel ( V2 , V1 ) | ( r_subElements_Function ( V2 , V1 ) | ( r_data_FunctionalInterface ( V2 , V1 ) | ( r_outgoingLinks_FunctionalOutput ( V2 , V1 ) | r_terminator_FunctionalData ( V2 , V1 ) ) ) ) ) ) ) ) .
fof ( containment_noCycle_3 , axiom , ~ ? [ V1 , V2 , V3 ] : ( ( r_interface_FunctionalElement ( V1 , V2 ) | ( r_rootElements_FunctionalArchitectureModel ( V1 , V2 ) | ( r_subElements_Function ( V1 , V2 ) | ( r_data_FunctionalInterface ( V1 , V2 ) | ( r_outgoingLinks_FunctionalOutput ( V1 , V2 ) | r_terminator_FunctionalData ( V1 , V2 ) ) ) ) ) ) & ( ( r_interface_FunctionalElement ( V2 , V3 ) | ( r_rootElements_FunctionalArchitectureModel ( V2 , V3 ) | ( r_subElements_Function ( V2 , V3 ) | ( r_data_FunctionalInterface ( V2 , V3 ) | ( r_outgoingLinks_FunctionalOutput ( V2 , V3 ) | r_terminator_FunctionalData ( V2 , V3 ) ) ) ) ) ) & ( r_interface_FunctionalElement ( V3 , V1 ) | ( r_rootElements_FunctionalArchitectureModel ( V3 , V1 ) | ( r_subElements_Function ( V3 , V1 ) | ( r_data_FunctionalInterface ( V3 , V1 ) | ( r_outgoingLinks_FunctionalOutput ( V3 , V1 ) | r_terminator_FunctionalData ( V3 , V1 ) ) ) ) ) ) ) ) ) .
fof ( containment_noCycle_4 , axiom , ~ ? [ V1 , V2 , V3 , V4 ] : ( ( r_interface_FunctionalElement ( V1 , V2 ) | ( r_rootElements_FunctionalArchitectureModel ( V1 , V2 ) | ( r_subElements_Function ( V1 , V2 ) | ( r_data_FunctionalInterface ( V1 , V2 ) | ( r_outgoingLinks_FunctionalOutput ( V1 , V2 ) | r_terminator_FunctionalData ( V1 , V2 ) ) ) ) ) ) & ( ( r_interface_FunctionalElement ( V2 , V3 ) | ( r_rootElements_FunctionalArchitectureModel ( V2 , V3 ) | ( r_subElements_Function ( V2 , V3 ) | ( r_data_FunctionalInterface ( V2 , V3 ) | ( r_outgoingLinks_FunctionalOutput ( V2 , V3 ) | r_terminator_FunctionalData ( V2 , V3 ) ) ) ) ) ) & ( ( r_interface_FunctionalElement ( V3 , V4 ) | ( r_rootElements_FunctionalArchitectureModel ( V3 , V4 ) | ( r_subElements_Function ( V3 , V4 ) | ( r_data_FunctionalInterface ( V3 , V4 ) | ( r_outgoingLinks_FunctionalOutput ( V3 , V4 ) | r_terminator_FunctionalData ( V3 , V4 ) ) ) ) ) ) & ( r_interface_FunctionalElement ( V4 , V1 ) | ( r_rootElements_FunctionalArchitectureModel ( V4 , V1 ) | ( r_subElements_Function ( V4 , V1 ) | ( r_data_FunctionalInterface ( V4 , V1 ) | ( r_outgoingLinks_FunctionalOutput ( V4 , V1 ) | r_terminator_FunctionalData ( V4 , V1 ) ) ) ) ) ) ) ) ) ) .
fof ( containment_noCycle_5 , axiom , ~ ? [ V1 , V2 , V3 , V4 , V5 ] : ( ( r_interface_FunctionalElement ( V1 , V2 ) | ( r_rootElements_FunctionalArchitectureModel ( V1 , V2 ) | ( r_subElements_Function ( V1 , V2 ) | ( r_data_FunctionalInterface ( V1 , V2 ) | ( r_outgoingLinks_FunctionalOutput ( V1 , V2 ) | r_terminator_FunctionalData ( V1 , V2 ) ) ) ) ) ) & ( ( r_interface_FunctionalElement ( V2 , V3 ) | ( r_rootElements_FunctionalArchitectureModel ( V2 , V3 ) | ( r_subElements_Function ( V2 , V3 ) | ( r_data_FunctionalInterface ( V2 , V3 ) | ( r_outgoingLinks_FunctionalOutput ( V2 , V3 ) | r_terminator_FunctionalData ( V2 , V3 ) ) ) ) ) ) & ( ( r_interface_FunctionalElement ( V3 , V4 ) | ( r_rootElements_FunctionalArchitectureModel ( V3 , V4 ) | ( r_subElements_Function ( V3 , V4 ) | ( r_data_FunctionalInterface ( V3 , V4 ) | ( r_outgoingLinks_FunctionalOutput ( V3 , V4 ) | r_terminator_FunctionalData ( V3 , V4 ) ) ) ) ) ) & ( ( r_interface_FunctionalElement ( V4 , V5 ) | ( r_rootElements_FunctionalArchitectureModel ( V4 , V5 ) | ( r_subElements_Function ( V4 , V5 ) | ( r_data_FunctionalInterface ( V4 , V5 ) | ( r_outgoingLinks_FunctionalOutput ( V4 , V5 ) | r_terminator_FunctionalData ( V4 , V5 ) ) ) ) ) ) & ( r_interface_FunctionalElement ( V5 , V1 ) | ( r_rootElements_FunctionalArchitectureModel ( V5 , V1 ) | ( r_subElements_Function ( V5 , V1 ) | ( r_data_FunctionalInterface ( V5 , V1 ) | ( r_outgoingLinks_FunctionalOutput ( V5 , V1 ) | r_terminator_FunctionalData ( V5 , V1 ) ) ) ) ) ) ) ) ) ) ) .
fof ( upperMultiplicity_interface_FunctionalElement , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalElement ( V_src ) & ( t_FunctionalInterface ( V_trg_1 ) & t_FunctionalInterface ( V_trg_2 ) ) ) => ( ( r_interface_FunctionalElement ( V_src , V_trg_1 ) & r_interface_FunctionalElement ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) .
fof ( lowerMultiplicity_model_FunctionalElement , axiom , ! [ V_src ] : ( t_FunctionalElement ( V_src ) => ? [ V_trg_1 ] : ( t_FunctionalArchitectureModel ( V_trg_1 ) & r_model_FunctionalElement ( V_src , V_trg_1 ) ) ) ) .
fof ( upperMultiplicity_model_FunctionalElement , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalElement ( V_src ) & ( t_FunctionalArchitectureModel ( V_trg_1 ) & t_FunctionalArchitectureModel ( V_trg_2 ) ) ) => ( ( r_model_FunctionalElement ( V_src , V_trg_1 ) & r_model_FunctionalElement ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) .
fof ( upperMultiplicity_parent_FunctionalElement , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalElement ( V_src ) & ( t_Function ( V_trg_1 ) & t_Function ( V_trg_2 ) ) ) => ( ( r_parent_FunctionalElement ( V_src , V_trg_1 ) & r_parent_FunctionalElement ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) .
fof ( upperMultiplicity_data_FAMTerminator , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FAMTerminator ( V_src ) & ( t_FunctionalData ( V_trg_1 ) & t_FunctionalData ( V_trg_2 ) ) ) => ( ( r_data_FAMTerminator ( V_src , V_trg_1 ) & r_data_FAMTerminator ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) .
fof ( upperMultiplicity_from_InformationLink , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_InformationLink ( V_src ) & ( t_FunctionalOutput ( V_trg_1 ) & t_FunctionalOutput ( V_trg_2 ) ) ) => ( ( r_from_InformationLink ( V_src , V_trg_1 ) & r_from_InformationLink ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) .
fof ( lowerMultiplicity_to_InformationLink , axiom , ! [ V_src ] : ( t_InformationLink ( V_src ) => ? [ V_trg_1 ] : ( t_FunctionalInput ( V_trg_1 ) & r_to_InformationLink ( V_src , V_trg_1 ) ) ) ) .
fof ( upperMultiplicity_to_InformationLink , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_InformationLink ( V_src ) & ( t_FunctionalInput ( V_trg_1 ) & t_FunctionalInput ( V_trg_2 ) ) ) => ( ( r_to_InformationLink ( V_src , V_trg_1 ) & r_to_InformationLink ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) .
fof ( upperMultiplicity_element_FunctionalInterface , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalInterface ( V_src ) & ( t_FunctionalElement ( V_trg_1 ) & t_FunctionalElement ( V_trg_2 ) ) ) => ( ( r_element_FunctionalInterface ( V_src , V_trg_1 ) & r_element_FunctionalInterface ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) .
fof ( upperMultiplicity_terminator_FunctionalData , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalData ( V_src ) & ( t_FAMTerminator ( V_trg_1 ) & t_FAMTerminator ( V_trg_2 ) ) ) => ( ( r_terminator_FunctionalData ( V_src , V_trg_1 ) & r_terminator_FunctionalData ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) .
fof ( upperMultiplicity_interface_FunctionalData , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalData ( V_src ) & ( t_FunctionalInterface ( V_trg_1 ) & t_FunctionalInterface ( V_trg_2 ) ) ) => ( ( r_interface_FunctionalData ( V_src , V_trg_1 ) & r_interface_FunctionalData ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) .
fof ( oppositeReference_interface_FunctionalElement , axiom , ! [ V_src , V_trg ] : ( ( t_FunctionalElement ( V_src ) & t_FunctionalInterface ( V_trg ) ) => ( r_interface_FunctionalElement ( V_src , V_trg ) <=> r_element_FunctionalInterface ( V_trg , V_src ) ) ) ) .
fof ( oppositeReference_parent_FunctionalElement , axiom , ! [ V_src , V_trg ] : ( ( t_FunctionalElement ( V_src ) & t_Function ( V_trg ) ) => ( r_parent_FunctionalElement ( V_src , V_trg ) <=> r_subElements_Function ( V_trg , V_src ) ) ) ) .
fof ( oppositeReference_data_FAMTerminator , axiom , ! [ V_src , V_trg ] : ( ( t_FAMTerminator ( V_src ) & t_FunctionalData ( V_trg ) ) => ( r_data_FAMTerminator ( V_src , V_trg ) <=> r_terminator_FunctionalData ( V_trg , V_src ) ) ) ) .
fof ( oppositeReference_from_InformationLink , axiom , ! [ V_src , V_trg ] : ( ( t_InformationLink ( V_src ) & t_FunctionalOutput ( V_trg ) ) => ( r_from_InformationLink ( V_src , V_trg ) <=> r_outgoingLinks_FunctionalOutput ( V_trg , V_src ) ) ) ) .
fof ( oppositeReference_to_InformationLink , axiom , ! [ V_src , V_trg ] : ( ( t_InformationLink ( V_src ) & t_FunctionalInput ( V_trg ) ) => ( r_to_InformationLink ( V_src , V_trg ) <=> r_IncomingLinks_FunctionalInput ( V_trg , V_src ) ) ) ) .
fof ( oppositeReference_data_FunctionalInterface , axiom , ! [ V_src , V_trg ] : ( ( t_FunctionalInterface ( V_src ) & t_FunctionalData ( V_trg ) ) => ( r_data_FunctionalInterface ( V_src , V_trg ) <=> r_interface_FunctionalData ( V_trg , V_src ) ) ) ) .
fof ( lowerMultiplicity_type_Function , axiom , ! [ V_src ] : ( t_Function ( V_src ) => ? [ V_trg_1 ] : ( t_FunctionType ( V_trg_1 ) & r_type_Function ( V_src , V_trg_1 ) ) ) ) .
fof ( upperMultiplicity_type_Function , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_Function ( V_src ) & ( t_FunctionType ( V_trg_1 ) & t_FunctionType ( V_trg_2 ) ) ) => ( ( r_type_Function ( V_src , V_trg_1 ) & r_type_Function ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) .
|
