Added missing axiom in concrete PCR FibPrimes1

Author: josedusol

Diff for: AbstractModel/PCR_A/PCR_A.tla

@@ -244,7 +244,7 @@ A1step == INSTANCE PCR_A1step
 
 ============================================================================
 \* Modification History
-\* Last modified Thu Nov 18 21:10:43 UYT 2021 by josedu
+\* Last modified Thu Mar 03 01:13:02 UYT 2022 by josedu
 \* Last modified Thu Jul 08 02:51:43 GMT-03:00 2021 by JosEdu
 \* Last modified Fri Jul 17 16:28:02 UYT 2020 by josed
 \* Created Mon Jul 06 13:03:07 UYT 2020 by josed

Diff for: AbstractModel/PCR_A/PCR_A.toolbox/.project

@@ -20,6 +20,11 @@
 			<type>1</type>
 			<locationURI>PARENT-1-PROJECT_LOC/PCR_A.tla</locationURI>
 		</link>
+		<link>
+			<name>PCR_A2.tla</name>
+			<type>1</type>
+			<locationURI>PARENT-1-PROJECT_LOC/PCR_A2.tla</locationURI>
+		</link>
 		<link>
 			<name>PCR_A_Thms.tla</name>
 			<type>1</type>

Diff for: AbstractModel/PCR_A/PCR_A_Thms.tla

@@ -1734,6 +1734,6 @@ THEOREM Thm_Refinement == Spec => A1step!Spec
 
 =============================================================================
 \* Modification History
-\* Last modified Mon Dec 20 14:28:20 UYT 2021 by josedu
+\* Last modified Fri Mar 11 16:20:23 UYT 2022 by josedu
 \* Last modified Thu Jul 08 02:50:17 GMT-03:00 2021 by JosEdu
 \* Created Sat Jun 19 01:21:17 UYT 2021 by josedu

Diff for: Concrete/PCR_FibPrimes1/PCR_FibPrimes1.tla

@@ -70,6 +70,12 @@ INSTANCE PCR_A_Thms
 
 ----------------------------------------------------------------------------
 
+(* 
+  Basic functions are still assumed to be partial functions.
+*)
+
+AXIOM H_BFunType_FP1 == H_BFunType
+
 (* 
   Most axioms can be promoted to ordinary mathematical lemmas. 
   These are proved in module PCR_FibPrimes1_Lems.

Diff for: Concrete/PCR_FibPrimes1/PCR_FibPrimes1_Lems.tla

@@ -151,6 +151,6 @@ LEMMA Lem_Algebra
 
 ============================================================================
 \* Modification History
-\* Last modified Wed Sep 08 18:42:19 UYT 2021 by josedu
+\* Last modified Fri Mar 11 19:23:59 UYT 2022 by josedu
 \* Last modified Tue Jul 06 15:39:14 GMT-03:00 2021 by JosEdu
 \* Created Mon Jul 05 18:48:36 GMT-03:00 2021 by JosEdu

Diff for: Concrete/PCR_FibPrimes1/PCR_FibPrimes1_Thms.tla

@@ -2,7 +2,20 @@
 
 EXTENDS PCR_FibPrimes1, PCR_FibPrimes1_Lems
 
-USE DEF Index, Assig, Lem_Algebra, Lem_Type, Lem_BFunWD, Lem_fpRelevance
+USE DEF Index, Assig, Lem_Algebra, Lem_Type, Lem_BFunWD, 
+        Lem_fpRelevance, Lem_fcRelevance, Lem_frRelevance
+
+THEOREM Thm_IndexInv_FP1 == Spec => []IndexInv
+  BY Thm_IndexInv, H_Type, H_BFunType_FP1, H_BFunWD, H_Algebra,
+     H_fpRelevance, H_fcRelevance, H_frRelevance, PTL
+     
+THEOREM Thm_TypeInv_FP1 == Spec => []TypeInv
+  BY Thm_TypeInv, H_Type, H_BFunType_FP1, H_BFunWD, H_Algebra,
+     H_fpRelevance, H_fcRelevance, H_frRelevance, PTL
+     
+THEOREM Thm_PInv_FP1 == Spec => []PInv
+  BY Thm_PInv, H_Type, H_BFunType_FP1, H_BFunWD, H_Algebra,
+     H_fpRelevance, H_fcRelevance, H_frRelevance, PTL           
 
 THEOREM Thm_ProdEqInv == Spec => []ProdEqInv
 <1> DEFINE x == X[I0]
@@ -15,7 +28,7 @@ THEOREM Thm_ProdEqInv == Spec => []ProdEqInv
                  PROVE  FALSE
     BY DEF ProdEqInv
   <2>1. /\ I0    \in Seq(Nat) 
-        /\ x     \in Nat        
+        /\ x     \in Nat      
         /\ It(x) \subseteq Nat
         /\ i     \in Nat 
     BY <2>0, Lem_Type DEF Init, It, deps, T 
@@ -165,10 +178,10 @@ THEOREM Thm_ProdEqInv == Spec => []ProdEqInv
   <2> QED
     BY <2>0, <2>A, <2>B, <2>C DEF Next            
 <1> QED      
-  BY <1>1, <1>2, Thm_IndexInv, Thm_TypeInv, Thm_PInv, PTL DEF Spec 
+  BY <1>1, <1>2, Thm_IndexInv_FP1, Thm_TypeInv_FP1, Thm_PInv_FP1, PTL DEF Spec 
 
 ============================================================================
 \* Modification History
-\* Last modified Wed Sep 08 18:40:20 UYT 2021 by josedu
+\* Last modified Fri Mar 11 19:20:27 UYT 2022 by josedu
 \* Last modified Wed Jul 07 17:17:17 GMT-03:00 2021 by JosEdu
 \* Created Sun Jul 04 20:40:25 GMT-03:00 2021 by JosEdu