%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SWV437+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n029.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Wed Jul 20 23:04:32 EDT 2022 % Result : Theorem 4.12s 4.35s % Output : Proof 4.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : SWV437+1 : TPTP v8.1.0. Released v4.0.0. % 0.06/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n029.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Thu Jun 16 02:29:27 EDT 2022 % 0.12/0.33 % CPUTime : % 4.12/4.35 (* PROOF-FOUND *) % 4.12/4.35 % SZS status Theorem % 4.12/4.35 (* BEGIN-PROOF *) % 4.12/4.35 % SZS output start Proof % 4.12/4.35 Theorem alicereadsecret : (admin_indi_may_file (admin) (alice) (secretfile) (read)). % 4.12/4.35 Proof. % 4.12/4.35 assert (zenon_L1_ : (~(admin_indi_has_citizenship (admin) (alice) (usa))) -> False). % 4.12/4.35 do 0 intro. intros zenon_H58. % 4.12/4.35 generalize (ax23 (alice)). zenon_intro zenon_H59. % 4.12/4.35 generalize (zenon_H59 (usa)). zenon_intro zenon_H5a. % 4.12/4.35 apply (zenon_imply_s _ _ zenon_H5a); [ zenon_intro zenon_H5c | zenon_intro zenon_H5b ]. % 4.12/4.35 exact (zenon_H5c ax71). % 4.12/4.35 exact (zenon_H58 zenon_H5b). % 4.12/4.35 (* end of lemma zenon_L1_ *) % 4.12/4.35 assert (zenon_L2_ : (forall SSO : zenon_U, ((system_compartment_has_sso (system) (compartmentb) SSO)->(admin_compartment_has_sso (admin) (compartmentb) SSO))) -> (~(admin_compartment_has_sso (admin) (compartmentb) (sso_compartmentb))) -> False). % 4.12/4.35 do 0 intro. intros zenon_H5d zenon_H5e. % 4.12/4.35 generalize (zenon_H5d (sso_compartmentb)). zenon_intro zenon_H5f. % 4.12/4.35 apply (zenon_imply_s _ _ zenon_H5f); [ zenon_intro zenon_H61 | zenon_intro zenon_H60 ]. % 4.12/4.35 exact (zenon_H61 ax44). % 4.12/4.35 exact (zenon_H5e zenon_H60). % 4.12/4.35 (* end of lemma zenon_L2_ *) % 4.12/4.35 assert (zenon_L3_ : (forall SSO : zenon_U, ((system_compartment_has_sso (system) (compartmenta) SSO)->(admin_compartment_has_sso (admin) (compartmenta) SSO))) -> (~(admin_compartment_has_sso (admin) (compartmenta) (sso_compartmenta))) -> False). % 4.12/4.35 do 0 intro. intros zenon_H62 zenon_H63. % 4.12/4.35 generalize (zenon_H62 (sso_compartmenta)). zenon_intro zenon_H64. % 4.12/4.35 apply (zenon_imply_s _ _ zenon_H64); [ zenon_intro zenon_H66 | zenon_intro zenon_H65 ]. % 4.12/4.35 exact (zenon_H66 ax47). % 4.12/4.35 exact (zenon_H63 zenon_H65). % 4.12/4.35 (* end of lemma zenon_L3_ *) % 4.12/4.35 assert (zenon_L4_ : (forall CL : zenon_U, ((system_file_needs_compartments (system) (secretfile) CL)->((admin_file_has_compartments_h (admin) (secretfile) CL CL)->(admin_file_has_compartments (admin) (secretfile) CL)))) -> (~(admin_file_has_compartments (admin) (secretfile) (cons (compartmentb) (cons (compartmenta) (nil))))) -> False). % 4.12/4.35 do 0 intro. intros zenon_H67 zenon_H68. % 4.12/4.35 generalize (zenon_H67 (cons (compartmentb) (cons (compartmenta) (nil)))). zenon_intro zenon_H69. % 4.12/4.35 apply (zenon_imply_s _ _ zenon_H69); [ zenon_intro zenon_H6b | zenon_intro zenon_H6a ]. % 4.12/4.35 exact (zenon_H6b ax51). % 4.12/4.35 apply (zenon_imply_s _ _ zenon_H6a); [ zenon_intro zenon_H6d | zenon_intro zenon_H6c ]. % 4.12/4.35 generalize (ax10 (secretfile)). zenon_intro zenon_H6e. % 4.12/4.35 generalize (zenon_H6e (cons (compartmentb) (cons (compartmenta) (nil)))). zenon_intro zenon_H6f. % 4.12/4.35 generalize (zenon_H6f (compartmentb)). zenon_intro zenon_H70. % 4.12/4.35 generalize (zenon_H70 (cons (compartmenta) (nil))). zenon_intro zenon_H71. % 4.12/4.35 generalize (ax6 (compartmentb)). zenon_intro zenon_H5d. % 4.12/4.35 generalize (zenon_H71 (sso_compartmentb)). zenon_intro zenon_H72. % 4.12/4.35 apply (zenon_imply_s _ _ zenon_H72); [ zenon_intro zenon_H5e | zenon_intro zenon_H73 ]. % 4.12/4.35 apply (zenon_L2_); trivial. % 4.12/4.35 apply (zenon_imply_s _ _ zenon_H73); [ zenon_intro zenon_H75 | zenon_intro zenon_H74 ]. % 4.12/4.35 exact (zenon_H75 ax52). % 4.12/4.35 apply (zenon_imply_s _ _ zenon_H74); [ zenon_intro zenon_H77 | zenon_intro zenon_H76 ]. % 4.12/4.35 generalize (zenon_H6f (compartmenta)). zenon_intro zenon_H78. % 4.12/4.35 generalize (zenon_H78 (nil)). zenon_intro zenon_H79. % 4.12/4.35 generalize (ax6 (compartmenta)). zenon_intro zenon_H62. % 4.12/4.35 generalize (zenon_H79 (sso_compartmenta)). zenon_intro zenon_H7a. % 4.12/4.35 apply (zenon_imply_s _ _ zenon_H7a); [ zenon_intro zenon_H63 | zenon_intro zenon_H7b ]. % 4.12/4.35 apply (zenon_L3_); trivial. % 4.12/4.35 apply (zenon_imply_s _ _ zenon_H7b); [ zenon_intro zenon_H7d | zenon_intro zenon_H7c ]. % 4.12/4.35 exact (zenon_H7d ax53). % 4.12/4.35 apply (zenon_imply_s _ _ zenon_H7c); [ zenon_intro zenon_H7f | zenon_intro zenon_H7e ]. % 4.12/4.35 generalize (ax9 (secretfile)). zenon_intro zenon_H80. % 4.12/4.35 generalize (zenon_H80 (cons (compartmentb) (cons (compartmenta) (nil)))). zenon_intro zenon_H81. % 4.12/4.35 exact (zenon_H7f zenon_H81). % 4.12/4.35 exact (zenon_H77 zenon_H7e). % 4.12/4.35 exact (zenon_H6d zenon_H76). % 4.12/4.35 exact (zenon_H68 zenon_H6c). % 4.12/4.35 (* end of lemma zenon_L4_ *) % 4.12/4.35 assert (zenon_L5_ : (~(admin_compartment_has_scg (admin) (compartmentb) (scg_compartmentb))) -> (forall SSO : zenon_U, ((system_compartment_has_sso (system) (compartmentb) SSO)->(admin_compartment_has_sso (admin) (compartmentb) SSO))) -> False). % 4.12/4.36 do 0 intro. intros zenon_H82 zenon_H5d. % 4.12/4.36 generalize (ax7 (oca)). zenon_intro zenon_H83. % 4.12/4.36 generalize (zenon_H83 (compartmentb)). zenon_intro zenon_H84. % 4.12/4.36 generalize (zenon_H84 (sso_compartmentb)). zenon_intro zenon_H85. % 4.12/4.36 generalize (zenon_H85 (scg_compartmentb)). zenon_intro zenon_H86. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H86); [ zenon_intro zenon_H88 | zenon_intro zenon_H87 ]. % 4.12/4.36 exact (zenon_H88 ax41). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H87); [ zenon_intro zenon_H8a | zenon_intro zenon_H89 ]. % 4.12/4.36 exact (zenon_H8a ax45). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H89); [ zenon_intro zenon_H5e | zenon_intro zenon_H8b ]. % 4.12/4.36 apply (zenon_L2_); trivial. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H8b); [ zenon_intro zenon_H8d | zenon_intro zenon_H8c ]. % 4.12/4.36 exact (zenon_H8d ax46). % 4.12/4.36 exact (zenon_H82 zenon_H8c). % 4.12/4.36 (* end of lemma zenon_L5_ *) % 4.12/4.36 assert (zenon_L6_ : (~(admin_file_has_level_h (admin) (secretfile) (secret) (nil))) -> False). % 4.12/4.36 do 0 intro. intros zenon_H8e. % 4.12/4.36 generalize (ax12 (secretfile)). zenon_intro zenon_H8f. % 4.12/4.36 generalize (zenon_H8f (secret)). zenon_intro zenon_H90. % 4.12/4.36 exact (zenon_H8e zenon_H90). % 4.12/4.36 (* end of lemma zenon_L6_ *) % 4.12/4.36 assert (zenon_L7_ : (forall L : zenon_U, (forall CL : zenon_U, ((system_file_needs_level (system) (secretfile) L)->((admin_file_has_compartments (admin) (secretfile) CL)->((admin_file_has_level_h (admin) (secretfile) L CL)->(admin_file_has_level (admin) (secretfile) L)))))) -> (~(admin_file_has_level (admin) (secretfile) (secret))) -> (forall CL : zenon_U, ((system_file_needs_compartments (system) (secretfile) CL)->((admin_file_has_compartments_h (admin) (secretfile) CL CL)->(admin_file_has_compartments (admin) (secretfile) CL)))) -> False). % 4.12/4.36 do 0 intro. intros zenon_H91 zenon_H92 zenon_H67. % 4.12/4.36 generalize (zenon_H91 (secret)). zenon_intro zenon_H93. % 4.12/4.36 generalize (zenon_H93 (cons (compartmentb) (cons (compartmenta) (nil)))). zenon_intro zenon_H94. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H94); [ zenon_intro zenon_H96 | zenon_intro zenon_H95 ]. % 4.12/4.36 exact (zenon_H96 ax54). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H95); [ zenon_intro zenon_H68 | zenon_intro zenon_H97 ]. % 4.12/4.36 apply (zenon_L4_); trivial. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H97); [ zenon_intro zenon_H99 | zenon_intro zenon_H98 ]. % 4.12/4.36 generalize (ax13 (secretfile)). zenon_intro zenon_H9a. % 4.12/4.36 generalize (zenon_H9a (secret)). zenon_intro zenon_H9b. % 4.12/4.36 generalize (zenon_H9b (compartmentb)). zenon_intro zenon_H9c. % 4.12/4.36 generalize (zenon_H9c (cons (compartmenta) (nil))). zenon_intro zenon_H9d. % 4.12/4.36 generalize (ax6 (compartmentb)). zenon_intro zenon_H5d. % 4.12/4.36 generalize (zenon_H9d (sso_compartmentb)). zenon_intro zenon_H9e. % 4.12/4.36 generalize (zenon_H9e (scg_compartmentb)). zenon_intro zenon_H9f. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H9f); [ zenon_intro zenon_H5e | zenon_intro zenon_Ha0 ]. % 4.12/4.36 apply (zenon_L2_); trivial. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Ha0); [ zenon_intro zenon_H82 | zenon_intro zenon_Ha1 ]. % 4.12/4.36 apply (zenon_L5_); trivial. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Ha1); [ zenon_intro zenon_Ha3 | zenon_intro zenon_Ha2 ]. % 4.12/4.36 exact (zenon_Ha3 ax55). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Ha2); [ zenon_intro zenon_Ha5 | zenon_intro zenon_Ha4 ]. % 4.12/4.36 generalize (zenon_H9b (compartmenta)). zenon_intro zenon_Ha6. % 4.12/4.36 generalize (zenon_Ha6 (nil)). zenon_intro zenon_Ha7. % 4.12/4.36 generalize (ax7 (oca)). zenon_intro zenon_H83. % 4.12/4.36 generalize (ax6 (compartmenta)). zenon_intro zenon_H62. % 4.12/4.36 generalize (zenon_H83 (compartmenta)). zenon_intro zenon_Ha8. % 4.12/4.36 generalize (zenon_Ha7 (sso_compartmenta)). zenon_intro zenon_Ha9. % 4.12/4.36 generalize (zenon_H62 (sso_compartmenta)). zenon_intro zenon_H64. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H64); [ zenon_intro zenon_H66 | zenon_intro zenon_H65 ]. % 4.12/4.36 exact (zenon_H66 ax47). % 4.12/4.36 generalize (zenon_Ha9 (scg_compartmenta)). zenon_intro zenon_Haa. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Haa); [ zenon_intro zenon_H63 | zenon_intro zenon_Hab ]. % 4.12/4.36 exact (zenon_H63 zenon_H65). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Hab); [ zenon_intro zenon_Had | zenon_intro zenon_Hac ]. % 4.12/4.36 generalize (zenon_Ha8 (sso_compartmenta)). zenon_intro zenon_Hae. % 4.12/4.36 generalize (zenon_Hae (scg_compartmenta)). zenon_intro zenon_Haf. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Haf); [ zenon_intro zenon_H88 | zenon_intro zenon_Hb0 ]. % 4.12/4.36 exact (zenon_H88 ax41). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Hb0); [ zenon_intro zenon_Hb2 | zenon_intro zenon_Hb1 ]. % 4.12/4.36 exact (zenon_Hb2 ax48). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Hb1); [ zenon_intro zenon_H63 | zenon_intro zenon_Hb3 ]. % 4.12/4.36 exact (zenon_H63 zenon_H65). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Hb3); [ zenon_intro zenon_Hb5 | zenon_intro zenon_Hb4 ]. % 4.12/4.36 exact (zenon_Hb5 ax49). % 4.12/4.36 exact (zenon_Had zenon_Hb4). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Hac); [ zenon_intro zenon_Hb7 | zenon_intro zenon_Hb6 ]. % 4.12/4.36 exact (zenon_Hb7 ax56). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Hb6); [ zenon_intro zenon_H8e | zenon_intro zenon_Hb8 ]. % 4.12/4.36 apply (zenon_L6_); trivial. % 4.12/4.36 exact (zenon_Ha5 zenon_Hb8). % 4.12/4.36 exact (zenon_H99 zenon_Ha4). % 4.12/4.36 exact (zenon_H92 zenon_H98). % 4.12/4.36 (* end of lemma zenon_L7_ *) % 4.12/4.36 assert (zenon_L8_ : (~(loca_level_direct_below (admin) (secret) (topsecret))) -> False). % 4.12/4.36 do 0 intro. intros zenon_Hb9. % 4.12/4.36 generalize (ax3 (admin)). zenon_intro zenon_Hba. % 4.12/4.36 exact (zenon_Hb9 zenon_Hba). % 4.12/4.36 (* end of lemma zenon_L8_ *) % 4.12/4.36 assert (zenon_L9_ : (forall L : zenon_U, (loca_level_below (admin) L L)) -> (~(loca_level_below (admin) (secret) (secret))) -> False). % 4.12/4.36 do 0 intro. intros zenon_Hbb zenon_Hbc. % 4.12/4.36 generalize (zenon_Hbb (secret)). zenon_intro zenon_Hbd. % 4.12/4.36 exact (zenon_Hbc zenon_Hbd). % 4.12/4.36 (* end of lemma zenon_L9_ *) % 4.12/4.36 assert (zenon_L10_ : (forall L11 : zenon_U, ((loca_level_direct_below (admin) (secret) L11)->((loca_level_below (admin) (secret) (secret))->(loca_level_below (admin) (secret) L11)))) -> (forall L : zenon_U, (loca_level_below (admin) L L)) -> (~(loca_level_below (admin) (secret) (topsecret))) -> False). % 4.12/4.36 do 0 intro. intros zenon_Hbe zenon_Hbb zenon_Hbf. % 4.12/4.36 generalize (zenon_Hbe (topsecret)). zenon_intro zenon_Hc0. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Hc0); [ zenon_intro zenon_Hb9 | zenon_intro zenon_Hc1 ]. % 4.12/4.36 apply (zenon_L8_); trivial. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Hc1); [ zenon_intro zenon_Hbc | zenon_intro zenon_Hc2 ]. % 4.12/4.36 apply (zenon_L9_); trivial. % 4.12/4.36 exact (zenon_Hbf zenon_Hc2). % 4.12/4.36 (* end of lemma zenon_L10_ *) % 4.12/4.36 assert (zenon_L11_ : (forall L1 : zenon_U, ((system_indi_is_background_admin (system) (background_admin))->((background_admin_indi_has_background (background_admin) (alice) L1)->((loca_level_below (admin) (secret) L1)->(admin_indi_has_background (admin) (alice) (secret)))))) -> (~(admin_indi_has_background (admin) (alice) (secret))) -> False). % 4.12/4.36 do 0 intro. intros zenon_Hc3 zenon_Hc4. % 4.12/4.36 generalize (ax4 (admin)). zenon_intro zenon_Hbb. % 4.12/4.36 generalize (ax5 (admin)). zenon_intro zenon_Hc5. % 4.12/4.36 generalize (zenon_Hc5 (secret)). zenon_intro zenon_Hc6. % 4.12/4.36 generalize (zenon_Hc6 (secret)). zenon_intro zenon_Hbe. % 4.12/4.36 generalize (zenon_Hc3 (topsecret)). zenon_intro zenon_Hc7. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Hc7); [ zenon_intro zenon_Hc9 | zenon_intro zenon_Hc8 ]. % 4.12/4.36 exact (zenon_Hc9 ax68). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Hc8); [ zenon_intro zenon_Hcb | zenon_intro zenon_Hca ]. % 4.12/4.36 exact (zenon_Hcb ax74). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Hca); [ zenon_intro zenon_Hbf | zenon_intro zenon_Hcc ]. % 4.12/4.36 apply (zenon_L10_); trivial. % 4.12/4.36 exact (zenon_Hc4 zenon_Hcc). % 4.12/4.36 (* end of lemma zenon_L11_ *) % 4.12/4.36 assert (zenon_L12_ : (forall L : zenon_U, (forall BA : zenon_U, (forall L1 : zenon_U, ((system_indi_is_background_admin (system) BA)->((background_admin_indi_has_background BA (alice) L1)->((loca_level_below (admin) L L1)->(admin_indi_has_background (admin) (alice) L))))))) -> (~(admin_indi_has_background (admin) (alice) (secret))) -> False). % 4.12/4.36 do 0 intro. intros zenon_Hcd zenon_Hc4. % 4.12/4.36 generalize (zenon_Hcd (secret)). zenon_intro zenon_Hce. % 4.12/4.36 generalize (zenon_Hce (background_admin)). zenon_intro zenon_Hc3. % 4.12/4.36 apply (zenon_L11_); trivial. % 4.12/4.36 (* end of lemma zenon_L12_ *) % 4.12/4.36 assert (zenon_L13_ : (~(admin_indi_has_level_for_file (admin) (alice) (secretfile))) -> (admin_indi_has_credit (admin) (alice)) -> (admin_indi_has_employment (admin) (alice)) -> (admin_indi_has_polygraph (admin) (alice)) -> (forall CL : zenon_U, ((system_file_needs_compartments (system) (secretfile) CL)->((admin_file_has_compartments_h (admin) (secretfile) CL CL)->(admin_file_has_compartments (admin) (secretfile) CL)))) -> (forall L : zenon_U, (forall CL : zenon_U, ((system_file_needs_level (system) (secretfile) L)->((admin_file_has_compartments (admin) (secretfile) CL)->((admin_file_has_level_h (admin) (secretfile) L CL)->(admin_file_has_level (admin) (secretfile) L)))))) -> (forall L : zenon_U, ((admin_file_has_level (admin) (secretfile) L)->((admin_indi_has_level (admin) (alice) L)->(admin_indi_has_level_for_file (admin) (alice) (secretfile))))) -> (forall L : zenon_U, (forall L1 : zenon_U, (forall LA : zenon_U, (forall L11 : zenon_U, ((system_indi_needs_level (system) (alice) L1)->((admin_indi_has_citizenship (admin) (alice) (usa))->((admin_indi_has_polygraph (admin) (alice))->((admin_indi_has_employment (admin) (alice))->((admin_indi_has_credit (admin) (alice))->((loca_level_below (admin) L L1)->((system_indi_is_level_admin (system) LA)->((level_admin_indi_has_level LA (alice) L11)->((loca_level_below (admin) L L11)->((admin_indi_has_background (admin) (alice) L)->(admin_indi_has_level (admin) (alice) L))))))))))))))) -> False). % 4.12/4.36 do 0 intro. intros zenon_Hcf zenon_Hd0 zenon_Hd1 zenon_Hd2 zenon_H67 zenon_H91 zenon_Hd3 zenon_Hd4. % 4.12/4.36 generalize (ax20 (alice)). zenon_intro zenon_Hcd. % 4.12/4.36 generalize (zenon_Hd4 (secret)). zenon_intro zenon_Hd5. % 4.12/4.36 generalize (ax5 (admin)). zenon_intro zenon_Hc5. % 4.12/4.36 generalize (ax4 (admin)). zenon_intro zenon_Hbb. % 4.12/4.36 generalize (zenon_Hc5 (secret)). zenon_intro zenon_Hc6. % 4.12/4.36 generalize (zenon_Hd5 (secret)). zenon_intro zenon_Hd6. % 4.12/4.36 generalize (zenon_Hd6 (level_admin)). zenon_intro zenon_Hd7. % 4.12/4.36 generalize (zenon_Hbb (secret)). zenon_intro zenon_Hbd. % 4.12/4.36 generalize (zenon_Hc6 (secret)). zenon_intro zenon_Hbe. % 4.12/4.36 generalize (zenon_Hd3 (secret)). zenon_intro zenon_Hd8. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Hd8); [ zenon_intro zenon_H92 | zenon_intro zenon_Hd9 ]. % 4.12/4.36 apply (zenon_L7_); trivial. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Hd9); [ zenon_intro zenon_Hdb | zenon_intro zenon_Hda ]. % 4.12/4.36 generalize (zenon_Hd7 (topsecret)). zenon_intro zenon_Hdc. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Hdc); [ zenon_intro zenon_Hde | zenon_intro zenon_Hdd ]. % 4.12/4.36 exact (zenon_Hde ax76). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Hdd); [ zenon_intro zenon_H58 | zenon_intro zenon_Hdf ]. % 4.12/4.36 apply (zenon_L1_); trivial. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Hdf); [ zenon_intro zenon_He1 | zenon_intro zenon_He0 ]. % 4.12/4.36 exact (zenon_He1 zenon_Hd2). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_He0); [ zenon_intro zenon_He3 | zenon_intro zenon_He2 ]. % 4.12/4.36 exact (zenon_He3 zenon_Hd1). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_He2); [ zenon_intro zenon_He5 | zenon_intro zenon_He4 ]. % 4.12/4.36 exact (zenon_He5 zenon_Hd0). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_He4); [ zenon_intro zenon_Hbc | zenon_intro zenon_He6 ]. % 4.12/4.36 exact (zenon_Hbc zenon_Hbd). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_He6); [ zenon_intro zenon_He8 | zenon_intro zenon_He7 ]. % 4.12/4.36 exact (zenon_He8 ax70). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_He7); [ zenon_intro zenon_Hea | zenon_intro zenon_He9 ]. % 4.12/4.36 exact (zenon_Hea ax77). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_He9); [ zenon_intro zenon_Hbf | zenon_intro zenon_Heb ]. % 4.12/4.36 apply (zenon_L10_); trivial. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Heb); [ zenon_intro zenon_Hc4 | zenon_intro zenon_Hec ]. % 4.12/4.36 apply (zenon_L12_); trivial. % 4.12/4.36 exact (zenon_Hdb zenon_Hec). % 4.12/4.36 exact (zenon_Hcf zenon_Hda). % 4.12/4.36 (* end of lemma zenon_L13_ *) % 4.12/4.36 assert (zenon_L14_ : (forall PA : zenon_U, ((system_indi_is_polygraph_admin (system) PA)->((polygraph_admin_indi_has_polygraph PA (alice))->(admin_indi_has_polygraph (admin) (alice))))) -> (~(admin_indi_has_level_for_file (admin) (alice) (secretfile))) -> (admin_indi_has_credit (admin) (alice)) -> (admin_indi_has_employment (admin) (alice)) -> (forall CL : zenon_U, ((system_file_needs_compartments (system) (secretfile) CL)->((admin_file_has_compartments_h (admin) (secretfile) CL CL)->(admin_file_has_compartments (admin) (secretfile) CL)))) -> (forall L : zenon_U, (forall CL : zenon_U, ((system_file_needs_level (system) (secretfile) L)->((admin_file_has_compartments (admin) (secretfile) CL)->((admin_file_has_level_h (admin) (secretfile) L CL)->(admin_file_has_level (admin) (secretfile) L)))))) -> (forall L : zenon_U, ((admin_file_has_level (admin) (secretfile) L)->((admin_indi_has_level (admin) (alice) L)->(admin_indi_has_level_for_file (admin) (alice) (secretfile))))) -> (forall L : zenon_U, (forall L1 : zenon_U, (forall LA : zenon_U, (forall L11 : zenon_U, ((system_indi_needs_level (system) (alice) L1)->((admin_indi_has_citizenship (admin) (alice) (usa))->((admin_indi_has_polygraph (admin) (alice))->((admin_indi_has_employment (admin) (alice))->((admin_indi_has_credit (admin) (alice))->((loca_level_below (admin) L L1)->((system_indi_is_level_admin (system) LA)->((level_admin_indi_has_level LA (alice) L11)->((loca_level_below (admin) L L11)->((admin_indi_has_background (admin) (alice) L)->(admin_indi_has_level (admin) (alice) L))))))))))))))) -> False). % 4.12/4.36 do 0 intro. intros zenon_Hed zenon_Hcf zenon_Hd0 zenon_Hd1 zenon_H67 zenon_H91 zenon_Hd3 zenon_Hd4. % 4.12/4.36 generalize (zenon_Hed (polygraph_admin)). zenon_intro zenon_Hee. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Hee); [ zenon_intro zenon_Hf0 | zenon_intro zenon_Hef ]. % 4.12/4.36 exact (zenon_Hf0 ax66). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Hef); [ zenon_intro zenon_Hf1 | zenon_intro zenon_Hd2 ]. % 4.12/4.36 exact (zenon_Hf1 ax72). % 4.12/4.36 apply (zenon_L13_); trivial. % 4.12/4.36 (* end of lemma zenon_L14_ *) % 4.12/4.36 assert (zenon_L15_ : (forall CA : zenon_U, ((system_indi_is_credit_admin (system) CA)->((credit_admin_indi_has_credit CA (alice))->(admin_indi_has_credit (admin) (alice))))) -> (forall PA : zenon_U, ((system_indi_is_polygraph_admin (system) PA)->((polygraph_admin_indi_has_polygraph PA (alice))->(admin_indi_has_polygraph (admin) (alice))))) -> (~(admin_indi_has_level_for_file (admin) (alice) (secretfile))) -> (admin_indi_has_employment (admin) (alice)) -> (forall CL : zenon_U, ((system_file_needs_compartments (system) (secretfile) CL)->((admin_file_has_compartments_h (admin) (secretfile) CL CL)->(admin_file_has_compartments (admin) (secretfile) CL)))) -> (forall L : zenon_U, (forall CL : zenon_U, ((system_file_needs_level (system) (secretfile) L)->((admin_file_has_compartments (admin) (secretfile) CL)->((admin_file_has_level_h (admin) (secretfile) L CL)->(admin_file_has_level (admin) (secretfile) L)))))) -> (forall L : zenon_U, ((admin_file_has_level (admin) (secretfile) L)->((admin_indi_has_level (admin) (alice) L)->(admin_indi_has_level_for_file (admin) (alice) (secretfile))))) -> (forall L : zenon_U, (forall L1 : zenon_U, (forall LA : zenon_U, (forall L11 : zenon_U, ((system_indi_needs_level (system) (alice) L1)->((admin_indi_has_citizenship (admin) (alice) (usa))->((admin_indi_has_polygraph (admin) (alice))->((admin_indi_has_employment (admin) (alice))->((admin_indi_has_credit (admin) (alice))->((loca_level_below (admin) L L1)->((system_indi_is_level_admin (system) LA)->((level_admin_indi_has_level LA (alice) L11)->((loca_level_below (admin) L L11)->((admin_indi_has_background (admin) (alice) L)->(admin_indi_has_level (admin) (alice) L))))))))))))))) -> False). % 4.12/4.36 do 0 intro. intros zenon_Hf2 zenon_Hed zenon_Hcf zenon_Hd1 zenon_H67 zenon_H91 zenon_Hd3 zenon_Hd4. % 4.12/4.36 generalize (zenon_Hf2 (credit_admin)). zenon_intro zenon_Hf3. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Hf3); [ zenon_intro zenon_Hf5 | zenon_intro zenon_Hf4 ]. % 4.12/4.36 exact (zenon_Hf5 ax67). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Hf4); [ zenon_intro zenon_Hf6 | zenon_intro zenon_Hd0 ]. % 4.12/4.36 exact (zenon_Hf6 ax73). % 4.12/4.36 apply (zenon_L14_); trivial. % 4.12/4.36 (* end of lemma zenon_L15_ *) % 4.12/4.36 assert (zenon_L16_ : (~(admin_compartment_has_sso (admin) (compartmentb) (sso_compartmentb))) -> False). % 4.12/4.36 do 0 intro. intros zenon_H5e. % 4.12/4.36 generalize (ax6 (compartmentb)). zenon_intro zenon_H5d. % 4.12/4.36 apply (zenon_L2_); trivial. % 4.12/4.36 (* end of lemma zenon_L16_ *) % 4.12/4.36 assert (zenon_L17_ : (forall L2 : zenon_U, (forall B1 : zenon_U, (forall B2 : zenon_U, ((system_indi_is_oca (system) (oca))->((oca_compartment_is_compartment (oca) (compartmentb) (confidential) L2 B1 B2)->((admin_indi_has_background (admin) (alice) L2)->(admin_indi_has_background_for_compartment (admin) (alice) (compartmentb)))))))) -> (admin_indi_has_background (admin) (alice) (topsecret)) -> (~(admin_indi_has_background_for_compartment (admin) (alice) (compartmentb))) -> False). % 4.12/4.36 do 0 intro. intros zenon_Hf7 zenon_Hf8 zenon_Hf9. % 4.12/4.36 generalize (zenon_Hf7 (topsecret)). zenon_intro zenon_Hfa. % 4.12/4.36 generalize (zenon_Hfa (yes)). zenon_intro zenon_Hfb. % 4.12/4.36 generalize (zenon_Hfb (yes)). zenon_intro zenon_Hfc. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Hfc); [ zenon_intro zenon_H88 | zenon_intro zenon_Hfd ]. % 4.12/4.36 exact (zenon_H88 ax41). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Hfd); [ zenon_intro zenon_Hff | zenon_intro zenon_Hfe ]. % 4.12/4.36 exact (zenon_Hff ax42). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Hfe); [ zenon_intro zenon_H101 | zenon_intro zenon_H100 ]. % 4.12/4.36 exact (zenon_H101 zenon_Hf8). % 4.12/4.36 exact (zenon_Hf9 zenon_H100). % 4.12/4.36 (* end of lemma zenon_L17_ *) % 4.12/4.36 assert (zenon_L18_ : (~(loca_level_direct_below (admin) (confidential) (secret))) -> False). % 4.12/4.36 do 0 intro. intros zenon_H102. % 4.12/4.36 generalize (ax2 (admin)). zenon_intro zenon_H103. % 4.12/4.36 exact (zenon_H102 zenon_H103). % 4.12/4.36 (* end of lemma zenon_L18_ *) % 4.12/4.36 assert (zenon_L19_ : (forall L11 : zenon_U, ((loca_level_direct_below (admin) (confidential) L11)->((loca_level_below (admin) (confidential) (confidential))->(loca_level_below (admin) (confidential) L11)))) -> (loca_level_below (admin) (confidential) (confidential)) -> (~(loca_level_below (admin) (confidential) (secret))) -> False). % 4.12/4.36 do 0 intro. intros zenon_H104 zenon_H105 zenon_H106. % 4.12/4.36 generalize (zenon_H104 (secret)). zenon_intro zenon_H107. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H107); [ zenon_intro zenon_H102 | zenon_intro zenon_H108 ]. % 4.12/4.36 apply (zenon_L18_); trivial. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H108); [ zenon_intro zenon_H10a | zenon_intro zenon_H109 ]. % 4.12/4.36 exact (zenon_H10a zenon_H105). % 4.12/4.36 exact (zenon_H106 zenon_H109). % 4.12/4.36 (* end of lemma zenon_L19_ *) % 4.12/4.36 assert (zenon_L20_ : (forall L11 : zenon_U, ((loca_level_direct_below (admin) (secret) L11)->((loca_level_below (admin) (confidential) (secret))->(loca_level_below (admin) (confidential) L11)))) -> (forall L11 : zenon_U, ((loca_level_direct_below (admin) (confidential) L11)->((loca_level_below (admin) (confidential) (confidential))->(loca_level_below (admin) (confidential) L11)))) -> (loca_level_below (admin) (confidential) (confidential)) -> (~(loca_level_below (admin) (confidential) (topsecret))) -> False). % 4.12/4.36 do 0 intro. intros zenon_H10b zenon_H104 zenon_H105 zenon_H10c. % 4.12/4.36 generalize (zenon_H10b (topsecret)). zenon_intro zenon_H10d. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H10d); [ zenon_intro zenon_Hb9 | zenon_intro zenon_H10e ]. % 4.12/4.36 apply (zenon_L8_); trivial. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H10e); [ zenon_intro zenon_H106 | zenon_intro zenon_H10f ]. % 4.12/4.36 apply (zenon_L19_); trivial. % 4.12/4.36 exact (zenon_H10c zenon_H10f). % 4.12/4.36 (* end of lemma zenon_L20_ *) % 4.12/4.36 assert (zenon_L21_ : (loca_level_below (admin) (confidential) (confidential)) -> (~(loca_level_below (admin) (confidential) (topsecret))) -> (forall L1 : zenon_U, (forall L11 : zenon_U, ((loca_level_direct_below (admin) L1 L11)->((loca_level_below (admin) (confidential) L1)->(loca_level_below (admin) (confidential) L11))))) -> False). % 4.12/4.36 do 0 intro. intros zenon_H105 zenon_H10c zenon_H110. % 4.12/4.36 generalize (zenon_H110 (confidential)). zenon_intro zenon_H104. % 4.12/4.36 generalize (zenon_H110 (secret)). zenon_intro zenon_H10b. % 4.12/4.36 apply (zenon_L20_); trivial. % 4.12/4.36 (* end of lemma zenon_L21_ *) % 4.12/4.36 assert (zenon_L22_ : (forall L : zenon_U, (forall BA : zenon_U, (forall L1 : zenon_U, ((system_indi_is_background_admin (system) BA)->((background_admin_indi_has_background BA (alice) L1)->((loca_level_below (admin) L L1)->(admin_indi_has_background (admin) (alice) L))))))) -> (forall L : zenon_U, (loca_level_below (admin) L L)) -> (~(admin_indi_has_background (admin) (alice) (confidential))) -> False). % 4.12/4.36 do 0 intro. intros zenon_Hcd zenon_Hbb zenon_H111. % 4.12/4.36 generalize (zenon_Hcd (confidential)). zenon_intro zenon_H112. % 4.12/4.36 generalize (zenon_H112 (background_admin)). zenon_intro zenon_H113. % 4.12/4.36 generalize (ax5 (admin)). zenon_intro zenon_Hc5. % 4.12/4.36 generalize (zenon_Hc5 (confidential)). zenon_intro zenon_H110. % 4.12/4.36 generalize (zenon_Hbb (confidential)). zenon_intro zenon_H105. % 4.12/4.36 generalize (zenon_H110 (confidential)). zenon_intro zenon_H104. % 4.12/4.36 generalize (zenon_H110 (secret)). zenon_intro zenon_H10b. % 4.12/4.36 generalize (zenon_H113 (topsecret)). zenon_intro zenon_H114. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H114); [ zenon_intro zenon_Hc9 | zenon_intro zenon_H115 ]. % 4.12/4.36 exact (zenon_Hc9 ax68). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H115); [ zenon_intro zenon_Hcb | zenon_intro zenon_H116 ]. % 4.12/4.36 exact (zenon_Hcb ax74). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H116); [ zenon_intro zenon_H10c | zenon_intro zenon_H117 ]. % 4.12/4.36 apply (zenon_L20_); trivial. % 4.12/4.36 exact (zenon_H111 zenon_H117). % 4.12/4.36 (* end of lemma zenon_L22_ *) % 4.12/4.36 assert (zenon_L23_ : (~(loca_level_direct_below (admin) (sbu) (confidential))) -> False). % 4.12/4.36 do 0 intro. intros zenon_H118. % 4.12/4.36 generalize (ax1 (admin)). zenon_intro zenon_H119. % 4.12/4.36 exact (zenon_H118 zenon_H119). % 4.12/4.36 (* end of lemma zenon_L23_ *) % 4.12/4.36 assert (zenon_L24_ : (forall L11 : zenon_U, ((loca_level_direct_below (admin) (confidential) L11)->((loca_level_below (admin) (sbu) (confidential))->(loca_level_below (admin) (sbu) L11)))) -> (loca_level_direct_below (admin) (confidential) (secret)) -> (loca_level_below (admin) (sbu) (confidential)) -> (~(loca_level_below (admin) (sbu) (secret))) -> False). % 4.12/4.36 do 0 intro. intros zenon_H11a zenon_H103 zenon_H11b zenon_H11c. % 4.12/4.36 generalize (zenon_H11a (secret)). zenon_intro zenon_H11d. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H11d); [ zenon_intro zenon_H102 | zenon_intro zenon_H11e ]. % 4.12/4.36 exact (zenon_H102 zenon_H103). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H11e); [ zenon_intro zenon_H120 | zenon_intro zenon_H11f ]. % 4.12/4.36 exact (zenon_H120 zenon_H11b). % 4.12/4.36 exact (zenon_H11c zenon_H11f). % 4.12/4.36 (* end of lemma zenon_L24_ *) % 4.12/4.36 assert (zenon_L25_ : (loca_level_direct_below (admin) (secret) (topsecret)) -> (forall L11 : zenon_U, ((loca_level_direct_below (admin) (confidential) L11)->((loca_level_below (admin) (sbu) (confidential))->(loca_level_below (admin) (sbu) L11)))) -> (~(loca_level_below (admin) (sbu) (topsecret))) -> (forall L1 : zenon_U, (forall L11 : zenon_U, ((loca_level_direct_below (admin) L1 L11)->((loca_level_below (admin) (sbu) L1)->(loca_level_below (admin) (sbu) L11))))) -> (loca_level_below (admin) (sbu) (sbu)) -> (forall L11 : zenon_U, ((loca_level_direct_below (admin) (sbu) L11)->((loca_level_below (admin) (sbu) (sbu))->(loca_level_below (admin) (sbu) L11)))) -> False). % 4.12/4.36 do 0 intro. intros zenon_Hba zenon_H11a zenon_H121 zenon_H122 zenon_H123 zenon_H124. % 4.12/4.36 generalize (ax2 (admin)). zenon_intro zenon_H103. % 4.12/4.36 generalize (zenon_H124 (confidential)). zenon_intro zenon_H125. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H125); [ zenon_intro zenon_H118 | zenon_intro zenon_H126 ]. % 4.12/4.36 apply (zenon_L23_); trivial. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H126); [ zenon_intro zenon_H127 | zenon_intro zenon_H11b ]. % 4.12/4.36 exact (zenon_H127 zenon_H123). % 4.12/4.36 generalize (zenon_H122 (secret)). zenon_intro zenon_H128. % 4.12/4.36 generalize (zenon_H128 (topsecret)). zenon_intro zenon_H129. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H129); [ zenon_intro zenon_Hb9 | zenon_intro zenon_H12a ]. % 4.12/4.36 exact (zenon_Hb9 zenon_Hba). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H12a); [ zenon_intro zenon_H11c | zenon_intro zenon_H12b ]. % 4.12/4.36 apply (zenon_L24_); trivial. % 4.12/4.36 exact (zenon_H121 zenon_H12b). % 4.12/4.36 (* end of lemma zenon_L25_ *) % 4.12/4.36 assert (zenon_L26_ : (forall L11 : zenon_U, ((loca_level_direct_below (admin) (sbu) L11)->((loca_level_below (admin) (sbu) (sbu))->(loca_level_below (admin) (sbu) L11)))) -> (loca_level_below (admin) (sbu) (sbu)) -> (forall L1 : zenon_U, (forall L11 : zenon_U, ((loca_level_direct_below (admin) L1 L11)->((loca_level_below (admin) (sbu) L1)->(loca_level_below (admin) (sbu) L11))))) -> (~(loca_level_below (admin) (sbu) (topsecret))) -> (forall L11 : zenon_U, ((loca_level_direct_below (admin) (confidential) L11)->((loca_level_below (admin) (sbu) (confidential))->(loca_level_below (admin) (sbu) L11)))) -> False). % 4.12/4.36 do 0 intro. intros zenon_H124 zenon_H123 zenon_H122 zenon_H121 zenon_H11a. % 4.12/4.36 generalize (ax3 (admin)). zenon_intro zenon_Hba. % 4.12/4.36 apply (zenon_L25_); trivial. % 4.12/4.36 (* end of lemma zenon_L26_ *) % 4.12/4.36 assert (zenon_L27_ : (forall L : zenon_U, (forall BA : zenon_U, (forall L1 : zenon_U, ((system_indi_is_background_admin (system) BA)->((background_admin_indi_has_background BA (alice) L1)->((loca_level_below (admin) L L1)->(admin_indi_has_background (admin) (alice) L))))))) -> (~(admin_indi_has_background (admin) (alice) (sbu))) -> (forall L : zenon_U, (forall L1 : zenon_U, (forall L11 : zenon_U, ((loca_level_direct_below (admin) L1 L11)->((loca_level_below (admin) L L1)->(loca_level_below (admin) L L11)))))) -> False). % 4.12/4.36 do 0 intro. intros zenon_Hcd zenon_H12c zenon_Hc5. % 4.12/4.36 generalize (zenon_Hcd (sbu)). zenon_intro zenon_H12d. % 4.12/4.36 generalize (zenon_H12d (background_admin)). zenon_intro zenon_H12e. % 4.12/4.36 generalize (ax4 (admin)). zenon_intro zenon_Hbb. % 4.12/4.36 generalize (zenon_Hc5 (sbu)). zenon_intro zenon_H122. % 4.12/4.36 generalize (zenon_Hbb (sbu)). zenon_intro zenon_H123. % 4.12/4.36 generalize (zenon_H122 (sbu)). zenon_intro zenon_H124. % 4.12/4.36 generalize (zenon_H122 (confidential)). zenon_intro zenon_H11a. % 4.12/4.36 generalize (zenon_H12e (topsecret)). zenon_intro zenon_H12f. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H12f); [ zenon_intro zenon_Hc9 | zenon_intro zenon_H130 ]. % 4.12/4.36 exact (zenon_Hc9 ax68). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H130); [ zenon_intro zenon_Hcb | zenon_intro zenon_H131 ]. % 4.12/4.36 exact (zenon_Hcb ax74). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H131); [ zenon_intro zenon_H121 | zenon_intro zenon_H132 ]. % 4.12/4.36 apply (zenon_L26_); trivial. % 4.12/4.36 exact (zenon_H12c zenon_H132). % 4.12/4.36 (* end of lemma zenon_L27_ *) % 4.12/4.36 assert (zenon_L28_ : (forall L11 : zenon_U, ((system_indi_needs_level (system) (alice) (secret))->((admin_indi_has_citizenship (admin) (alice) (usa))->((admin_indi_has_polygraph (admin) (alice))->((admin_indi_has_employment (admin) (alice))->((admin_indi_has_credit (admin) (alice))->((loca_level_below (admin) (sbu) (secret))->((system_indi_is_level_admin (system) (level_admin))->((level_admin_indi_has_level (level_admin) (alice) L11)->((loca_level_below (admin) (sbu) L11)->((admin_indi_has_background (admin) (alice) (sbu))->(admin_indi_has_level (admin) (alice) (sbu))))))))))))) -> (admin_indi_has_polygraph (admin) (alice)) -> (admin_indi_has_employment (admin) (alice)) -> (admin_indi_has_credit (admin) (alice)) -> (forall L1 : zenon_U, (forall L11 : zenon_U, ((loca_level_direct_below (admin) L1 L11)->((loca_level_below (admin) (sbu) L1)->(loca_level_below (admin) (sbu) L11))))) -> (loca_level_below (admin) (sbu) (sbu)) -> (forall L11 : zenon_U, ((loca_level_direct_below (admin) (sbu) L11)->((loca_level_below (admin) (sbu) (sbu))->(loca_level_below (admin) (sbu) L11)))) -> (loca_level_below (admin) (sbu) (topsecret)) -> (forall L : zenon_U, (forall BA : zenon_U, (forall L1 : zenon_U, ((system_indi_is_background_admin (system) BA)->((background_admin_indi_has_background BA (alice) L1)->((loca_level_below (admin) L L1)->(admin_indi_has_background (admin) (alice) L))))))) -> (forall L : zenon_U, (forall L1 : zenon_U, (forall L11 : zenon_U, ((loca_level_direct_below (admin) L1 L11)->((loca_level_below (admin) L L1)->(loca_level_below (admin) L L11)))))) -> (~(admin_indi_has_level (admin) (alice) (sbu))) -> False). % 4.12/4.36 do 0 intro. intros zenon_H133 zenon_Hd2 zenon_Hd1 zenon_Hd0 zenon_H122 zenon_H123 zenon_H124 zenon_H12b zenon_Hcd zenon_Hc5 zenon_H134. % 4.12/4.36 generalize (zenon_H133 (topsecret)). zenon_intro zenon_H135. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H135); [ zenon_intro zenon_Hde | zenon_intro zenon_H136 ]. % 4.12/4.36 exact (zenon_Hde ax76). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H136); [ zenon_intro zenon_H58 | zenon_intro zenon_H137 ]. % 4.12/4.36 apply (zenon_L1_); trivial. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H137); [ zenon_intro zenon_He1 | zenon_intro zenon_H138 ]. % 4.12/4.36 exact (zenon_He1 zenon_Hd2). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H138); [ zenon_intro zenon_He3 | zenon_intro zenon_H139 ]. % 4.12/4.36 exact (zenon_He3 zenon_Hd1). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H139); [ zenon_intro zenon_He5 | zenon_intro zenon_H13a ]. % 4.12/4.36 exact (zenon_He5 zenon_Hd0). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H13a); [ zenon_intro zenon_H11c | zenon_intro zenon_H13b ]. % 4.12/4.36 generalize (ax2 (admin)). zenon_intro zenon_H103. % 4.12/4.36 generalize (zenon_H124 (confidential)). zenon_intro zenon_H125. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H125); [ zenon_intro zenon_H118 | zenon_intro zenon_H126 ]. % 4.12/4.36 apply (zenon_L23_); trivial. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H126); [ zenon_intro zenon_H127 | zenon_intro zenon_H11b ]. % 4.12/4.36 exact (zenon_H127 zenon_H123). % 4.12/4.36 generalize (zenon_H122 (confidential)). zenon_intro zenon_H11a. % 4.12/4.36 apply (zenon_L24_); trivial. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H13b); [ zenon_intro zenon_He8 | zenon_intro zenon_H13c ]. % 4.12/4.36 exact (zenon_He8 ax70). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H13c); [ zenon_intro zenon_Hea | zenon_intro zenon_H13d ]. % 4.12/4.36 exact (zenon_Hea ax77). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H13d); [ zenon_intro zenon_H121 | zenon_intro zenon_H13e ]. % 4.12/4.36 exact (zenon_H121 zenon_H12b). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H13e); [ zenon_intro zenon_H12c | zenon_intro zenon_H13f ]. % 4.12/4.36 apply (zenon_L27_); trivial. % 4.12/4.36 exact (zenon_H134 zenon_H13f). % 4.12/4.36 (* end of lemma zenon_L28_ *) % 4.12/4.36 assert (zenon_L29_ : (~(admin_indi_has_level (admin) (alice) (sbu))) -> (forall L : zenon_U, (forall L1 : zenon_U, (forall L11 : zenon_U, ((loca_level_direct_below (admin) L1 L11)->((loca_level_below (admin) L L1)->(loca_level_below (admin) L L11)))))) -> (forall L : zenon_U, (forall BA : zenon_U, (forall L1 : zenon_U, ((system_indi_is_background_admin (system) BA)->((background_admin_indi_has_background BA (alice) L1)->((loca_level_below (admin) L L1)->(admin_indi_has_background (admin) (alice) L))))))) -> (forall L11 : zenon_U, ((loca_level_direct_below (admin) (sbu) L11)->((loca_level_below (admin) (sbu) (sbu))->(loca_level_below (admin) (sbu) L11)))) -> (loca_level_below (admin) (sbu) (sbu)) -> (forall L1 : zenon_U, (forall L11 : zenon_U, ((loca_level_direct_below (admin) L1 L11)->((loca_level_below (admin) (sbu) L1)->(loca_level_below (admin) (sbu) L11))))) -> (admin_indi_has_credit (admin) (alice)) -> (admin_indi_has_employment (admin) (alice)) -> (admin_indi_has_polygraph (admin) (alice)) -> (forall L11 : zenon_U, ((system_indi_needs_level (system) (alice) (secret))->((admin_indi_has_citizenship (admin) (alice) (usa))->((admin_indi_has_polygraph (admin) (alice))->((admin_indi_has_employment (admin) (alice))->((admin_indi_has_credit (admin) (alice))->((loca_level_below (admin) (sbu) (secret))->((system_indi_is_level_admin (system) (level_admin))->((level_admin_indi_has_level (level_admin) (alice) L11)->((loca_level_below (admin) (sbu) L11)->((admin_indi_has_background (admin) (alice) (sbu))->(admin_indi_has_level (admin) (alice) (sbu))))))))))))) -> (loca_level_below (admin) (sbu) (secret)) -> (loca_level_direct_below (admin) (secret) (topsecret)) -> False). % 4.12/4.36 do 0 intro. intros zenon_H134 zenon_Hc5 zenon_Hcd zenon_H124 zenon_H123 zenon_H122 zenon_Hd0 zenon_Hd1 zenon_Hd2 zenon_H133 zenon_H11f zenon_Hba. % 4.12/4.36 generalize (zenon_H122 (secret)). zenon_intro zenon_H128. % 4.12/4.36 generalize (zenon_H128 (topsecret)). zenon_intro zenon_H129. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H129); [ zenon_intro zenon_Hb9 | zenon_intro zenon_H12a ]. % 4.12/4.36 exact (zenon_Hb9 zenon_Hba). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H12a); [ zenon_intro zenon_H11c | zenon_intro zenon_H12b ]. % 4.12/4.36 exact (zenon_H11c zenon_H11f). % 4.12/4.36 apply (zenon_L28_); trivial. % 4.12/4.36 (* end of lemma zenon_L29_ *) % 4.12/4.36 assert (zenon_L30_ : (forall L11 : zenon_U, ((loca_level_direct_below (admin) (confidential) L11)->((loca_level_below (admin) (sbu) (confidential))->(loca_level_below (admin) (sbu) L11)))) -> (loca_level_direct_below (admin) (confidential) (secret)) -> (loca_level_below (admin) (sbu) (confidential)) -> (~(admin_indi_has_level (admin) (alice) (sbu))) -> (forall L : zenon_U, (forall L1 : zenon_U, (forall L11 : zenon_U, ((loca_level_direct_below (admin) L1 L11)->((loca_level_below (admin) L L1)->(loca_level_below (admin) L L11)))))) -> (forall L : zenon_U, (forall BA : zenon_U, (forall L1 : zenon_U, ((system_indi_is_background_admin (system) BA)->((background_admin_indi_has_background BA (alice) L1)->((loca_level_below (admin) L L1)->(admin_indi_has_background (admin) (alice) L))))))) -> (forall L11 : zenon_U, ((loca_level_direct_below (admin) (sbu) L11)->((loca_level_below (admin) (sbu) (sbu))->(loca_level_below (admin) (sbu) L11)))) -> (loca_level_below (admin) (sbu) (sbu)) -> (forall L1 : zenon_U, (forall L11 : zenon_U, ((loca_level_direct_below (admin) L1 L11)->((loca_level_below (admin) (sbu) L1)->(loca_level_below (admin) (sbu) L11))))) -> (admin_indi_has_credit (admin) (alice)) -> (admin_indi_has_employment (admin) (alice)) -> (admin_indi_has_polygraph (admin) (alice)) -> (forall L11 : zenon_U, ((system_indi_needs_level (system) (alice) (secret))->((admin_indi_has_citizenship (admin) (alice) (usa))->((admin_indi_has_polygraph (admin) (alice))->((admin_indi_has_employment (admin) (alice))->((admin_indi_has_credit (admin) (alice))->((loca_level_below (admin) (sbu) (secret))->((system_indi_is_level_admin (system) (level_admin))->((level_admin_indi_has_level (level_admin) (alice) L11)->((loca_level_below (admin) (sbu) L11)->((admin_indi_has_background (admin) (alice) (sbu))->(admin_indi_has_level (admin) (alice) (sbu))))))))))))) -> (loca_level_direct_below (admin) (secret) (topsecret)) -> False). % 4.12/4.36 do 0 intro. intros zenon_H11a zenon_H103 zenon_H11b zenon_H134 zenon_Hc5 zenon_Hcd zenon_H124 zenon_H123 zenon_H122 zenon_Hd0 zenon_Hd1 zenon_Hd2 zenon_H133 zenon_Hba. % 4.12/4.36 generalize (zenon_H11a (secret)). zenon_intro zenon_H11d. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H11d); [ zenon_intro zenon_H102 | zenon_intro zenon_H11e ]. % 4.12/4.36 exact (zenon_H102 zenon_H103). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H11e); [ zenon_intro zenon_H120 | zenon_intro zenon_H11f ]. % 4.12/4.36 exact (zenon_H120 zenon_H11b). % 4.12/4.36 apply (zenon_L29_); trivial. % 4.12/4.36 (* end of lemma zenon_L30_ *) % 4.12/4.36 assert (zenon_L31_ : (forall L11 : zenon_U, ((system_indi_needs_level (system) (alice) (secret))->((admin_indi_has_citizenship (admin) (alice) (usa))->((admin_indi_has_polygraph (admin) (alice))->((admin_indi_has_employment (admin) (alice))->((admin_indi_has_credit (admin) (alice))->((loca_level_below (admin) (sbu) (secret))->((system_indi_is_level_admin (system) (level_admin))->((level_admin_indi_has_level (level_admin) (alice) L11)->((loca_level_below (admin) (sbu) L11)->((admin_indi_has_background (admin) (alice) (sbu))->(admin_indi_has_level (admin) (alice) (sbu))))))))))))) -> (admin_indi_has_polygraph (admin) (alice)) -> (admin_indi_has_employment (admin) (alice)) -> (admin_indi_has_credit (admin) (alice)) -> (forall L1 : zenon_U, (forall L11 : zenon_U, ((loca_level_direct_below (admin) L1 L11)->((loca_level_below (admin) (sbu) L1)->(loca_level_below (admin) (sbu) L11))))) -> (forall L : zenon_U, (forall BA : zenon_U, (forall L1 : zenon_U, ((system_indi_is_background_admin (system) BA)->((background_admin_indi_has_background BA (alice) L1)->((loca_level_below (admin) L L1)->(admin_indi_has_background (admin) (alice) L))))))) -> (forall L : zenon_U, (forall L1 : zenon_U, (forall L11 : zenon_U, ((loca_level_direct_below (admin) L1 L11)->((loca_level_below (admin) L L1)->(loca_level_below (admin) L L11)))))) -> (~(admin_indi_has_level (admin) (alice) (sbu))) -> (loca_level_below (admin) (sbu) (sbu)) -> False). % 4.12/4.36 do 0 intro. intros zenon_H133 zenon_Hd2 zenon_Hd1 zenon_Hd0 zenon_H122 zenon_Hcd zenon_Hc5 zenon_H134 zenon_H123. % 4.12/4.36 generalize (zenon_H122 (sbu)). zenon_intro zenon_H124. % 4.12/4.36 generalize (zenon_H122 (confidential)). zenon_intro zenon_H11a. % 4.12/4.36 generalize (ax3 (admin)). zenon_intro zenon_Hba. % 4.12/4.36 generalize (ax1 (admin)). zenon_intro zenon_H119. % 4.12/4.36 generalize (ax2 (admin)). zenon_intro zenon_H103. % 4.12/4.36 generalize (zenon_H124 (confidential)). zenon_intro zenon_H125. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H125); [ zenon_intro zenon_H118 | zenon_intro zenon_H126 ]. % 4.12/4.36 exact (zenon_H118 zenon_H119). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H126); [ zenon_intro zenon_H127 | zenon_intro zenon_H11b ]. % 4.12/4.36 exact (zenon_H127 zenon_H123). % 4.12/4.36 apply (zenon_L30_); trivial. % 4.12/4.36 (* end of lemma zenon_L31_ *) % 4.12/4.36 assert (zenon_L32_ : (forall L1 : zenon_U, (forall L2 : zenon_U, (forall B1 : zenon_U, (forall B2 : zenon_U, ((system_indi_is_oca (system) (oca))->((oca_compartment_is_compartment (oca) (compartmenta) L1 L2 B1 B2)->((admin_indi_has_level (admin) (alice) L1)->(admin_indi_has_level_for_compartment (admin) (alice) (compartmenta))))))))) -> (~(admin_indi_has_level_for_compartment (admin) (alice) (compartmenta))) -> (loca_level_below (admin) (sbu) (sbu)) -> (forall L : zenon_U, (forall L1 : zenon_U, (forall L11 : zenon_U, ((loca_level_direct_below (admin) L1 L11)->((loca_level_below (admin) L L1)->(loca_level_below (admin) L L11)))))) -> (forall L : zenon_U, (forall BA : zenon_U, (forall L1 : zenon_U, ((system_indi_is_background_admin (system) BA)->((background_admin_indi_has_background BA (alice) L1)->((loca_level_below (admin) L L1)->(admin_indi_has_background (admin) (alice) L))))))) -> (forall L1 : zenon_U, (forall L11 : zenon_U, ((loca_level_direct_below (admin) L1 L11)->((loca_level_below (admin) (sbu) L1)->(loca_level_below (admin) (sbu) L11))))) -> (admin_indi_has_credit (admin) (alice)) -> (admin_indi_has_employment (admin) (alice)) -> (admin_indi_has_polygraph (admin) (alice)) -> (forall L1 : zenon_U, (forall LA : zenon_U, (forall L11 : zenon_U, ((system_indi_needs_level (system) (alice) L1)->((admin_indi_has_citizenship (admin) (alice) (usa))->((admin_indi_has_polygraph (admin) (alice))->((admin_indi_has_employment (admin) (alice))->((admin_indi_has_credit (admin) (alice))->((loca_level_below (admin) (sbu) L1)->((system_indi_is_level_admin (system) LA)->((level_admin_indi_has_level LA (alice) L11)->((loca_level_below (admin) (sbu) L11)->((admin_indi_has_background (admin) (alice) (sbu))->(admin_indi_has_level (admin) (alice) (sbu))))))))))))))) -> False). % 4.12/4.36 do 0 intro. intros zenon_H140 zenon_H141 zenon_H123 zenon_Hc5 zenon_Hcd zenon_H122 zenon_Hd0 zenon_Hd1 zenon_Hd2 zenon_H142. % 4.12/4.36 generalize (zenon_H140 (sbu)). zenon_intro zenon_H143. % 4.12/4.36 generalize (zenon_H143 (unclassified)). zenon_intro zenon_H144. % 4.12/4.36 generalize (zenon_H144 (no)). zenon_intro zenon_H145. % 4.12/4.36 generalize (zenon_H145 (no)). zenon_intro zenon_H146. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H146); [ zenon_intro zenon_H88 | zenon_intro zenon_H147 ]. % 4.12/4.36 exact (zenon_H88 ax41). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H147); [ zenon_intro zenon_H149 | zenon_intro zenon_H148 ]. % 4.12/4.36 exact (zenon_H149 ax43). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H148); [ zenon_intro zenon_H134 | zenon_intro zenon_H14a ]. % 4.12/4.36 generalize (zenon_H142 (secret)). zenon_intro zenon_H14b. % 4.12/4.36 generalize (zenon_H14b (level_admin)). zenon_intro zenon_H133. % 4.12/4.36 apply (zenon_L31_); trivial. % 4.12/4.36 exact (zenon_H141 zenon_H14a). % 4.12/4.36 (* end of lemma zenon_L32_ *) % 4.12/4.36 assert (zenon_L33_ : (~(admin_indi_has_compartments (admin) (alice) (nil))) -> False). % 4.12/4.36 do 0 intro. intros zenon_H14c. % 4.12/4.36 generalize (ax26 (alice)). zenon_intro zenon_H14d. % 4.12/4.36 exact (zenon_H14c zenon_H14d). % 4.12/4.36 (* end of lemma zenon_L33_ *) % 4.12/4.36 assert (zenon_L34_ : (forall CL : zenon_U, ((admin_file_has_compartments (admin) (secretfile) CL)->((admin_indi_has_compartments (admin) (alice) CL)->(admin_indi_has_compartments_for_file (admin) (alice) (secretfile))))) -> (forall CL : zenon_U, ((system_file_needs_compartments (system) (secretfile) CL)->((admin_file_has_compartments_h (admin) (secretfile) CL CL)->(admin_file_has_compartments (admin) (secretfile) CL)))) -> (admin_indi_has_compartments (admin) (alice) (cons (compartmentb) (cons (compartmenta) (nil)))) -> (~(admin_indi_has_compartments_for_file (admin) (alice) (secretfile))) -> False). % 4.12/4.36 do 0 intro. intros zenon_H14e zenon_H67 zenon_H14f zenon_H150. % 4.12/4.36 generalize (zenon_H14e (cons (compartmentb) (cons (compartmenta) (nil)))). zenon_intro zenon_H151. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H151); [ zenon_intro zenon_H68 | zenon_intro zenon_H152 ]. % 4.12/4.36 apply (zenon_L4_); trivial. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H152); [ zenon_intro zenon_H154 | zenon_intro zenon_H153 ]. % 4.12/4.36 exact (zenon_H154 zenon_H14f). % 4.12/4.36 exact (zenon_H150 zenon_H153). % 4.12/4.36 (* end of lemma zenon_L34_ *) % 4.12/4.36 assert (zenon_L35_ : (admin_indi_has_employment (admin) (alice)) -> (admin_indi_has_polygraph (admin) (alice)) -> (admin_indi_has_credit (admin) (alice)) -> (forall C : zenon_U, (forall CL : zenon_U, (forall SSO : zenon_U, ((system_indi_needs_compartment (system) (alice) C)->((admin_indi_has_employment (admin) (alice))->((admin_indi_has_citizenship (admin) (alice) (usa))->((admin_indi_has_polygraph_for_compartment (admin) (alice) C)->((admin_indi_has_credit_for_compartment (admin) (alice) C)->((admin_compartment_has_sso (admin) C SSO)->((sso_indi_has_compartment SSO (alice) C)->((admin_indi_has_background_for_compartment (admin) (alice) C)->((admin_indi_has_level_for_compartment (admin) (alice) C)->((admin_indi_has_compartments (admin) (alice) CL)->(admin_indi_has_compartments (admin) (alice) (cons C CL))))))))))))))) -> (forall CL : zenon_U, ((admin_file_has_compartments (admin) (secretfile) CL)->((admin_indi_has_compartments (admin) (alice) CL)->(admin_indi_has_compartments_for_file (admin) (alice) (secretfile))))) -> (forall CL : zenon_U, ((system_file_needs_compartments (system) (secretfile) CL)->((admin_file_has_compartments_h (admin) (secretfile) CL CL)->(admin_file_has_compartments (admin) (secretfile) CL)))) -> (~(admin_indi_has_compartments_for_file (admin) (alice) (secretfile))) -> False). % 4.12/4.36 do 0 intro. intros zenon_Hd1 zenon_Hd2 zenon_Hd0 zenon_H155 zenon_H14e zenon_H67 zenon_H150. % 4.12/4.36 generalize (zenon_H155 (compartmentb)). zenon_intro zenon_H156. % 4.12/4.36 generalize (zenon_H156 (cons (compartmenta) (nil))). zenon_intro zenon_H157. % 4.12/4.36 generalize (zenon_H157 (sso_compartmentb)). zenon_intro zenon_H158. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H158); [ zenon_intro zenon_H15a | zenon_intro zenon_H159 ]. % 4.12/4.36 exact (zenon_H15a ax78). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H159); [ zenon_intro zenon_He3 | zenon_intro zenon_H15b ]. % 4.12/4.36 exact (zenon_He3 zenon_Hd1). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H15b); [ zenon_intro zenon_H58 | zenon_intro zenon_H15c ]. % 4.12/4.36 apply (zenon_L1_); trivial. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H15c); [ zenon_intro zenon_H15e | zenon_intro zenon_H15d ]. % 4.12/4.36 generalize (ax30 (alice)). zenon_intro zenon_H15f. % 4.12/4.36 generalize (zenon_H15f (compartmentb)). zenon_intro zenon_H160. % 4.12/4.36 generalize (zenon_H160 (oca)). zenon_intro zenon_H161. % 4.12/4.36 generalize (zenon_H161 (confidential)). zenon_intro zenon_H162. % 4.12/4.36 generalize (zenon_H162 (topsecret)). zenon_intro zenon_H163. % 4.12/4.36 generalize (zenon_H163 (yes)). zenon_intro zenon_H164. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H164); [ zenon_intro zenon_H88 | zenon_intro zenon_H165 ]. % 4.12/4.36 exact (zenon_H88 ax41). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H165); [ zenon_intro zenon_Hff | zenon_intro zenon_H166 ]. % 4.12/4.36 exact (zenon_Hff ax42). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H166); [ zenon_intro zenon_He1 | zenon_intro zenon_H167 ]. % 4.12/4.36 exact (zenon_He1 zenon_Hd2). % 4.12/4.36 exact (zenon_H15e zenon_H167). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H15d); [ zenon_intro zenon_H169 | zenon_intro zenon_H168 ]. % 4.12/4.36 generalize (ax32 (alice)). zenon_intro zenon_H16a. % 4.12/4.36 generalize (zenon_H16a (compartmentb)). zenon_intro zenon_H16b. % 4.12/4.36 generalize (zenon_H16b (oca)). zenon_intro zenon_H16c. % 4.12/4.36 generalize (zenon_H16c (confidential)). zenon_intro zenon_H16d. % 4.12/4.36 generalize (zenon_H16d (topsecret)). zenon_intro zenon_H16e. % 4.12/4.36 generalize (zenon_H16e (yes)). zenon_intro zenon_H16f. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H16f); [ zenon_intro zenon_H88 | zenon_intro zenon_H170 ]. % 4.12/4.36 exact (zenon_H88 ax41). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H170); [ zenon_intro zenon_Hff | zenon_intro zenon_H171 ]. % 4.12/4.36 exact (zenon_Hff ax42). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H171); [ zenon_intro zenon_He5 | zenon_intro zenon_H172 ]. % 4.12/4.36 exact (zenon_He5 zenon_Hd0). % 4.12/4.36 exact (zenon_H169 zenon_H172). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H168); [ zenon_intro zenon_H5e | zenon_intro zenon_H173 ]. % 4.12/4.36 apply (zenon_L16_); trivial. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H173); [ zenon_intro zenon_H175 | zenon_intro zenon_H174 ]. % 4.12/4.36 exact (zenon_H175 ax80). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H174); [ zenon_intro zenon_Hf9 | zenon_intro zenon_H176 ]. % 4.12/4.36 generalize (ax28 (alice)). zenon_intro zenon_H177. % 4.12/4.36 generalize (zenon_H177 (compartmentb)). zenon_intro zenon_H178. % 4.12/4.36 generalize (zenon_H178 (oca)). zenon_intro zenon_H179. % 4.12/4.36 generalize (zenon_H179 (confidential)). zenon_intro zenon_Hf7. % 4.12/4.36 generalize (ax20 (alice)). zenon_intro zenon_Hcd. % 4.12/4.36 generalize (zenon_Hcd (topsecret)). zenon_intro zenon_H17a. % 4.12/4.36 generalize (zenon_H17a (background_admin)). zenon_intro zenon_H17b. % 4.12/4.36 generalize (ax4 (admin)). zenon_intro zenon_Hbb. % 4.12/4.36 generalize (zenon_Hbb (topsecret)). zenon_intro zenon_H17c. % 4.12/4.36 generalize (zenon_H17b (topsecret)). zenon_intro zenon_H17d. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H17d); [ zenon_intro zenon_Hc9 | zenon_intro zenon_H17e ]. % 4.12/4.36 exact (zenon_Hc9 ax68). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H17e); [ zenon_intro zenon_Hcb | zenon_intro zenon_H17f ]. % 4.12/4.36 exact (zenon_Hcb ax74). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H17f); [ zenon_intro zenon_H180 | zenon_intro zenon_Hf8 ]. % 4.12/4.36 exact (zenon_H180 zenon_H17c). % 4.12/4.36 apply (zenon_L17_); trivial. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H176); [ zenon_intro zenon_H182 | zenon_intro zenon_H181 ]. % 4.12/4.36 generalize (ax29 (alice)). zenon_intro zenon_H183. % 4.12/4.36 generalize (zenon_H183 (compartmentb)). zenon_intro zenon_H184. % 4.12/4.36 generalize (zenon_H184 (oca)). zenon_intro zenon_H185. % 4.12/4.36 generalize (ax25 (alice)). zenon_intro zenon_Hd4. % 4.12/4.36 generalize (zenon_Hd4 (confidential)). zenon_intro zenon_H186. % 4.12/4.36 generalize (ax4 (admin)). zenon_intro zenon_Hbb. % 4.12/4.36 generalize (ax20 (alice)). zenon_intro zenon_Hcd. % 4.12/4.36 generalize (zenon_Hbb (confidential)). zenon_intro zenon_H105. % 4.12/4.36 generalize (ax5 (admin)). zenon_intro zenon_Hc5. % 4.12/4.36 generalize (zenon_Hc5 (confidential)). zenon_intro zenon_H110. % 4.12/4.36 generalize (zenon_H110 (confidential)). zenon_intro zenon_H104. % 4.12/4.36 generalize (zenon_H185 (confidential)). zenon_intro zenon_H187. % 4.12/4.36 generalize (zenon_H187 (topsecret)). zenon_intro zenon_H188. % 4.12/4.36 generalize (zenon_H188 (yes)). zenon_intro zenon_H189. % 4.12/4.36 generalize (zenon_H189 (yes)). zenon_intro zenon_H18a. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H18a); [ zenon_intro zenon_H88 | zenon_intro zenon_H18b ]. % 4.12/4.36 exact (zenon_H88 ax41). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H18b); [ zenon_intro zenon_Hff | zenon_intro zenon_H18c ]. % 4.12/4.36 exact (zenon_Hff ax42). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H18c); [ zenon_intro zenon_H18e | zenon_intro zenon_H18d ]. % 4.12/4.36 generalize (zenon_H186 (secret)). zenon_intro zenon_H18f. % 4.12/4.36 generalize (zenon_H18f (level_admin)). zenon_intro zenon_H190. % 4.12/4.36 generalize (zenon_H104 (secret)). zenon_intro zenon_H107. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H107); [ zenon_intro zenon_H102 | zenon_intro zenon_H108 ]. % 4.12/4.36 apply (zenon_L18_); trivial. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H108); [ zenon_intro zenon_H10a | zenon_intro zenon_H109 ]. % 4.12/4.36 exact (zenon_H10a zenon_H105). % 4.12/4.36 generalize (zenon_H190 (topsecret)). zenon_intro zenon_H191. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H191); [ zenon_intro zenon_Hde | zenon_intro zenon_H192 ]. % 4.12/4.36 exact (zenon_Hde ax76). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H192); [ zenon_intro zenon_H58 | zenon_intro zenon_H193 ]. % 4.12/4.36 apply (zenon_L1_); trivial. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H193); [ zenon_intro zenon_He1 | zenon_intro zenon_H194 ]. % 4.12/4.36 exact (zenon_He1 zenon_Hd2). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H194); [ zenon_intro zenon_He3 | zenon_intro zenon_H195 ]. % 4.12/4.36 exact (zenon_He3 zenon_Hd1). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H195); [ zenon_intro zenon_He5 | zenon_intro zenon_H196 ]. % 4.12/4.36 exact (zenon_He5 zenon_Hd0). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H196); [ zenon_intro zenon_H106 | zenon_intro zenon_H197 ]. % 4.12/4.36 exact (zenon_H106 zenon_H109). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H197); [ zenon_intro zenon_He8 | zenon_intro zenon_H198 ]. % 4.12/4.36 exact (zenon_He8 ax70). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H198); [ zenon_intro zenon_Hea | zenon_intro zenon_H199 ]. % 4.12/4.36 exact (zenon_Hea ax77). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H199); [ zenon_intro zenon_H10c | zenon_intro zenon_H19a ]. % 4.12/4.36 apply (zenon_L21_); trivial. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H19a); [ zenon_intro zenon_H111 | zenon_intro zenon_H19b ]. % 4.12/4.36 apply (zenon_L22_); trivial. % 4.12/4.36 exact (zenon_H18e zenon_H19b). % 4.12/4.36 exact (zenon_H182 zenon_H18d). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H181); [ zenon_intro zenon_H19c | zenon_intro zenon_H14f ]. % 4.12/4.36 generalize (zenon_H155 (compartmenta)). zenon_intro zenon_H19d. % 4.12/4.36 generalize (zenon_H19d (nil)). zenon_intro zenon_H19e. % 4.12/4.36 generalize (zenon_H19e (sso_compartmenta)). zenon_intro zenon_H19f. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H19f); [ zenon_intro zenon_H1a1 | zenon_intro zenon_H1a0 ]. % 4.12/4.36 exact (zenon_H1a1 ax79). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H1a0); [ zenon_intro zenon_He3 | zenon_intro zenon_H1a2 ]. % 4.12/4.36 exact (zenon_He3 zenon_Hd1). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H1a2); [ zenon_intro zenon_H58 | zenon_intro zenon_H1a3 ]. % 4.12/4.36 apply (zenon_L1_); trivial. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H1a3); [ zenon_intro zenon_H1a5 | zenon_intro zenon_H1a4 ]. % 4.12/4.36 generalize (ax31 (alice)). zenon_intro zenon_H1a6. % 4.12/4.36 generalize (zenon_H1a6 (compartmenta)). zenon_intro zenon_H1a7. % 4.12/4.36 generalize (zenon_H1a7 (oca)). zenon_intro zenon_H1a8. % 4.12/4.36 generalize (zenon_H1a8 (sbu)). zenon_intro zenon_H1a9. % 4.12/4.36 generalize (zenon_H1a9 (unclassified)). zenon_intro zenon_H1aa. % 4.12/4.36 generalize (zenon_H1aa (no)). zenon_intro zenon_H1ab. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H1ab); [ zenon_intro zenon_H88 | zenon_intro zenon_H1ac ]. % 4.12/4.36 exact (zenon_H88 ax41). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H1ac); [ zenon_intro zenon_H149 | zenon_intro zenon_H1ad ]. % 4.12/4.36 exact (zenon_H149 ax43). % 4.12/4.36 exact (zenon_H1a5 zenon_H1ad). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H1a4); [ zenon_intro zenon_H1af | zenon_intro zenon_H1ae ]. % 4.12/4.36 generalize (ax33 (alice)). zenon_intro zenon_H1b0. % 4.12/4.36 generalize (zenon_H1b0 (compartmenta)). zenon_intro zenon_H1b1. % 4.12/4.36 generalize (zenon_H1b1 (oca)). zenon_intro zenon_H1b2. % 4.12/4.36 generalize (zenon_H1b2 (sbu)). zenon_intro zenon_H1b3. % 4.12/4.36 generalize (zenon_H1b3 (unclassified)). zenon_intro zenon_H1b4. % 4.12/4.36 generalize (zenon_H1b4 (no)). zenon_intro zenon_H1b5. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H1b5); [ zenon_intro zenon_H88 | zenon_intro zenon_H1b6 ]. % 4.12/4.36 exact (zenon_H88 ax41). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H1b6); [ zenon_intro zenon_H149 | zenon_intro zenon_H1b7 ]. % 4.12/4.36 exact (zenon_H149 ax43). % 4.12/4.36 exact (zenon_H1af zenon_H1b7). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H1ae); [ zenon_intro zenon_H63 | zenon_intro zenon_H1b8 ]. % 4.12/4.36 generalize (ax6 (compartmenta)). zenon_intro zenon_H62. % 4.12/4.36 apply (zenon_L3_); trivial. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H1b8); [ zenon_intro zenon_H1ba | zenon_intro zenon_H1b9 ]. % 4.12/4.36 exact (zenon_H1ba ax81). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H1b9); [ zenon_intro zenon_H1bc | zenon_intro zenon_H1bb ]. % 4.12/4.36 generalize (ax28 (alice)). zenon_intro zenon_H177. % 4.12/4.36 generalize (zenon_H177 (compartmenta)). zenon_intro zenon_H1bd. % 4.12/4.36 generalize (zenon_H1bd (oca)). zenon_intro zenon_H1be. % 4.12/4.36 generalize (zenon_H1be (sbu)). zenon_intro zenon_H1bf. % 4.12/4.36 generalize (zenon_H1bf (unclassified)). zenon_intro zenon_H1c0. % 4.12/4.36 generalize (zenon_H1c0 (no)). zenon_intro zenon_H1c1. % 4.12/4.36 generalize (zenon_H1c1 (no)). zenon_intro zenon_H1c2. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H1c2); [ zenon_intro zenon_H88 | zenon_intro zenon_H1c3 ]. % 4.12/4.36 exact (zenon_H88 ax41). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H1c3); [ zenon_intro zenon_H149 | zenon_intro zenon_H1c4 ]. % 4.12/4.36 exact (zenon_H149 ax43). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H1c4); [ zenon_intro zenon_H1c6 | zenon_intro zenon_H1c5 ]. % 4.12/4.36 generalize (ax19 (alice)). zenon_intro zenon_H1c7. % 4.12/4.36 exact (zenon_H1c6 zenon_H1c7). % 4.12/4.36 exact (zenon_H1bc zenon_H1c5). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H1bb); [ zenon_intro zenon_H141 | zenon_intro zenon_H1c8 ]. % 4.12/4.36 generalize (ax29 (alice)). zenon_intro zenon_H183. % 4.12/4.36 generalize (zenon_H183 (compartmenta)). zenon_intro zenon_H1c9. % 4.12/4.36 generalize (zenon_H1c9 (oca)). zenon_intro zenon_H140. % 4.12/4.36 generalize (ax25 (alice)). zenon_intro zenon_Hd4. % 4.12/4.36 generalize (zenon_Hd4 (sbu)). zenon_intro zenon_H142. % 4.12/4.36 generalize (ax20 (alice)). zenon_intro zenon_Hcd. % 4.12/4.36 generalize (ax5 (admin)). zenon_intro zenon_Hc5. % 4.12/4.36 generalize (ax4 (admin)). zenon_intro zenon_Hbb. % 4.12/4.36 generalize (zenon_Hc5 (sbu)). zenon_intro zenon_H122. % 4.12/4.36 generalize (zenon_Hbb (sbu)). zenon_intro zenon_H123. % 4.12/4.36 apply (zenon_L32_); trivial. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H1c8); [ zenon_intro zenon_H14c | zenon_intro zenon_H1ca ]. % 4.12/4.36 apply (zenon_L33_); trivial. % 4.12/4.36 exact (zenon_H19c zenon_H1ca). % 4.12/4.36 apply (zenon_L34_); trivial. % 4.12/4.36 (* end of lemma zenon_L35_ *) % 4.12/4.36 assert (zenon_L36_ : (forall PA : zenon_U, ((system_indi_is_polygraph_admin (system) PA)->((polygraph_admin_indi_has_polygraph PA (alice))->(admin_indi_has_polygraph (admin) (alice))))) -> (admin_indi_has_employment (admin) (alice)) -> (admin_indi_has_credit (admin) (alice)) -> (forall C : zenon_U, (forall CL : zenon_U, (forall SSO : zenon_U, ((system_indi_needs_compartment (system) (alice) C)->((admin_indi_has_employment (admin) (alice))->((admin_indi_has_citizenship (admin) (alice) (usa))->((admin_indi_has_polygraph_for_compartment (admin) (alice) C)->((admin_indi_has_credit_for_compartment (admin) (alice) C)->((admin_compartment_has_sso (admin) C SSO)->((sso_indi_has_compartment SSO (alice) C)->((admin_indi_has_background_for_compartment (admin) (alice) C)->((admin_indi_has_level_for_compartment (admin) (alice) C)->((admin_indi_has_compartments (admin) (alice) CL)->(admin_indi_has_compartments (admin) (alice) (cons C CL))))))))))))))) -> (forall CL : zenon_U, ((admin_file_has_compartments (admin) (secretfile) CL)->((admin_indi_has_compartments (admin) (alice) CL)->(admin_indi_has_compartments_for_file (admin) (alice) (secretfile))))) -> (forall CL : zenon_U, ((system_file_needs_compartments (system) (secretfile) CL)->((admin_file_has_compartments_h (admin) (secretfile) CL CL)->(admin_file_has_compartments (admin) (secretfile) CL)))) -> (~(admin_indi_has_compartments_for_file (admin) (alice) (secretfile))) -> False). % 4.12/4.36 do 0 intro. intros zenon_Hed zenon_Hd1 zenon_Hd0 zenon_H155 zenon_H14e zenon_H67 zenon_H150. % 4.12/4.36 generalize (zenon_Hed (polygraph_admin)). zenon_intro zenon_Hee. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Hee); [ zenon_intro zenon_Hf0 | zenon_intro zenon_Hef ]. % 4.12/4.36 exact (zenon_Hf0 ax66). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Hef); [ zenon_intro zenon_Hf1 | zenon_intro zenon_Hd2 ]. % 4.12/4.36 exact (zenon_Hf1 ax72). % 4.12/4.36 apply (zenon_L35_); trivial. % 4.12/4.36 (* end of lemma zenon_L36_ *) % 4.12/4.36 assert (zenon_L37_ : (forall HR : zenon_U, ((system_indi_is_hr_admin (system) HR)->((hr_admin_indi_has_employment HR (alice))->(admin_indi_has_employment (admin) (alice))))) -> (forall PA : zenon_U, ((system_indi_is_polygraph_admin (system) PA)->((polygraph_admin_indi_has_polygraph PA (alice))->(admin_indi_has_polygraph (admin) (alice))))) -> (admin_indi_has_credit (admin) (alice)) -> (forall C : zenon_U, (forall CL : zenon_U, (forall SSO : zenon_U, ((system_indi_needs_compartment (system) (alice) C)->((admin_indi_has_employment (admin) (alice))->((admin_indi_has_citizenship (admin) (alice) (usa))->((admin_indi_has_polygraph_for_compartment (admin) (alice) C)->((admin_indi_has_credit_for_compartment (admin) (alice) C)->((admin_compartment_has_sso (admin) C SSO)->((sso_indi_has_compartment SSO (alice) C)->((admin_indi_has_background_for_compartment (admin) (alice) C)->((admin_indi_has_level_for_compartment (admin) (alice) C)->((admin_indi_has_compartments (admin) (alice) CL)->(admin_indi_has_compartments (admin) (alice) (cons C CL))))))))))))))) -> (forall CL : zenon_U, ((admin_file_has_compartments (admin) (secretfile) CL)->((admin_indi_has_compartments (admin) (alice) CL)->(admin_indi_has_compartments_for_file (admin) (alice) (secretfile))))) -> (forall CL : zenon_U, ((system_file_needs_compartments (system) (secretfile) CL)->((admin_file_has_compartments_h (admin) (secretfile) CL CL)->(admin_file_has_compartments (admin) (secretfile) CL)))) -> (~(admin_indi_has_compartments_for_file (admin) (alice) (secretfile))) -> False). % 4.12/4.36 do 0 intro. intros zenon_H1cb zenon_Hed zenon_Hd0 zenon_H155 zenon_H14e zenon_H67 zenon_H150. % 4.12/4.36 generalize (zenon_H1cb (hr_admin)). zenon_intro zenon_H1cc. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H1cc); [ zenon_intro zenon_H1ce | zenon_intro zenon_H1cd ]. % 4.12/4.36 exact (zenon_H1ce ax69). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H1cd); [ zenon_intro zenon_H1cf | zenon_intro zenon_Hd1 ]. % 4.12/4.36 exact (zenon_H1cf ax75). % 4.12/4.36 apply (zenon_L36_); trivial. % 4.12/4.36 (* end of lemma zenon_L37_ *) % 4.12/4.36 apply NNPP. intro zenon_G. % 4.12/4.36 generalize (ax39 (alice)). zenon_intro zenon_H1d0. % 4.12/4.36 generalize (zenon_H1d0 (secretfile)). zenon_intro zenon_H1d1. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H1d1); [ zenon_intro zenon_H1d3 | zenon_intro zenon_H1d2 ]. % 4.12/4.36 exact (zenon_H1d3 ax50). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H1d2); [ zenon_intro zenon_H1d5 | zenon_intro zenon_H1d4 ]. % 4.12/4.36 generalize (ax38 (alice)). zenon_intro zenon_H1d6. % 4.12/4.36 generalize (zenon_H1d6 (secretfile)). zenon_intro zenon_H1d7. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H1d7); [ zenon_intro zenon_H58 | zenon_intro zenon_H1d8 ]. % 4.12/4.36 apply (zenon_L1_); trivial. % 4.12/4.36 exact (zenon_H1d5 zenon_H1d8). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H1d4); [ zenon_intro zenon_H1da | zenon_intro zenon_H1d9 ]. % 4.12/4.36 generalize (ax36 (alice)). zenon_intro zenon_H1db. % 4.12/4.36 generalize (zenon_H1db (secretfile)). zenon_intro zenon_H1dc. % 4.12/4.36 generalize (zenon_H1dc (owner_secretfile)). zenon_intro zenon_H1dd. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H1dd); [ zenon_intro zenon_H1df | zenon_intro zenon_H1de ]. % 4.12/4.36 exact (zenon_H1df ax60). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H1de); [ zenon_intro zenon_H1e1 | zenon_intro zenon_H1e0 ]. % 4.12/4.36 exact (zenon_H1e1 ax82). % 4.12/4.36 exact (zenon_H1da zenon_H1e0). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H1d9); [ zenon_intro zenon_Hcf | zenon_intro zenon_H1e2 ]. % 4.12/4.36 generalize (ax35 (alice)). zenon_intro zenon_H1e3. % 4.12/4.36 generalize (zenon_H1e3 (secretfile)). zenon_intro zenon_Hd3. % 4.12/4.36 generalize (ax11 (secretfile)). zenon_intro zenon_H91. % 4.12/4.36 generalize (ax25 (alice)). zenon_intro zenon_Hd4. % 4.12/4.36 generalize (ax21 (alice)). zenon_intro zenon_H1cb. % 4.12/4.36 generalize (ax18 (alice)). zenon_intro zenon_Hf2. % 4.12/4.36 generalize (ax8 (secretfile)). zenon_intro zenon_H67. % 4.12/4.36 generalize (ax17 (alice)). zenon_intro zenon_Hed. % 4.12/4.36 generalize (zenon_H1cb (hr_admin)). zenon_intro zenon_H1cc. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H1cc); [ zenon_intro zenon_H1ce | zenon_intro zenon_H1cd ]. % 4.12/4.36 exact (zenon_H1ce ax69). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H1cd); [ zenon_intro zenon_H1cf | zenon_intro zenon_Hd1 ]. % 4.12/4.36 exact (zenon_H1cf ax75). % 4.12/4.36 apply (zenon_L15_); trivial. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_H1e2); [ zenon_intro zenon_H150 | zenon_intro zenon_H1e4 ]. % 4.12/4.36 generalize (ax34 (alice)). zenon_intro zenon_H1e5. % 4.12/4.36 generalize (zenon_H1e5 (secretfile)). zenon_intro zenon_H14e. % 4.12/4.36 generalize (ax8 (secretfile)). zenon_intro zenon_H67. % 4.12/4.36 generalize (ax27 (alice)). zenon_intro zenon_H155. % 4.12/4.36 generalize (ax21 (alice)). zenon_intro zenon_H1cb. % 4.12/4.36 generalize (ax18 (alice)). zenon_intro zenon_Hf2. % 4.12/4.36 generalize (ax17 (alice)). zenon_intro zenon_Hed. % 4.12/4.36 generalize (zenon_Hf2 (credit_admin)). zenon_intro zenon_Hf3. % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Hf3); [ zenon_intro zenon_Hf5 | zenon_intro zenon_Hf4 ]. % 4.12/4.36 exact (zenon_Hf5 ax67). % 4.12/4.36 apply (zenon_imply_s _ _ zenon_Hf4); [ zenon_intro zenon_Hf6 | zenon_intro zenon_Hd0 ]. % 4.12/4.36 exact (zenon_Hf6 ax73). % 4.12/4.36 apply (zenon_L37_); trivial. % 4.12/4.36 exact (zenon_G zenon_H1e4). % 4.12/4.36 Qed. % 4.12/4.36 % SZS output end Proof % 4.12/4.36 (* END-PROOF *) % 4.12/4.36 nodes searched: 363329 % 4.12/4.36 max branch formulas: 18710 % 4.12/4.36 proof nodes created: 9062 % 4.12/4.36 formulas created: 519208 % 4.12/4.36 %------------------------------------------------------------------------------