Commit 6f99809a authored by Maarten de Mol's avatar Maarten de Mol
Browse files

removed fsmodel1 from Malcolm

parent d8847ef9
SECTION DEPENDENCIES:
THEOREM int_== (ints)
SYMBOL eval_tuple2 :: "!(a, b) -> Bool | eval a & eval b"
SYMBOL _create_dictionary_eval :: "!untypable -> "
SYMBOL eval_int :: "!Int -> Bool"
SYMBOL eval_tuple3 :: "!(a, b, c) -> Bool | eval a & eval b & eval c"
SYMBOL eval_OpenStatus :: "!OpenStatus -> Bool"
SYMBOL eval_list :: "![a] -> Bool | eval a"
SYMBOL +_int :: "!Int !Int -> Int"
SYMBOL length_list :: "![a] -> Int"
SYMBOL take :: "Int ![a] -> [a]"
SYMBOL drop :: "Int ![a] -> [a]"
SYMBOL OpenR :: "OpenStatus"
SYMBOL OpenRW :: "OpenStatus"
SYMBOL lkpN :: "Int [(Int, a)] -> Maybe a"
SYMBOL ovwN :: "Int b [(Int, b)] -> [(Int, b)]"
SYMBOL eval_uarray :: "!{#Char} -> Bool"
SYMBOL mapMaybe :: "(a -> b) (Maybe a) -> Maybe b"
SYMBOL retf1n :: "Int -> ([(Int, ([Int], Int, OpenStatus))], a) -> (Int, Int, [Int], OpenStatus)"
SYMBOL rea0 :: "Int Int [(Int, ([Int], Int, OpenStatus))] -> Maybe ([(Int, ([Int], Int, OpenStatus))], [Int])"
SYMBOL fst :: "!(!a, b) -> a"
SYMBOL rea1 :: "Int (Int, Int, [Int], OpenStatus) -> Maybe ((Int, Int, [Int], OpenStatus), [Int])"
SYMBOL retf :: "[(Int, ([Int], Int, OpenStatus))] Int -> (Int, Int, [Int], OpenStatus)"
SYMBOL snd :: "!(a, !b) -> b"
SYMBOL ret :: "[(Int, ([Int], Int, OpenStatus))] -> [(Int, ([Int], OpenStatus))]"
SYMBOL ret1 :: "([Int], Int, OpenStatus) -> ([Int], OpenStatus)"
SYMBOL chgRngN :: "(b -> c) [(Int, b)] -> [(Int, c)]"
SYMBOL ope0 :: "Bool Int [(Int, ([Int], Int, OpenStatus))] -> Maybe [(Int, ([Int], Int, OpenStatus))]"
SYMBOL ope1 :: "Bool Int [(Int, ([Int], OpenStatus))] -> Maybe ([(Int, ([Int], OpenStatus))], (Int, Int, [Int], OpenStatus))"
SYMBOL test1 :: "Int ([Int], Int, OpenStatus) [(Int, ([Int], Int, OpenStatus))] -> Maybe ([Int], Int, OpenStatus)"
SYMBOL Just :: "a -> Maybe a"
SYMBOL ==_int :: "!Int !Int -> Bool"
SYMBOL clo0 :: "Int [(Int, ([Int], Int, OpenStatus))] -> Maybe [(Int, ([Int], Int, OpenStatus))]"
SYMBOL clo1 :: "(Int, Int, [Int], OpenStatus) [(Int, ([Int], OpenStatus))] -> Maybe [(Int, ([Int], OpenStatus))]"
SECTION DEFINES:
THEOREM clo : (All fs (All n {(= (@ 5 eval_list (@ 1 _create_dictionary_eval (@ 0 eval_tuple2 (@ 1 _create_dictionary_eval (@ 3 eval_tuple3 (@ 1 _create_dictionary_eval (@ 4 eval_OpenStatus)) (@ 1 _create_dictionary_eval (@ 2 eval_int)) (@ 1 _create_dictionary_eval (@ 5 eval_list (@ 1 _create_dictionary_eval (@ 2 eval_int)))))) (@ 1 _create_dictionary_eval (@ 14 eval_uarray)))) fs) (BOOL True)) -> (= (@ 15 mapMaybe (@ 22 ret) (@ 30 clo0 n fs)) (@ 31 clo1 (@ 20 retf fs n) (@ 22 ret fs)))}))
THEOREM eval_FS0 : (All v (All w {(= (@ 0 eval_tuple2 (@ 1 _create_dictionary_eval (@ 2 eval_int)) (@ 1 _create_dictionary_eval (@ 3 eval_tuple3 (@ 1 _create_dictionary_eval (@ 4 eval_OpenStatus)) (@ 1 _create_dictionary_eval (@ 2 eval_int)) (@ 1 _create_dictionary_eval (@ 5 eval_list (@ 1 _create_dictionary_eval (@ 2 eval_int)))))) (TUPLE v w)) (BOOL True)) -> {(= (@ 2 eval_int v) (BOOL True)) /\ (= (@ 3 eval_tuple3 (@ 1 _create_dictionary_eval (@ 5 eval_list (@ 1 _create_dictionary_eval (@ 2 eval_int)))) (@ 1 _create_dictionary_eval (@ 2 eval_int)) (@ 1 _create_dictionary_eval (@ 4 eval_OpenStatus)) w) (BOOL True))}}))
THEOREM eval_tuple : (All a (All b {(= (@ 0 eval_tuple2 (@ 1 _create_dictionary_eval (@ 2 eval_int)) (@ 1 _create_dictionary_eval (@ 2 eval_int)) (TUPLE a b)) (BOOL True)) -> {(= (@ 2 eval_int a) (BOOL True)) /\ (= (@ 2 eval_int b) (BOOL True))}}))
THEOREM int_==_reflexive : (All i {~(= i BOTTOM) -> (= (@ 29 ==_int i i) (BOOL True))})
THEOREM lkpN : (All fs (All n {(= (@ 5 eval_list (@ 1 _create_dictionary_eval (@ 0 eval_tuple2 (@ 1 _create_dictionary_eval (@ 3 eval_tuple3 (@ 1 _create_dictionary_eval (@ 4 eval_OpenStatus)) (@ 1 _create_dictionary_eval (@ 2 eval_int)) (@ 1 _create_dictionary_eval (@ 5 eval_list (@ 1 _create_dictionary_eval (@ 2 eval_int)))))) (@ 1 _create_dictionary_eval (@ 14 eval_uarray)))) fs) (BOOL True)) -> (= (@ 15 mapMaybe (@ 23 ret1) (@ 12 lkpN n fs)) (@ 12 lkpN n (@ 22 ret fs)))}))
THEOREM lkpN_ovwN : (All fs (All n (All v {(= (@ 5 eval_list (@ 1 _create_dictionary_eval (@ 0 eval_tuple2 (@ 1 _create_dictionary_eval (@ 3 eval_tuple3 (@ 1 _create_dictionary_eval (@ 4 eval_OpenStatus)) (@ 1 _create_dictionary_eval (@ 2 eval_int)) (@ 1 _create_dictionary_eval (@ 5 eval_list (@ 1 _create_dictionary_eval (@ 2 eval_int)))))) (@ 1 _create_dictionary_eval (@ 2 eval_int)))) fs) (BOOL True)) -> {(= (@ 2 eval_int n) (BOOL True)) -> (= (@ 27 test1 n v fs) (@ 28 Just v))}})))
THEOREM ope : (All fs (All b (All n {(= (@ 5 eval_list (@ 1 _create_dictionary_eval (@ 0 eval_tuple2 (@ 1 _create_dictionary_eval (@ 3 eval_tuple3 (@ 1 _create_dictionary_eval (@ 4 eval_OpenStatus)) (@ 1 _create_dictionary_eval (@ 2 eval_int)) (@ 1 _create_dictionary_eval (@ 5 eval_list (@ 1 _create_dictionary_eval (@ 2 eval_int)))))) (@ 1 _create_dictionary_eval (@ 14 eval_uarray)))) fs) (BOOL True)) -> (= (@ 15 mapMaybe (@ 22 ret) (@ 25 ope0 b n fs)) (@ 15 mapMaybe (@ 18 fst) (@ 26 ope1 b n (@ 22 ret fs))))})))
THEOREM ovwN : (All fs (All n (All v {(= (@ 5 eval_list (@ 1 _create_dictionary_eval (@ 0 eval_tuple2 (@ 1 _create_dictionary_eval (@ 3 eval_tuple3 (@ 1 _create_dictionary_eval (@ 4 eval_OpenStatus)) (@ 1 _create_dictionary_eval (@ 2 eval_int)) (@ 1 _create_dictionary_eval (@ 5 eval_list (@ 1 _create_dictionary_eval (@ 2 eval_int)))))) (@ 1 _create_dictionary_eval (@ 14 eval_uarray)))) fs) (BOOL True)) -> (= (@ 22 ret (@ 13 ovwN n v fs)) (@ 13 ovwN n (@ 23 ret1 v) (@ 22 ret fs)))})))
THEOREM rea_1 : (All fs (All n (All l {(= (@ 5 eval_list (@ 1 _create_dictionary_eval (@ 0 eval_tuple2 (@ 1 _create_dictionary_eval (@ 3 eval_tuple3 (@ 1 _create_dictionary_eval (@ 4 eval_OpenStatus)) (@ 1 _create_dictionary_eval (@ 2 eval_int)) (@ 1 _create_dictionary_eval (@ 5 eval_list (@ 1 _create_dictionary_eval (@ 2 eval_int)))))) (@ 1 _create_dictionary_eval (@ 14 eval_uarray)))) fs) (BOOL True)) -> (= (@ 15 mapMaybe (@ 21 snd) (@ 17 rea0 n l fs)) (@ 15 mapMaybe (@ 21 snd) (@ 19 rea1 l (@ 20 retf fs n))))})))
THEOREM rea_2 : (All fs (All n (All l {(= (@ 5 eval_list (@ 1 _create_dictionary_eval (@ 0 eval_tuple2 (@ 1 _create_dictionary_eval (@ 3 eval_tuple3 (@ 1 _create_dictionary_eval (@ 4 eval_OpenStatus)) (@ 1 _create_dictionary_eval (@ 2 eval_int)) (@ 1 _create_dictionary_eval (@ 5 eval_list (@ 1 _create_dictionary_eval (@ 2 eval_int)))))) (@ 1 _create_dictionary_eval (@ 14 eval_uarray)))) fs) (BOOL True)) -> (= (@ 15 mapMaybe (@ 16 retf1n n) (@ 17 rea0 n l fs)) (@ 15 mapMaybe (@ 18 fst) (@ 19 rea1 l (@ 20 retf fs n))))})))
THEOREM:
clo
DEPENDS:
24 13 12 5 1 0 3 4 2 14 15 22 30 31 20
PROOF:
Introduce fs n H1.
Opaque 12 lkpN.
Opaque 13 ovwN.
Opaque 24 chgRngN.
Reduce NF All ( ).
Cut "lkpN".
Introduce H2.
ReduceH 1 (ret 1 NO) in H2 ( ).
Rewrite <- All H2.
1. Reduce 1 (mapMaybe 1 NO) ( ).
SplitCase 3.
1. Reduce 1 (case 1 NO) ( ).
Reduce 1 (case 1 NO) ( ).
Reduce 1 (case 2 NO) ( ).
Reduce 1 (case 1 NO) ( ).
Reflexive.
2. Reduce NF All ( ).
Reflexive.
3. Rewrite -> All H3.
SplitCase 3.
1. Rewrite -> All H4.
Reduce 1 (ret1 2 NO) ( ).
Reduce 1 (case 5 NO) ( ).
Reduce NF All ( ).
Reflexive.
2. Rewrite -> All H4.
Cut "ovwN".
Introduce H5.
ReduceH 1 (ret 2 NO) in H5 ( ).
Reduce NF All ( ).
Reduce 1 (fromJust 1 NO) ( ).
Reduce 1 (case 3 NO) ( ).
ReduceH 1 (ret 1 NO) in H5 ( ).
Cases s1.
1. Reduce NF All ( ).
Reflexive.
2. Reduce NF All ( ).
Reflexive.
3. Reduce NF All ( ).
Rewrite -> All H5.
1. Reduce NF (ret1 1 NO) ( ).
Reflexive.
2. Apply H1.
4. Reduce NF All ( ).
Rewrite -> All H5.
1. Reduce 1 (ret1 1 NO) ( ).
Reduce 1 (case 1 NO) ( ).
Reflexive.
2. Apply H1.
2. Apply H1.
THEOREM:
eval_FS0
DEPENDS:
0 1 2 3 4 5
PROOF:
Introduce v w H1.
Split Deep.
1. ReduceH NF All in H1 ( ).
Cut H1.
SplitCase 1.
1. Definedness.
2. Introduce H3.
Apply H2.
3. Introduce H3.
AbsurdEqualityH H3.
2. ReduceH NF All in H1 ( ).
Cut H1.
SplitCase 1.
1. Definedness.
2. Introduce H3.
*
3. Introduce H3.
AbsurdEqualityH H3.
THEOREM:
eval_tuple
DEPENDS:
0 1 2
PROOF:
Introduce a b.
Reduce NF All ( ).
SplitCase 1.
1. Definedness.
2. Rewrite -> All H1.
Reduce NF All ( ).
Introduce H2.
Split Deep.
1. Apply H2.
2. Apply H2.
3. Introduce H2.
AbsurdEqualityH H2.
THEOREM 85-80-0-0:
int_==_reflexive
DEPENDS:
29
PROOF:
Introduce i H1.
Rewrite -> All "int_==".
1. Reflexive.
2. Apply H1.
THEOREM 0-0-65-65:
lkpN
DEPENDS:
5 1 0 3 4 2 14 15 23 12 22
PROOF:
Induction fs.
1. Definedness.
2. Reduce NF All ( ).
Reflexive.
3. Introduce f fs IH n.
Reduce 1 (eval_list 1 NO) ( ).
Reduce 1 (case 1 NO) ( ).
SplitCase 1.
1. Definedness.
2. Introduce H2.
Reduce 1 (lkpN 2 NO) ( ).
Reduce 1 (ret 1 NO) ( ).
ReduceH 1 (ret 1 NO) in IH ( ).
Reduce 1 (chgRngN 1 NO) ( ).
Reduce 1 (case 2 NO) ( ).
SplitCase 2.
1. Definedness.
2. Reduce 1 (case 1 NO) ( ).
Reduce 1 (case 1 NO) ( ).
Rewrite <- All IH.
1. Reduce 1 (mapMaybe 1 NO) ( ).
Reduce 1 (lkpN 1 NO) ( ).
Reduce 1 (case 2 NO) ( ).
Rewrite -> All H3.
Reduce 1 (case 2 NO) ( ).
SplitCase 2.
1. Reduce NF All ( ).
Reflexive.
2. Reduce NF All ( ).
Reflexive.
3. Reduce NF All ( ).
Reflexive.
2. Apply H2.
3. Introduce H2.
AbsurdEqualityH H2.
THEOREM:
lkpN_ovwN
DEPENDS:
5 1 0 3 4 2 27 28
PROOF:
Induction fs.
1. Definedness.
2. Introduce n v H1 H2.
Assume ~(= n BOTTOM).
1. Apply "int_==_reflexive" to H3.
Reduce NF All ( ).
Rewrite -> All H4.
Reduce NF All ( ).
Reflexive.
2. Definedness.
3. Introduce f fs IH n v H1 H2.
Cut H1.
Reduce NF (eval_list 1 NO) ( ).
SplitCase 1.
1. Definedness.
2. Introduce H4.
Assume ~(= n BOTTOM).
1. Reduce 1 (test1 1 NO) ( ).
Reduce 1 (lkpN 1 NO) ( ).
Reduce 1 (ovwN 1 NO) ( ).
Reduce 1 (case 2 NO) ( ).
SplitCase 2.
1. Definedness.
2. SplitCase 2.
1. Rewrite -> All H6 in H3.
Assume ~(= v1 BOTTOM).
1. Definedness.
2. *
2. Reduce 1 (case 1 NO) ( ).
Reduce 1 (case 1 NO) ( ).
Apply "int_==_reflexive" to H5.
Rewrite -> All H8.
Reduce NF All ( ).
Reflexive.
3. Reduce 2 (case 1 NO) ( ).
Assume ~(= v1 BOTTOM).
1. Rewrite -> All H7.
Reduce 1 (case 1 NO) ( ).
ReduceH 1 (test1 1 NO) in IH ( ).
Apply IH.
Split Deep.
1. Apply H4.
2. Apply H2.
2. Definedness.
2. Definedness.
3. Introduce H4.
AbsurdEqualityH H4.
THEOREM:
ope
DEPENDS:
24 13 12 5 1 0 3 4 2 14 15 22 25 18 26
PROOF:
Introduce fs b n H1.
Reduce 1 (ope0 1 NO) ( ).
Reduce 1 (ope1 1 NO) ( ).
Rewrite <- All "lkpN".
1. Opaque 12 lkpN.
Opaque 13 ovwN.
Opaque 24 chgRngN.
Reduce NF All ( ).
SplitCase 3.
1. Reduce NF All ( ).
Reflexive.
2. Rewrite -> All H2.
Reduce NF All ( ).
Injective.
Cut "ovwN".
Introduce H3.
ReduceH 1 (ret 2 NO) in H3 ( ).
ReduceH 1 (ret 1 NO) in H3 ( ).
Rewrite -> All H3.
1. Reduce 1 (ret1 1 NO) ( ).
Reduce 1 (case 1 NO) ( ).
Reflexive.
2. Apply H1.
3. Rewrite -> All H2.
Reduce NF All ( ).
SplitCase 3.
1. Reduce NF All ( ).
Reflexive.
2. Rewrite -> All H3.
Reduce NF All ( ).
SplitCase 2.
1. Reduce NF All ( ).
Reflexive.
2. Reduce NF All ( ).
Reflexive.
3. Reduce NF All ( ).
Cut "ovwN".
Introduce H5.
ReduceH 1 (ret 1 NO) in H5 ( ).
Rewrite -> All H5.
1. Injective.
Reduce 1 (ret1 1 NO) ( ).
Reduce 1 (case 1 NO) ( ).
Reduce 1 (ret 1 NO) ( ).
Reflexive.
2. Apply H1.
2. Apply H1.
THEOREM 0-0-65-65:
ovwN
DEPENDS:
5 1 0 3 4 2 14 22 13 23
PROOF:
Induction fs.
1. Definedness.
2. Reduce NF All ( ).
Reflexive.
3. Introduce f fs IH n v.
Reduce NF (eval_list 1 NO) ( ).
SplitCase 1.
1. Definedness.
2. Introduce H2.
Reduce 1 (ovwN 2 NO) ( ).
ReduceH 1 (ret 2 NO) in IH ( ).
Reduce 1 (ret 2 NO) ( ).
Reduce 1 (chgRngN 1 NO) ( ).
Reduce 1 (case 2 NO) ( ).
SplitCase 2.
1. Definedness.
2. Reduce 1 (case 1 NO) ( ).
Reduce 1 (case 1 NO) ( ).
Rewrite <- All IH.
1. Rewrite -> All H3.
SplitCase 1.
1. Reduce 1 (ovwN 1 NO) ( ).
Reduce 1 (case 1 NO) ( ).
Reduce 1 (case 1 NO) ( ).
Rewrite -> All H4.
Reduce NF All ( ).
Reflexive.
2. Reduce 1 (ovwN 1 NO) ( ).
Reduce 2 (case 1 NO) ( ).
Rewrite -> All H4.
Reduce 1 (case 1 NO) ( ).
Reduce 2 (ret 1 NO) ( ).
Reduce 1 (case 1 NO) ( ).
Reduce 1 (case 1 NO) ( ).
Reflexive.
3. Reduce 1 (ret 1 NO) ( ).
Reduce 1 (chgRngN 1 NO) ( ).
Reduce 3 (case 1 NO) ( ).
Rewrite -> All H4.
Reduce 1 (case 2 NO) ( ).
Reduce 1 (case 1 NO) ( ).
Reduce 1 (case 1 NO) ( ).
Reduce 1 (ret 1 NO) ( ).
Reflexive.
2. Apply H2.
3. Introduce H2.
AbsurdEqualityH H2.
THEOREM:
rea_1
DEPENDS:
12 13 5 1 0 3 4 2 14 15 21 17 19 20
PROOF:
Introduce fs n l H1.
Reduce 1 (rea0 1 NO) ( ).
Reduce 1 (rea1 1 NO) ( ).
Reduce 1 (retf 1 NO) ( ).
Opaque 13 ovwN.
Opaque 12 lkpN.
Reduce 1 (mapMaybe 1 NO) ( ).
Reduce 1 (mapMaybe 1 NO) ( ).
Reduce 1 (let 1 NO) ( ).
Reduce 1 (let 1 NO) ( ).
SplitCase 3.
1. Rewrite -> All H2.
Reduce NF All ( ).
Reflexive.
2. Rewrite -> All H2.
Reduce NF All ( ).
Reflexive.
3. Rewrite -> All H2.
SplitCase 3.
1. Rewrite -> All H3.
Reduce NF All ( ).
Reflexive.
2. Rewrite -> All H3.
Reduce NF All ( ).
SplitCase 2.
1. Reflexive.
2. Reflexive.
3. Reduce NF All ( ).
Reflexive.
THEOREM:
rea_2
DEPENDS:
6 7 8 9 10 11 2 12 13 5 1 0 3 4 14 15 16 17 18 19 20
PROOF:
Introduce fs n l H1.
Opaque 13 ovwN.
Opaque 12 lkpN.
Reduce NF All ( ).
SplitCase 3.
1. Rewrite -> All H2.
Reduce NF All ( ).
Reflexive.
2. Rewrite -> All H2.
Reduce NF All ( ).
Reflexive.
3. Rewrite -> All H2.
SplitCase 3.
1. Reduce NF All ( ).
Reflexive.
2. Rewrite -> All H3.
Reduce NF All ( ).
Reduce 1 (fromJust 1 NO) ( ).
Reduce 1 (case 3 NO) ( ).
Reduce 1 (_tupleselect_3_1 1 NO) ( ).
Reduce 1 (case 3 NO) ( ).
Reduce 1 (fromJust 1 NO) ( ).
Reduce 1 (case 3 NO) ( ).
Reduce 1 (_tupleselect_3_2 1 NO) ( ).
Reduce 1 (case 3 NO) ( ).
Reduce 1 (fromJust 1 NO) ( ).
Reduce 1 (case 3 NO) ( ).
Reduce 1 (_tupleselect_3_2 1 NO) ( ).
Reduce 1 (case 3 NO) ( ).
Reduce 1 (fromJust 1 NO) ( ).
Reduce 1 (case 3 NO) ( ).
Reduce 1 (_tupleselect_3_1 1 NO) ( ).
Reduce 1 (case 3 NO) ( ).
Reduce 1 (fromJust 1 NO) ( ).
Reduce 1 (case 3 NO) ( ).
Reduce 1 (_tupleselect_3_3 1 NO) ( ).
Reduce 1 (case 3 NO) ( ).
Reduce 1 (fromJust 1 NO) ( ).
Reduce 1 (case 3 NO) ( ).
Reduce 1 (_tupleselect_3_2 1 NO) ( ).
Reduce 1 (case 3 NO) ( ).
Reduce 1 (fromJust 1 NO) ( ).
Reduce 1 (case 3 NO) ( ).
Reduce 1 (_tupleselect_3_1 1 NO) ( ).
Reduce 1 (case 3 NO) ( ).
Reduce 1 (_tupleselect_3_1 1 NO) ( ).
Reduce 1 (_tupleselect_3_1 1 NO) ( ).
Reduce 1 (case 16 NO) ( ).
Reduce 1 (case 16 NO) ( ).
Reduce 1 (case 15 NO) ( ).
Reduce NF (_tupleselect_3_2 1 NO) ( ).
Reduce NF (_tupleselect_3_2 1 NO) ( ).
Reduce NF (_tupleselect_3_2 1 NO) ( ).
Reduce NF (_tupleselect_3_1 1 NO) ( ).
Cases s1.
1. Reduce NF All ( ).
Reflexive.
2. Reduce NF All ( ).
Reflexive.
3. Reduce NF All ( ).
Assume (= (@ 2 eval_int n) (BOOL True)).
1. Cut "lkpN_ovwN".
Introduce H5.
SpecializeE H5 with fs.
SpecializeE H5 with n.
SpecializeE H5 with (TUPLE d1 (@ 6 +_int p1 (@ 7 length_list (@ 8 take l (@ 9 drop p1 d1)))) (@ 11 OpenRW)).
*
2. *
4. Reduce NF (==_OpenStatus 1 NO) ( ).
Reduce 1 (case 1 NO) ( ).
Reduce 1 (case 1 NO) ( ).
Reduce 1 (case 1 NO) ( ).
Cut "lkpN_ovwN".
Introduce H4.
SpecializeE H4 with fs.
SpecializeE H4 with n.
SpecializeE H4 with (TUPLE d1 (@ 6 +_int p1 (@ 7 length_list (@ 8 take l (@ 9 drop p1 d1)))) (@ 10 OpenR)).
*
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment