SECTION DEPENDENCIES: SYMBOL writeStore :: "(StoreId a) a PSt -> PSt" SYMBOL snd :: "!(a, !b) -> b" SYMBOL readStore :: "(StoreId a) PSt -> (a, PSt)" SYMBOL gec :: "((IncludeUpdate -> b -> PSt -> PSt) -> PSt -> (IncludeUpdate -> a -> PSt -> PSt, PSt)) (a -> b) (IncludeUpdate -> b -> PSt -> PSt) PSt -> (IncludeUpdate -> a -> PSt -> PSt, PSt)" SYMBOL self` :: "(((IncludeUpdate -> (a, EITHER a a) -> PSt -> PSt) -> PSt -> (IncludeUpdate -> (a, EITHER a a) -> PSt -> PSt, PSt)) -> (IncludeUpdate -> (a, EITHER a a) -> PSt -> PSt) -> PSt -> (IncludeUpdate -> (a, EITHER a a) -> PSt -> PSt, PSt)) ((IncludeUpdate -> a -> PSt -> PSt) -> PSt -> (IncludeUpdate -> a -> PSt -> PSt, PSt)) ((IncludeUpdate -> a -> PSt -> PSt) -> PSt -> (IncludeUpdate -> a -> PSt -> PSt, PSt)) (IncludeUpdate -> a -> PSt -> PSt) PSt -> (IncludeUpdate -> a -> PSt -> PSt, PSt)" SYMBOL feedback` :: "(((IncludeUpdate -> a -> PSt -> PSt) -> PSt -> (IncludeUpdate -> a -> PSt -> PSt, PSt)) -> ((IncludeUpdate -> a -> PSt -> PSt) -> PSt -> (IncludeUpdate -> a -> PSt -> PSt, PSt)) -> (IncludeUpdate -> a -> PSt -> PSt) -> PSt -> (IncludeUpdate -> a -> PSt -> PSt, PSt)) ((IncludeUpdate -> a -> PSt -> PSt) -> PSt -> (IncludeUpdate -> a -> PSt -> PSt, PSt)) (IncludeUpdate -> a -> PSt -> PSt) PSt -> (IncludeUpdate -> a -> PSt -> PSt, PSt)" SYMBOL self :: "((IncludeUpdate -> a -> PSt -> PSt) -> PSt -> (IncludeUpdate -> a -> PSt -> PSt, PSt)) ((IncludeUpdate -> a -> PSt -> PSt) -> PSt -> (IncludeUpdate -> a -> PSt -> PSt, PSt)) (IncludeUpdate -> a -> PSt -> PSt) PSt -> (IncludeUpdate -> a -> PSt -> PSt, PSt)" SYMBOL feedback :: "((IncludeUpdate -> a -> PSt -> PSt) -> PSt -> (IncludeUpdate -> a -> PSt -> PSt, PSt)) (IncludeUpdate -> a -> PSt -> PSt) PSt -> (IncludeUpdate -> a -> PSt -> PSt, PSt)" SYMBOL openStore :: "(StoreId a) (Maybe a) PSt -> (Bool, PSt)" SYMBOL Nothing :: "Maybe a" SYMBOL Just :: "a -> Maybe a" SYMBOL openStoreId :: "PSt -> (StoreId a, PSt)" SYMBOL StoreId :: "Int -> StoreId a" SYMBOL arr :: "(a -> b) (IncludeUpdate -> b -> PSt -> PSt) PSt -> (IncludeUpdate -> a -> PSt -> PSt, PSt)" SYMBOL id :: "!a -> a" SYMBOL loop :: "((IncludeUpdate -> (c, b) -> PSt -> PSt) -> PSt -> (IncludeUpdate -> (a, b) -> PSt -> PSt, PSt)) (IncludeUpdate -> c -> PSt -> PSt) PSt -> (IncludeUpdate -> a -> PSt -> PSt, PSt)" SYMBOL simple_loop :: "((a, b) -> (c, b)) a -> c" SYMBOL second :: "((IncludeUpdate -> b -> PSt -> PSt) -> PSt -> (IncludeUpdate -> a -> PSt -> PSt, PSt)) (IncludeUpdate -> (c, b) -> PSt -> PSt) PSt -> (IncludeUpdate -> (c, a) -> PSt -> PSt, PSt)" SYMBOL >>> :: "((IncludeUpdate -> b -> PSt -> PSt) -> PSt -> (IncludeUpdate -> a -> PSt -> PSt, PSt)) ((IncludeUpdate -> c -> PSt -> PSt) -> PSt -> (IncludeUpdate -> b -> PSt -> PSt, PSt)) (IncludeUpdate -> c -> PSt -> PSt) PSt -> (IncludeUpdate -> a -> PSt -> PSt, PSt)" SYMBOL assoc :: "((a, b), c) -> (a, (b, c))" SYMBOL unassoc :: "(a, (b, c)) -> ((a, b), c)" SYMBOL cross :: "(a -> b) (c -> d) (a, c) -> (b, d)" SYMBOL first :: "((IncludeUpdate -> b -> PSt -> PSt) -> PSt -> (IncludeUpdate -> a -> PSt -> PSt, PSt)) (IncludeUpdate -> (b, c) -> PSt -> PSt) PSt -> (IncludeUpdate -> (a, c) -> PSt -> PSt, PSt)" SYMBOL fst :: "!(!a, b) -> a" SYMBOL o :: "(a -> b) (c -> a) -> c -> b" SECTION DEFINES: THEOREM 01identity : (All f (= (@ 18 >>> (@ 13 arr (@ 14 id)) f) f)) THEOREM 02identity : (All f (= (@ 18 >>> f (@ 13 arr (@ 14 id))) f)) THEOREM 03associativity : (All f (All g (All h (= (@ 18 >>> (@ 18 >>> f g) h) (@ 18 >>> f (@ 18 >>> g h)))))) THEOREM 04functor_composition : (All g (All f (= (@ 13 arr (@ 24 o g f)) (@ 18 >>> (@ 13 arr f) (@ 13 arr g))))) THEOREM 05extension : (All f (= (@ 22 first (@ 13 arr f)) (@ 13 arr (@ 21 cross f (@ 14 id))))) THEOREM 06functor : (All f (All g (= (@ 22 first (@ 18 >>> f g)) (@ 18 >>> (@ 22 first f) (@ 22 first g))))) THEOREM 07exchange : (All f (All g (= (@ 18 >>> (@ 22 first f) (@ 13 arr (@ 21 cross (@ 14 id) g))) (@ 18 >>> (@ 13 arr (@ 21 cross (@ 14 id) g)) (@ 22 first f))))) THEOREM 08unit : (All f (= (@ 18 >>> (@ 22 first f) (@ 13 arr (@ 23 fst))) (@ 18 >>> (@ 13 arr (@ 23 fst)) f))) THEOREM 09association : (All f (= (@ 18 >>> (@ 22 first (@ 22 first f)) (@ 13 arr (@ 19 assoc))) (@ 18 >>> (@ 13 arr (@ 19 assoc)) (@ 22 first f)))) THEOREM 10left_tightening : (All h (All f (= (@ 15 loop (@ 18 >>> (@ 22 first h) f)) (@ 18 >>> h (@ 15 loop f))))) THEOREM 11right_tightening : (All f (All h (= (@ 15 loop (@ 18 >>> f (@ 22 first h))) (@ 18 >>> (@ 15 loop f) h)))) THEOREM 12sliding : (All f (All k (= (@ 15 loop (@ 18 >>> f (@ 13 arr (@ 21 cross (@ 14 id) k)))) (@ 15 loop (@ 18 >>> (@ 13 arr (@ 21 cross (@ 14 id) k)) f))))) THEOREM 13vanishing : (All f (= (@ 15 loop (@ 15 loop f)) (@ 15 loop (@ 18 >>> (@ 13 arr (@ 20 unassoc)) (@ 18 >>> f (@ 13 arr (@ 19 assoc))))))) THEOREM 14superposing : (All f (= (@ 17 second (@ 15 loop f)) (@ 15 loop (@ 18 >>> (@ 13 arr (@ 19 assoc)) (@ 18 >>> (@ 17 second f) (@ 13 arr (@ 20 unassoc))))))) THEOREM 15extension : (All f (= (@ 15 loop (@ 13 arr f)) (@ 13 arr (@ 16 simple_loop f)))) THEOREM GecCircuit : (All f (Ex f` (= f (@ 3 gec f f`)))) THEOREM axiom : (= (BOOL False) (BOOL True)) THEOREM feedback_self_id : (All f (= (@ 7 feedback f) (@ 6 self f (@ 13 arr (@ 14 id))))) THEOREM openStoreId_0 : (All env (= (@ 11 openStoreId env) (TUPLE (@ 12 StoreId (INT 0)) env))) THEOREM openStoreId_1 : (All env (= (@ 11 openStoreId env) (TUPLE (@ 12 StoreId (INT 1)) env))) THEOREM openStoreId_2 : (All env (= (@ 11 openStoreId env) (TUPLE (@ 12 StoreId (INT 2)) env))) THEOREM openStoreId_3 : (All env (= (@ 11 openStoreId env) (TUPLE (@ 12 StoreId (INT 3)) env))) THEOREM openStore_Just : (All i (All x (All env (= (@ 8 openStore i (@ 10 Just x) env) (TUPLE (BOOL True) (@ 0 writeStore i x env)))))) THEOREM openStore_Nothing : (All i (All env (= (@ 8 openStore i (@ 9 Nothing) env) (TUPLE (BOOL True) env)))) THEOREM readStore_writeStore : (All i (All x (All env (= (@ 2 readStore i (@ 0 writeStore i x env)) (TUPLE x env))))) THEOREM self`_feedback_self : (All g (All f (= (@ 4 self` (@ 7 feedback) g f) (@ 6 self g f)))) THEOREM self`_feedback`_self : (All g (All f (= (@ 4 self` (@ 5 feedback` (@ 6 self)) g f) (@ 6 self g f)))) THEOREM snd_readStore : (All i (All env (= (@ 1 snd (@ 2 readStore i env)) env))) THEOREM writeStore : (All i (All x (All env (= (@ 0 writeStore i x env) env)))) THEOREM: 01identity DEPENDS: 3 18 13 14 PROOF: Introduce f. Assume (Ex f` (= f (@ 3 gec f f`))). 1. Witness for H1. Rewrite -> All H1. Extensionality set1. Extensionality env1. Introduce env1 set1. Reduce NF All ( ). Injective. Split Deep. 1. Extensionality u1. Extensionality x1. Extensionality env2. Introduce env2 x1 u1. Reduce NF All ( ). Reflexive. 2. Reflexive. 2. Apply "GecCircuit". THEOREM: 02identity DEPENDS: 3 18 13 14 PROOF: Introduce f. Assume (Ex f` (= f (@ 3 gec f f`))). 1. Witness for H1. Rewrite -> All H1. Extensionality set1. Extensionality env1. Introduce env1 set1. Reduce NF All ( ). Injective. Split Deep. 1. Extensionality u1. Extensionality x1. Extensionality env2. Introduce env2 x1 u1. Reduce NF All ( ). Reflexive. 2. Reflexive. 2. Apply "GecCircuit". THEOREM: 03associativity DEPENDS: 18 PROOF: Introduce f g h. Extensionality set1. Extensionality env1. Introduce env1 set1. Reduce NF All ( ). SplitCase 4. 1. Reduce NF All ( ). Reflexive. 2. Reduce NF All ( ). Reflexive. THEOREM: 04functor_composition DEPENDS: 13 24 18 PROOF: Introduce g f. Extensionality set1. Extensionality env1. Introduce env1 set1. Reduce NF All ( ). Injective. Split Deep. 1. Extensionality u. Extensionality x. Extensionality env2. Introduce env2 x u. Reduce NF All ( ). Reflexive. 2. Reflexive. THEOREM: 05extension DEPENDS: 22 13 21 14 PROOF: Introduce f. Extensionality set1. Extensionality env1. Introduce env1 set1. Reduce 2 All ( ). Rewrite -> All "openStoreId_0". Rewrite -> All "openStore_Nothing". Reduce NF All ( ). Injective. Split Deep. 1. Extensionality u. Extensionality x. Extensionality env2. Introduce env2 x u. Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "readStore_writeStore". Reduce 1 All ( ). Reduce 1 All ( ). Reduce NF All ( ). Reflexive. 2. Reflexive. THEOREM: 06functor DEPENDS: 3 22 18 PROOF: Introduce f g. Assume (Ex f` (= f (@ 3 gec f f`))). 1. Assume (Ex g` (= g (@ 3 gec g g`))). 1. Witness for H1. Witness for H2. Rewrite -> All H1. Rewrite -> All H2. Extensionality set1. Extensionality env1. Introduce env1 set1. Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "openStoreId_0". Rewrite -> All "openStore_Nothing". Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "openStoreId_1". Reduce 1 All ( ). Rewrite -> All "openStore_Nothing". Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "openStoreId_2". Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "openStore_Nothing". Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Injective. Split Deep. 1. Extensionality u1. Extensionality x1. Extensionality env2. Introduce env2 x1 u1. Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "readStore_writeStore". Reduce 1 All ( ). Rewrite -> All "readStore_writeStore". Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "readStore_writeStore". Reduce 1 All ( ). Reduce 1 All ( ). Reduce NF All ( ). Reflexive. 2. Reflexive. 2. Apply "GecCircuit". 2. Apply "GecCircuit". THEOREM: 07exchange DEPENDS: 3 18 22 13 21 14 PROOF: Introduce f g. Assume (Ex f` (= f (@ 3 gec f f`))). 1. Assume (Ex g` (= g (@ 3 gec g g`))). 1. Witness for H2. Witness for H1. Rewrite -> All H1. Rewrite -> All H2. Extensionality set1. Extensionality env1. Introduce env1 set1. Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "openStoreId_0". Reduce 1 All ( ). Rewrite -> All "openStore_Nothing". Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "openStoreId_1". Reduce 1 All ( ). Rewrite -> All "openStore_Nothing". Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Injective. Split Deep. 1. Extensionality u1. Extensionality x1. Extensionality env2. Introduce env2 x1 u1. Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "readStore_writeStore". Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "readStore_writeStore". Reduce 1 All ( ). Reduce NF All ( ). Reflexive. 2. Reflexive. 2. Apply "GecCircuit". 2. Apply "GecCircuit". THEOREM: 08unit DEPENDS: 3 18 22 13 23 PROOF: Introduce f. Assume (Ex f` (= f (@ 3 gec f f`))). 1. Witness for H1. Extensionality set1. Extensionality env1. Introduce env1 set1. Rewrite -> All H1. Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "openStoreId_0". Reduce 1 All ( ). Rewrite -> All "openStore_Nothing". Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Injective. Split Deep. 1. Extensionality u1. Extensionality x1. Extensionality env2. Introduce env2 x1 u1. Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "readStore_writeStore". Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce NF All ( ). Reflexive. 2. Reflexive. 2. Apply "GecCircuit". THEOREM: 09association DEPENDS: 3 18 22 13 19 PROOF: Introduce f. Assume (Ex f` (= f (@ 3 gec f f`))). 1. Witness for H1. Rewrite -> All H1. Extensionality set1. Extensionality env1. Introduce env1 set1. Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "openStoreId_0". Reduce 1 All ( ). Rewrite -> All "openStore_Nothing". Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "openStoreId_1". Reduce 1 All ( ). Rewrite -> All "openStore_Nothing". Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "openStoreId_2". Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "openStore_Nothing". Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Injective. Split Deep. 1. Extensionality u1. Extensionality x1. Extensionality env2. Introduce env2 x1 u1. Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "readStore_writeStore". Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "readStore_writeStore". Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce NF All ( ). Reflexive. 2. Reflexive. 2. Apply "GecCircuit". THEOREM: 10left_tightening DEPENDS: 3 15 18 22 PROOF: Introduce h f. Assume (Ex f` (= f (@ 3 gec f f`))). 1. Assume (Ex h` (= h (@ 3 gec h h`))). 1. Witness for H1. Witness for H2. Extensionality set1. Extensionality env1. Introduce env1 set1. Rewrite -> All H1. Rewrite -> All H2. Reduce 1 All ( ). Rewrite -> All "openStoreId_0". Reduce 1 All ( ). Rewrite -> All "openStore_Nothing". Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "openStoreId_1". Reduce 1 All ( ). Rewrite -> All "openStore_Nothing". Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "openStoreId_2". Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "openStore_Nothing". Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Injective. Split Deep. 1. Extensionality u1. Extensionality x1. Extensionality env2. Introduce env2 x1 u1. Reduce 1 (set` 3 NO) ( ). Uncurry. Reduce 1 All ( ). Uncurry. Reduce 1 (set` 3 NO) ( ). Uncurry. Reduce 1 (loop_setcb 2 NO) ( ). Reduce 1 (first_setac 1 NO) ( ). Uncurry. Reduce 1 (set` 1 NO) ( ). Uncurry. Reduce 1 (first_setb 1 NO) ( ). Rewrite -> All "readStore_writeStore". Reduce 2 (first_setb2 1 NO) ( ). Uncurry. Reduce 1 (set` 1 NO) ( ). Uncurry. Reduce 1 (loop_setcb 1 NO) ( ). Rewrite -> All "readStore_writeStore". Reduce 4 (snd 2 NO) ( ). Reduce 4 (fst 3 NO) ( ). Reduce 4 (snd 2 NO) ( ). Reduce 4 (fst 1 NO) ( ). Reflexive. 2. Reflexive. 2. Apply "GecCircuit". 2. Apply "GecCircuit". THEOREM: 11right_tightening DEPENDS: 3 15 18 22 PROOF: Introduce f h. Assume (Ex f` (= f (@ 3 gec f f`))). 1. Assume (Ex h` (= h (@ 3 gec h h`))). 1. Witness for H1. Witness for H2. Rewrite -> All H1. Rewrite -> All H2. Extensionality set1. Extensionality env1. Introduce env1 set1. Reduce 1 All ( ). Rewrite -> All "openStoreId_0". Reduce 1 All ( ). Rewrite -> All "openStore_Nothing". Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "openStoreId_1". Reduce 1 All ( ). Rewrite -> All "openStore_Nothing". Reduce 1 All ( ). Rewrite -> All "openStoreId_2". Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "openStore_Nothing". Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Injective. Split Deep. 1. Extensionality u1. Extensionality x1. Extensionality env2. Introduce env2 x1 u1. Reduce 1 All ( ). Uncurry. Reduce 1 (set` 1 NO) ( ). Reduce 1 (set` 2 NO) ( ). Uncurry. Reduce 1 (first_setac 1 NO) ( ). Uncurry. Reduce 1 (set` 1 NO) ( ). Uncurry. Reduce 1 (first_setb 1 NO) ( ). Rewrite -> All "readStore_writeStore". Reduce 2 (first_setb2 1 NO) ( ). Uncurry. Reduce 1 (loop_setcb 1 NO) ( ). Reduce 1 (loop_setcb 1 NO) ( ). Rewrite -> All "readStore_writeStore". Reduce NF (snd 1 NO) ( ). Reduce NF (fst 1 NO) ( ). Uncurry. Reduce NF (set` 1 NO) ( ). Reflexive. 2. Reflexive. 2. Apply "GecCircuit". 2. Apply "GecCircuit". THEOREM: 12sliding DEPENDS: 3 15 18 13 21 14 PROOF: Introduce f k. Assume (Ex f` (= f (@ 3 gec f f`))). 1. Witness for H1. Rewrite -> All H1. Extensionality set1. Extensionality env1. Introduce env1 set1. Reduce 1 All ( ). Rewrite -> 1 "openStoreId_0". Rewrite -> All "openStoreId_1". Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "openStore_Nothing". Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Injective. Split Deep. 1. Extensionality u1. Extensionality x1. Extensionality env2. Introduce env2 x1 u1. Reduce 1 All ( ). Uncurry. Reduce 5 (set` 1 NO) ( ). Reduce 5 (arr_seta 1 NO) ( ). Rewrite -> All "readStore_writeStore". Uncurry. Reduce NF (snd 1 NO) ( ). Reduce NF (snd 2 NO) ( ). Reduce NF (cross 1 NO) ( ). Reduce NF (cross 1 NO) ( ). Reduce NF (fst 1 NO) ( ). Reduce 1 (_tupleselect_2_1 1 NO) ( ). Reduce 1 (_tupleselect_2_2 1 NO) ( ). Reduce 1 (_tupleselect_2_2 1 NO) ( ). Reduce 1 (_tupleselect_2_1 1 NO) ( ). * 2. Reflexive. 2. Apply "GecCircuit". THEOREM: 13vanishing DEPENDS: 3 15 18 13 20 19 PROOF: Introduce f. Assume (Ex f` (= f (@ 3 gec f f`))). 1. Witness for H1. Rewrite -> All H1. Extensionality set1. Extensionality env1. Introduce env1 set1. Reduce 1 All ( ). Rewrite -> 1 "openStoreId_0". Rewrite -> All "openStoreId_1". Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "openStore_Nothing". Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "openStoreId_2". Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "openStore_Nothing". Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Injective. Split Deep. 1. Extensionality u1. Extensionality x1. Extensionality env2. Introduce env2 x1 u1. Reduce 1 All ( ). Uncurry. Reduce 2 (arr_seta 1 NO) ( ). Reduce 2 (set` 2 NO) ( ). Reduce 2 (arr_seta 1 NO) ( ). Reduce 1 (loop_setcb 3 NO) ( ). Rewrite -> All "readStore_writeStore". Reduce 1 (loop_seta0 1 NO) ( ). Uncurry. Reduce 2 (set` 1 NO) ( ). Reduce 1 (loop_setcb 1 NO) ( ). Rewrite -> All "readStore_writeStore". Uncurry. Reduce 1 (loop_setcb 1 NO) ( ). * 2. Reflexive. 2. Apply "GecCircuit". THEOREM: 14superposing DEPENDS: 3 17 15 18 13 19 20 PROOF: Introduce f. Assume (Ex f` (= f (@ 3 gec f f`))). 1. Witness for H1. Rewrite -> All H1. Extensionality set1. Extensionality env1. Introduce env1 set1. Reduce 1 All ( ). Rewrite -> All "openStoreId_0". Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "openStore_Nothing". Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "openStoreId_1". Reduce 1 All ( ). Rewrite -> All "openStore_Nothing". Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "openStoreId_2". Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "openStoreId_3". Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "openStore_Nothing". Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Injective. Split Deep. 1. Extensionality u1. Extensionality x1. Extensionality env2. Introduce env2 x1 u1. Reduce 2 (arr_seta 1 NO) ( ). Reduce 2 (first_setac 1 NO) ( ). Reduce 1 All ( ). Uncurry. Reduce 2 (set` 1 NO) ( ). Reduce 2 (arr_seta 2 NO) ( ). Reduce 2 (arr_seta 2 NO) ( ). Reduce 2 (first_setac 1 NO) ( ). Reduce 2 (set` 1 NO) ( ). Reduce 1 (first_setb 2 NO) ( ). Rewrite -> All "readStore_writeStore". Reduce 3 (first_setb2 1 NO) ( ). Reduce 2 (arr_seta 2 NO) ( ). Reduce 2 (arr_seta 2 NO) ( ). Reduce 1 (loop_setcb 1 NO) ( ). Reduce 1 (loop_setcb 1 NO) ( ). Rewrite -> All "readStore_writeStore". Uncurry. Reduce 1 (first_setb 1 NO) ( ). Rewrite -> All "readStore_writeStore". Reduce 3 (first_setb2 1 NO) ( ). Reduce 1 (arr_seta 1 NO) ( ). Reduce 1 (unassoc 1 NO) ( ). Reduce 1 (unassoc 1 NO) ( ). Reduce 1 (assoc 1 NO) ( ). Reduce 1 (assoc 1 NO) ( ). Reduce 1 (assoc 1 NO) ( ). Reduce 1 (assoc 1 NO) ( ). Reduce 1 (assoc 1 NO) ( ). Reduce 1 (assoc 1 NO) ( ). Reduce 1 (assoc 1 NO) ( ). Reduce 1 (assoc 1 NO) ( ). Reduce 1 (assoc 1 NO) ( ). Reduce 1 (assoc 1 NO) ( ). Reduce NF (fst 1 NO) ( ). Reduce NF (fst 4 NO) ( ). Reduce NF (fst 3 NO) ( ). Reduce NF (fst 5 NO) ( ). Reduce NF (fst 4 NO) ( ). Reduce NF (fst 5 NO) ( ). Reduce NF (fst 5 NO) ( ). Reduce NF (fst 6 NO) ( ). Reduce NF (snd 9 NO) ( ). Reduce NF (snd 7 NO) ( ). Reduce NF (fst 6 NO) ( ). Reduce NF (fst 8 NO) ( ). Reduce NF (fst 8 NO) ( ). Reduce NF (fst 9 NO) ( ). Reduce 5 (snd 3 NO) ( ). Reduce 5 (snd 7 NO) ( ). Reduce 5 (snd 8 NO) ( ). Reduce 5 (snd 10 NO) ( ). Reduce 5 (snd 11 NO) ( ). Reduce 5 (fst 2 NO) ( ). * 2. Reflexive. 2. Apply "GecCircuit". THEOREM: 15extension DEPENDS: 15 13 16 PROOF: Introduce f. Extensionality set1. Extensionality env1. Introduce env1 set1. Reduce 1 All ( ). Rewrite -> All "openStoreId_0". Reduce 1 All ( ). Rewrite -> All "openStore_Nothing". Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Injective. Split Deep. 1. Extensionality u1. Extensionality x1. Extensionality env2. Introduce env2 x1 u1. Reduce 1 All ( ). Uncurry. Reduce 1 (arr_seta 1 NO) ( ). Uncurry. Reduce 1 (loop_setcb 1 NO) ( ). Rewrite -> All "readStore_writeStore". Reduce 2 (simple_loop 1 NO) ( ). * 2. Reflexive. THEOREM: GecCircuit DEPENDS: 3 PROOF: Contradiction. Assume (= (BOOL False) (BOOL True)). 1. AbsurdEqualityH H2. 2. Exact "axiom". THEOREM: axiom DEPENDS: PROOF: * THEOREM: feedback_self_id DEPENDS: 3 7 6 13 14 PROOF: Introduce f. Assume (Ex f` (= f (@ 3 gec f f`))). 1. Witness for H1. Rewrite -> All H1. Extensionality set1. Extensionality env1. Introduce env1 set1. Reduce 1 All ( ). Rewrite -> 1 "openStoreId_0". Rewrite -> 1 "openStoreId_1". Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "openStore_Just". Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 1 All ( ). Reduce 3 (RunCircuit 1 NO) ( ). Reduce 3 (RunCircuit 1 NO) ( ). Reduce 3 (RunCircuit 1 NO) ( ). * 2. Apply "GecCircuit". THEOREM: openStoreId_0 DEPENDS: 11 12 PROOF: Contradiction. Assume (= (BOOL False) (BOOL True)). 1. AbsurdEqualityH H2. 2. Rewrite -> All "axiom". Reflexive. THEOREM: openStoreId_1 DEPENDS: 11 12 PROOF: Contradiction. Assume (= (BOOL False) (BOOL True)). 1. AbsurdEqualityH H2. 2. Rewrite -> All "axiom". Reflexive. THEOREM: openStoreId_2 DEPENDS: 11 12 PROOF: Contradiction. Assume (= (BOOL False) (BOOL True)). 1. AbsurdEqualityH H2. 2. Rewrite -> All "axiom". Reflexive. THEOREM: openStoreId_3 DEPENDS: 11 12 PROOF: Contradiction. Assume (= (BOOL False) (BOOL True)). 1. AbsurdEqualityH H2. 2. Exact "axiom". THEOREM: openStore_Just DEPENDS: 8 10 0 PROOF: Introduce i x env. Reduce 1 All ( ). Reduce 1 All ( ). Reflexive. THEOREM: openStore_Nothing DEPENDS: 8 9 PROOF: Introduce i env. Reduce NF All ( ). Reflexive. THEOREM: readStore_writeStore DEPENDS: 2 0 PROOF: Contradiction. Assume (= (BOOL False) (BOOL True)). 1. AbsurdEqualityH H2. 2. Rewrite -> All "axiom". Reflexive. THEOREM: self`_feedback_self DEPENDS: 3 4 7 6 PROOF: Introduce g f. Assume (Ex f` (= f (@ 3 gec f f`))). 1. Assume (Ex g` (= g (@ 3 gec g g`))). 1. Witness for H2. Witness for H1. Rewrite -> All H1. Rewrite -> All H2. Extensionality set1. Extensionality env1. Introduce env1 set1. Reduce 1 All ( ). Reduce 1 All ( ). Rewrite -> All "openStoreId_0". SplitCase 1. 1. Definedness. 2. InjectiveH in H3. Split Deep H3. Rewrite <- All H4. Rewrite <- All H3. Reduce 1 All ( ). * 2. Apply "GecCircuit". 2. Apply "GecCircuit". THEOREM: self`_feedback`_self DEPENDS: 3 4 5 6 PROOF: Introduce g f. Assume (Ex f` (= f (@ 3 gec f f`))). 1. Assume (Ex g` (= g (@ 3 gec g g`))). 1. Witness for H1. Witness for H2. Extensionality set1. Extensionality env1. Introduce env1 set1. Rewrite -> All H1. Rewrite -> All H2. Reduce 17 (self` 1 NO) ( ). Rewrite -> All "openStoreId_0". Reduce 5 (self2 1 NO) ( ). Reduce 3 (RunCircuit 1 NO) ( ). SplitCase 2. 1. Definedness. 2. InjectiveH in H3. Split Deep H3. Rewrite <- All H4. Rewrite <- All H3. Reduce 2 (self 1 NO) ( ). Rewrite -> All "openStoreId_1". * 2. Apply "GecCircuit". 2. Apply "GecCircuit". THEOREM: snd_readStore DEPENDS: 1 2 PROOF: Contradiction. Assume (= (BOOL False) (BOOL True)). 1. AbsurdEqualityH H2. 2. Exact "axiom". THEOREM: writeStore DEPENDS: 0 PROOF: Contradiction. Assume (= (BOOL False) (BOOL True)). 1. AbsurdEqualityH H2. 2. Exact "axiom".